BarycentricSupport.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Supports of finite barycenters

A nonempty average of simplex vectors is a simplex vector. Its strict-positive coordinate support is exactly the union of the supports being averaged. These statements concern the actual finite average and require no geometric coverage assumption.

def OAI.Tingley.positiveCarrier line 25
Source documentation
The coordinates at which a vector is strictly positive.
```
def positiveCarrier (x : ι → ℝ) : Finset ι :=
…
```
theorem OAI.Tingley.mem_positiveCarrier line 28
theorem OAI.Tingley.not_mem_positiveCarrier_iff line 33
Source documentation
Outside the positive carrier, a nonnegative vector has zero coordinates.
```
theorem not_mem_positiveCarrier_iff {x : ι → ℝ} (hx : ∀ i, 0 ≤ x i) (i : ι) :
    i ∉ positiveCarrier x ↔ x i = 0 := by
…
```
Mentions: OAI.Tingley.positiveCarrier
theorem OAI.Tingley.positiveCarrier_subset_iff line 39
Source documentation
Containment in a coordinate face is exactly vanishing outside that face.
```
theorem positiveCarrier_subset_iff {x : ι → ℝ} (hx : ∀ i, 0 ≤ x i)
    (I : Finset ι) :
    positiveCarrier x ⊆ I ↔ ∀ i, i ∉ I → x i = 0 := by
…
```
Mentions: OAI.Tingley.positiveCarrier
theorem OAI.Tingley.finiteBarycenter_apply_nonneg line 55
Source documentation
Finite averaging preserves nonnegative coordinates, including for the empty set.
```
theorem finiteBarycenter_apply_nonneg (p : V → ι → ℝ) (S : Finset V)
    (hp : ∀ v ∈ S, ∀ i, 0 ≤ p v i) (i : ι) :
    0 ≤ finiteBarycenter p S i := by
…
```
Mentions: OAI.Tingley.finiteBarycenter

theorem OAI.Tingley.finiteBarycenter_mem_stdSimplex line 63

Source documentation

A nonempty finite average stays in the standard simplex.

theorem finiteBarycenter_mem_stdSimplex (p : V → ι → ℝ) {S : Finset V}
    (hs : S.Nonempty) (hp : ∀ v ∈ S, p v ∈ probabilitySimplexSet ι) :
    finiteBarycenter p S ∈ probabilitySimplexSet ι := by
…

Mentions: OAI.Tingley.probabilitySimplexSet, OAI.Tingley.finiteBarycenter

theorem OAI.Tingley.finiteBarycenter_pos_iff line 70
Source documentation
A coordinate of a nonempty nonnegative average is positive exactly when one of the averaged coordinates is positive.
```
theorem finiteBarycenter_pos_iff (p : V → ι → ℝ) {S : Finset V}
    (hs : S.Nonempty) (hp : ∀ v ∈ S, ∀ i, 0 ≤ p v i) (i : ι) :
    0 < finiteBarycenter p S i ↔ ∃ v ∈ S, 0 < p v i := by
…
```
Mentions: OAI.Tingley.finiteBarycenter

theorem OAI.Tingley.positiveCarrier_finiteBarycenter line 91

Source documentation

The support of a nonempty nonnegative average is the exact support union.

theorem positiveCarrier_finiteBarycenter (p : V → ι → ℝ) {S : Finset V}
    (hs : S.Nonempty) (hp : ∀ v ∈ S, ∀ i, 0 ≤ p v i) :
    positiveCarrier (finiteBarycenter p S) =
      S.biUnion (fun v => positiveCarrier (p v)) := by
…

Mentions: OAI.Tingley.positiveCarrier, OAI.Tingley.finiteBarycenter

theorem OAI.Tingley.positiveCarrier_finiteBarycenter_subset_iff line 101

Source documentation

The new vertex belongs to an original coordinate face exactly when every averaged vertex belongs to that face.

theorem positiveCarrier_finiteBarycenter_subset_iff (p : V → ι → ℝ)
    {S : Finset V} (hs : S.Nonempty) (hp : ∀ v ∈ S, ∀ i, 0 ≤ p v i)
    (I : Finset ι) :
    positiveCarrier (finiteBarycenter p S) ⊆ I ↔
      ∀ v ∈ S, positiveCarrier (p v) ⊆ I := by
…

Mentions: OAI.Tingley.positiveCarrier, OAI.Tingley.finiteBarycenter

theorem OAI.Tingley.positiveCarrier_nonempty_of_mem_stdSimplex line 110
Source documentation
A simplex vector has a positive coordinate because its total mass is one.
```
theorem positiveCarrier_nonempty_of_mem_stdSimplex {x : ι → ℝ}
    (hx : x ∈ probabilitySimplexSet ι) : (positiveCarrier x).Nonempty := by
…
```
Mentions: OAI.Tingley.probabilitySimplexSet, OAI.Tingley.positiveCarrier