[Merged by Bors] - feat(analysis/convex/combination): lemmas connecting convex hull with affine combinations and barycentric coordinates

[ocfnash]

---

[PatrickMassot]

I felt very sad that all those lemmas are duplicated so I tried to deduced this version from the existing lemma. But of course I got a proof that is longer... I'll paste this proof here anyway. If someone has courage maybe more finset.sum or affine geometry lemmas could be extracted to make it shorter. But I'm ready to merge your version if nobody has courage (however something is really wrong, all those proofs shouldn't be so painful).

lemma finset.sum_image'' {α β γ : Type*} [add_comm_monoid γ] (s : finset α) (f : α → β) (g : α → γ) :
 ∑ a in s, g a = ∑ b in s.image f, (∑ a in s, if f a = b then g a else 0) :=
begin
  rw finset.sum_image' g,  
  intros b b_in,  
  rw sum_filter
end

example (v : ι → E) :
  convex_hull R (range v) = { x | ∃ (s : finset ι) (w : ι → R)
    (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1), s.affine_combination v w = x } :=
begin
  rw convex_hull_eq,
  ext x,
  dsimp,
  split,
  { rintro ⟨J, s, w, p, hw, ⟨hw', mem, H⟩⟩,
    obtain ⟨j, j_in⟩ : s.nonempty,
    { by_contra H',
      rw [finset.not_nonempty_iff_eq_empty] at H',
      rw [H', sum_empty] at hw',
      exact zero_ne_one hw' },
    cases mem j j_in with i hi,
    haveI : nonempty ι := ⟨i⟩,
    dsimp [set.range] at mem,
    choose! f hf using mem,
    use finset.image f s,
    have h_sum : ∑ (i : ι) in image f s, ∑ (j : J) in s, ite (f j = i) (w j) 0 = 1,
    by rwa ← s.sum_image'',
    refine ⟨λ i, ∑ j in s, if f j = i then w j else 0, _, _, _⟩,
    { intros i i_in,
      apply sum_nonneg,
      intros j j_in,
      split_ifs ; simp [hw j j_in] },
    { exact h_sum },
    { rw affine_combination_eq_center_mass,
      { rw finset.center_mass_eq_of_sum_1 _ _ h_sum,
        rw finset.center_mass_eq_of_sum_1 _ _ hw' at H,
        rw ← H,
        dsimp,
        simp_rw [sum_smul, ite_smul, zero_smul],
        have : ∀ j i, ite (f j = i) (w j • v i) 0 = ite (f j = i) (w j • v (f j)) 0,
        { intros j i, 
          split_ifs with h ; simp [h] },
        simp_rw this,
        rw ← s.sum_image'' f,
        apply sum_congr rfl,
        intros j j_in,
        rw [hf j j_in] },
      { exact h_sum } } },
   { rintro ⟨s, w, w_nonneg, w_sum, rfl⟩,
    use [ι, s, w, v, w_nonneg, w_sum],
    simp [affine_combination_eq_center_mass w_sum] }
end

[ocfnash]

I agree; also thanks for working out this new proof!

However I am inclined to stick with what I have. This is mostly because I think the right way to tidy up the mess here is to remove the (in my opinion) bad center_mass definition and instead to restate everything in terms of finset.affine_combination.

With that in mind I was motivated to come up with a proof that would be optimised for ease of such a future refactor, which is more or less what I've done here. In addition I started out reusing the existing lemmas but then decided (apparently correctly, in view of your proof) that it would be harder to write, harder to maintain, and longer.

Incidentally, my proof could be improved by building out a proper API for working with the fact that an affine combination of affine combinations is an affine combination but I felt I'd never get there if I took this detour.

I should also say that there is also a WIP PR #9268 which should be a step in the right direction.

[PatrickMassot]

I agree, I pasted my code there to archive it somewhere just in case.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests