noncomputable def Convexity.iteratedComb {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (cw : ℕ → ℕ → StdSimplex R ℕ) : ℕ → ℕ → StdSimplex R ℕ

Given a doubly-indexed family of convex weights cw : ℕ → ℕ → StdSimplex R ℕ, iteratedComb cw k n is the iterated convex multiplication obtained by combining the weights cw 0 n, cw 1 n, …, cw k n via iConvexComb.

Equations

• Convexity.iteratedComb cw 0 = cw 0
• Convexity.iteratedComb cw k.succ = fun (n : ℕ) => Convexity.iConvexComb (cw (k + 1) n) (Convexity.iteratedComb cw k)

theorem Convexity.iteratedComb_congr {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {cw1 cw2 : ℕ → ℕ → StdSimplex R ℕ} {k : ℕ} (h : ∀ i ≤ k, cw1 i = cw2 i) : iteratedComb cw1 k = iteratedComb cw2 k

theorem Convexity.iteratedComb_weights_eq_zero {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {cw : ℕ → ℕ → StdSimplex R ℕ} (hcw : ∀ (k n m : ℕ), m < n → (cw k n).weights m = 0) (k n m : ℕ) : m < n → (iteratedComb cw k n).weights m = 0

If each cw k n puts no weight on indices m < n, then neither does iteratedComb cw k n.

theorem Convexity.iConvexComb_sum_smul {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} {E : Type u_5} (a : StdSimplex R M) (b : M → StdSimplex R N) (f : N → E) [AddCommGroup E] [Module R E] [IsDomain R] : ((iConvexComb a b).sum fun (m : N) (cwm : R) => cwm • f m) = a.sum fun (i : M) (wi : R) => wi • (b i).sum fun (m : N) (bm : R) => bm • f m

theorem Convexity.eLpNorm_weights_sum_le {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Type u_6} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (w : StdSimplex ℝ ℕ) {h : ℕ → Ω → E} {B : ENNReal} (hB : ∀ (m : ℕ), MeasureTheory.eLpNorm (h m) 1 μ ≤ B) : MeasureTheory.eLpNorm (w.sum fun (m : ℕ) (c : ℝ) => c • h m) 1 μ ≤ B

theorem Convexity.coeFn_sum_smul {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : Type u_6} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p : ENNReal} (s : Finset ℕ) (c : ℕ → ℝ) {h : ℕ → Ω → E} (hmem : ∀ (m : ℕ), MeasureTheory.MemLp (h m) p μ) : ↑↑(∑ m ∈ s, c m • MeasureTheory.MemLp.toLp (h m) ⋯) =ᵐ[μ] ∑ m ∈ s, c m • h m