KuratowskiConvexHull.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Convex-hull invariance of the Kuratowski measure

Finite coefficient bins give actual finite covers of a convex hull. Cover pieces are first intersected with the bounded original set; empty pieces are replaced by a singleton from that set. Thus every coordinate has a valid point, including coordinates with zero weight, and one norm bound controls all pieces.

theorem OAI.Tingley.dist_weighted_mixtures_le line 25

Source documentation

A diameter bound and a coefficient l1 bound control finite mixtures.

theorem dist_weighted_mixtures_le {ι : Type*} [Fintype ι]
    (w v : ι → ℝ) (z u : ι → E) (δ R η : ℝ)
    (hw : ∀ i, 0 ≤ w i) (hmass : (∑ i, w i) = 1)
    (hdiam : ∀ i, dist (z i) (u i) ≤ δ)
    (hnorm : ∀ i, ‖u i‖ ≤ R) (hR : 0 ≤ R)
    (hcoeff : (∑ i, |w i - v i|) ≤ η) :
    dist (∑ i, w i • z i) (∑ i, v i • u i) ≤ δ + R * η := by
…

theorem OAI.Tingley.finiteDiameterCover_convexHull_of_norm_le line 61

Source documentation

Construct a finite convex-hull cover with arbitrarily small coefficient error, using a fixed norm bound on the original set.

theorem finiteDiameterCover_convexHull_of_norm_le
    {H : Set E} {δ R η : ℝ}
    (hδ : 0 ≤ δ) (hR : 0 ≤ R) (hη : 0 < η)
    (hnorm : ∀ x ∈ H, ‖x‖ ≤ R) (hc : FiniteDiameterCover H δ) :
    FiniteDiameterCover (convexHull ℝ H) (δ + R * η) := by
…

Mentions: OAI.Tingley.FiniteDiameterCover

theorem OAI.Tingley.chi_convexHull line 125
Source documentation
Convexification preserves the Kuratowski measure of every bounded set.
```
theorem chi_convexHull {H : Set E} (hH : Bornology.IsBounded H) :
    chi (convexHull ℝ H) = chi H := by
…
```
Mentions: OAI.Tingley.chi
theorem OAI.Tingley.chi_closedConvexHull line 143
Source documentation
Taking the closed convex hull also preserves the Kuratowski measure.
```
theorem chi_closedConvexHull {H : Set E} (hH : Bornology.IsBounded H) :
    chi (closure (convexHull ℝ H)) = chi H := by
…
```
Mentions: OAI.Tingley.chi