PositiveConvexFace.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Positive combinations in a common support face

A norm-bounded functional that is one on a strictly positive barycenter is one on every vertex. The resulting simultaneous support keeps the enlarged convex hull in the unit sphere. For an infinite sequence, finite-prefix hull containment passes to a closed ambient set without choosing a common support for the entire sequence.

theorem OAI.Tingley.eq_one_of_positive_weighted_sum line 28
theorem OAI.Tingley.support_eq_one_of_positive_sum line 53
theorem OAI.Tingley.SupportAt.eq_one_of_positive_sum line 62
def OAI.Tingley.supportFace line 73
Source documentation
The closed unit ball cut by the level-one hyperplane of one functional.
```
def supportFace (φ : X →L[ℝ] ℝ) : Set X :=
…
```
theorem OAI.Tingley.convex_supportFace line 76
theorem OAI.Tingley.isClosed_supportFace line 88
theorem OAI.Tingley.supportFace_subset_sphere line 92
theorem OAI.Tingley.convexHull_subset_supportFace line 97
theorem OAI.Tingley.closure_convexHull_subset_supportFace line 102
theorem OAI.Tingley.enlarged_convexHull_in_supportFace line 111

theorem OAI.Tingley.convexHull_insert_subset_of_common_support line 129

Source documentation

The actual geometric propagation rule can now be applied to every new hull point.

theorem convexHull_insert_subset_of_common_support (φ : X →L[ℝ] ℝ) (hφ : ‖φ‖ ≤ 1)
    (weights : ι → ℝ) (v : ι → X) (w : X) (E : Set X)
    (hpos : ∀ i, 0 < weights i) (hsum : ∑ i, weights i = 1)
    (hv : ∀ i, ‖v i‖ = 1) (hw : ‖w‖ = 1)
    (ha : φ (∑ i, weights i • v i) = 1) (hwφ : φ w = 1)
    (hprop : ∀ x, ‖x‖ = 1 → φ x = 1 → x ∈ E) :
    convexHull ℝ (insert w (Set.range v)) ⊆ E := by
…

def OAI.Tingley.prefixVertices line 143
Source documentation
The actual values at indices zero through n; repeated values are allowed.
```
def prefixVertices (v : ℕ → X) (n : ℕ) : Set X := v '' {i : ℕ | i ≤ n}
…
```
theorem OAI.Tingley.prefixVertices_mono line 146
theorem OAI.Tingley.prefixVertices_subset_range line 152
theorem OAI.Tingley.prefixVertices_eq_range_fin line 158
theorem OAI.Tingley.convexHull_range_eq_iUnion_prefix line 167
theorem OAI.Tingley.closure_convexHull_range_subset_of_prefix line 183
theorem OAI.Tingley.closed_convex_extremal_hull line 191