English
The convex hull of a Cartesian product of spaces is the product of the convex hulls, under suitable finiteness assumptions.
Русский
Выпуклая оболочка декартового произведения пространств равна произведению выпуклых оболочек, при соответствующих ограничениях на конечность.
LaTeX
$$$\operatorname{conv}(R, \prod_i E_i) = \prod_i \operatorname{conv}(R, E_i)$$$
Lean4
theorem mem_convexHull_pi (h : ∀ i ∈ s, x i ∈ convexHull 𝕜 (t i)) : x ∈ convexHull 𝕜 (s.pi t) := by
classical
cases nonempty_fintype ι
wlog hs : s = Set.univ generalizing s t
· rw [← pi_univ_ite]
refine this (fun i _ ↦ ?_) rfl
split_ifs with hi
· exact h i hi
· simp
subst hs
simp only [Set.mem_univ, mem_convexHull_iff_exists_fintype, true_implies] at h
choose κ _ w f hw₀ hw₁ hft hf using h
refine
mem_convexHull_of_exists_fintype (fun k : Π i, κ i ↦ ∏ i, w i (k i)) (fun g i ↦ f _ (g i))
(fun g ↦ prod_nonneg fun _ _ ↦ hw₀ _ _) ?_ (fun _ _ _ ↦ hft _ _) ?_
· rw [← Fintype.prod_sum]
exact prod_eq_one fun _ _ ↦ hw₁ _
ext i
calc
_ = ∑ g : ∀ i, κ i, (∏ i, w i (g i)) • f i (g i) := by simp only [Finset.sum_apply, Pi.smul_apply]
_ = ∑ j : κ i, ∑ g : { g : ∀ k, κ k // g i = j }, (∏ k, w k (g.1 k)) • f i ((g : ∀ i, κ i) i) := by
rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]
_ = ∑ j : κ i, (∑ g : { g : ∀ k, κ k // g i = j }, ∏ k, w k (g.1 k)) • f i j :=
by
simp_rw [sum_smul]
congr! with j _ g _
exact g.2
_ = ∑ j : κ i, w i j • f i j := ?_
_ = x i := hf _
congr! with j _
calc
∑ g : { g : ∀ k, κ k // g i = j }, ∏ k, w k (g.1 k) =
∑ g ∈ piFinset fun k ↦ if hk : k = i then hk ▸ { j } else univ, ∏ k, w k (g k) :=
Finset.sum_bij' (fun g _ ↦ g) (fun g hg ↦ ⟨g, by simpa using mem_piFinset.1 hg i⟩) (by aesop) (by simp) (by simp)
(by simp) (by simp)
_ = w i j := by
rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single, Finset.prod_eq_one,
mul_one] <;>
simp +contextual [hw₁]
