@[implicit_reducible]

instance Convexity.StdSimplex.instFunLike {R : Type u_1} [PartialOrder R] [Semiring R] {M : Type u_2} : FunLike (StdSimplex R M) M R

Equations

• Convexity.StdSimplex.instFunLike = { coe := fun (s : Convexity.StdSimplex R M) => s.weights.toFun, coe_injective := ⋯ }

noncomputable def Convexity.StdSimplex.bind {R : Type u_1} [PartialOrder R] [Semiring R] {M : Type u_2} {N : Type u_3} [IsStrictOrderedRing R] (a : StdSimplex R M) (b : M → StdSimplex R N) : StdSimplex R N

Given convex weights a : StdSimplex R ι and a family of convex weights b : ι → StdSimplex R ι', StdSimplex.bind a b is the convex combination of the b k, weighted by a, defined as monadic bind.

Equations

• a.bind b = (Convexity.StdSimplex.map b a).join

@[simp]

theorem Convexity.StdSimplex.bind_single {R : Type u_1} [PartialOrder R] [Semiring R] {M : Type u_2} {N : Type u_3} [IsStrictOrderedRing R] (b : M → StdSimplex R N) (i : M) : (single i).bind b = b i

@[simp]

theorem Convexity.StdSimplex.bind_const {R : Type u_1} [PartialOrder R] [Semiring R] {M : Type u_2} {N : Type u_3} [IsStrictOrderedRing R] (a : StdSimplex R M) (c : StdSimplex R N) : (a.bind fun (x : M) => c) = c

theorem Convexity.StdSimplex.weights_bind {R : Type u_1} [PartialOrder R] [Semiring R] {M : Type u_2} {N : Type u_3} [IsStrictOrderedRing R] (a : StdSimplex R M) (b : M → StdSimplex R N) : ⇑(a.bind b).weights = fun (m : N) => ∑ k ∈ a.weights.support, a.weights k * (b k).weights m

theorem Convexity.StdSimplex.support_subset_support_bind {R : Type u_1} [PartialOrder R] [Semiring R] {M : Type u_2} {N : Type u_3} [IsStrictOrderedRing R] {a : StdSimplex R M} (b : M → StdSimplex R N) {i : M} (hi : i ∈ a.weights.support) : (b i).weights.support ⊆ (a.bind b).weights.support

noncomputable def Convexity.StdSimplex.iteratedBind {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 ℕ, iteratedBind cw k n is the iterated convex multiplication obtained by combining the weights cw 0 n, cw 1 n, …, cw k n via StdSimplex.bind.

Equations

• Convexity.StdSimplex.iteratedBind cw 0 = cw 0
• Convexity.StdSimplex.iteratedBind cw k.succ = fun (n : ℕ) => (cw (k + 1) n).bind (Convexity.StdSimplex.iteratedBind cw k)

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

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

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

theorem Convexity.StdSimplex.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