EqualWeightAverages.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Equal-weight approximation of closed convex hulls

Natural multiplicities approximate any finite convex combination: round scaled weights down, normalize their total, and repeat the corresponding points. No compactness or dimension restriction on the normed space is used.

theorem OAI.KadisonKastler.exists_equalWeightAverage_of_natWeights line 26

Source documentation

A natural-weight mean is literally an equal-weight mean with repetitions.

theorem exists_equalWeightAverage_of_natWeights {ι : Type*} [Fintype ι]
    (c : ι → ℕ) (f : ι → E) (hc : 0 < ∑ i, c i) :
    ∃ n : ℕ, 0 < n ∧ ∃ g : Fin n → E,
      (∀ j, g j ∈ Set.range f) ∧
      (n : ℝ)⁻¹ • ∑ j, g j = ((∑ i, c i : ℕ) : ℝ)⁻¹ • ∑ i, (c i : ℝ) • f i := by
…

theorem OAI.KadisonKastler.rounded_mean_eq line 48

theorem OAI.KadisonKastler.exists_equalWeightAverage_of_convexCombination line 66

Source documentation

Finite convex combinations can be approximated by means with repeated points.

theorem exists_equalWeightAverage_of_convexCombination {ι : Type*} [Fintype ι]
    (w : ι → ℝ) (f : ι → E) (hw : ∀ i, 0 ≤ w i) (hw1 : ∑ i, w i = 1)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ n : ℕ, 0 < n ∧ ∃ g : Fin n → E,
      (∀ j, g j ∈ Set.range f) ∧
      ‖(n : ℝ)⁻¹ • ∑ j, g j - ∑ i, w i • f i‖ < ε := by
…

theorem OAI.KadisonKastler.exists_equalWeightAverage_of_mem_convexHull line 103

Source documentation

Equal-weight means of points of a set are dense in its convex hull.

theorem exists_equalWeightAverage_of_mem_convexHull {S : Set E} {z : E}
    (hz : z ∈ convexHull ℝ S) {ε : ℝ} (hε : 0 < ε) :
    ∃ n : ℕ, 0 < n ∧ ∃ f : Fin n → E,
      (∀ i, f i ∈ S) ∧ ‖(n : ℝ)⁻¹ • ∑ i, f i - z‖ < ε := by
…

theorem OAI.KadisonKastler.exists_equalWeightAverage_of_mem_closedConvexHull line 119

Source documentation

Every point of the closed convex hull is approximated by a finite nonempty equal-weight average of points of the original set.

theorem exists_equalWeightAverage_of_mem_closedConvexHull {S : Set E} {z : E}
    (hz : z ∈ closure (convexHull ℝ S)) {ε : ℝ} (hε : 0 < ε) :
    ∃ n : ℕ, 0 < n ∧ ∃ f : Fin n → E,
      (∀ i, f i ∈ S) ∧ ‖(n : ℝ)⁻¹ • ∑ i, f i - z‖ < ε := by
…