IteratedPoints.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Actual geometric points of iterated subdivision

Initial vertices are coordinate unit vectors. Every later vertex is the finite barycenter of the nonempty old face that it represents. Simplex membership, exact carriers, and the geometric mesh bound follow from this recursive formula.

def OAI.Tingley.iterDataPoint line 19

Source documentation

The actual geometric realization of every recursively constructed vertex.

def iterDataPoint (I : Type) [Fintype I] [DecidableEq I] :
    (k : ℕ) → (iterData I k).Vertex → I → ℝ
  | 0, v => Pi.single v 1
  | k + 1, v => finiteBarycenter (iterDataPoint I k) v.val

Mentions: OAI.Tingley.iterData, OAI.Tingley.finiteBarycenter

theorem OAI.Tingley.iterDataPoint_zero line 24
theorem OAI.Tingley.iterDataPoint_succ line 27
theorem OAI.Tingley.iterDataPoint_mem_stdSimplex line 32
Source documentation
The recursion produces simplex vectors at every level.
```
theorem iterDataPoint_mem_stdSimplex (I : Type) [Fintype I] [DecidableEq I] :
    ∀ (k : ℕ) (v : (iterData I k).Vertex),
      iterDataPoint I k v ∈ probabilitySimplexSet I := by
…
```
Mentions: OAI.Tingley.iterData, OAI.Tingley.iterDataPoint, OAI.Tingley.probabilitySimplexSet
theorem OAI.Tingley.positiveCarrier_iterDataPoint line 47
Source documentation
The recursively defined combinatorial carrier is exactly the set of strict-positive coordinates of the actual recursive point.
```
theorem positiveCarrier_iterDataPoint (I : Type) [Fintype I] [DecidableEq I] :
    ∀ (k : ℕ) (v : (iterData I k).Vertex),
      positiveCarrier (iterDataPoint I k v) = (iterData I k).carrier v := by
…
```
Mentions: OAI.Tingley.iterData, OAI.Tingley.positiveCarrier, OAI.Tingley.iterDataPoint
abbrev OAI.Tingley.iterPoint line 70
Source documentation
The coordinate form used by the simplex fixed-point argument.
```
abbrev iterPoint (m k : ℕ) : IterVertex m k → Fin (m + 1) → ℝ :=
…
```
Mentions: OAI.Tingley.IterVertex
theorem OAI.Tingley.iterPoint_zero line 73
theorem OAI.Tingley.iterPoint_succ line 76
theorem OAI.Tingley.iterPoint_mem_stdSimplex line 79
theorem OAI.Tingley.positiveCarrier_iterPoint line 83
theorem OAI.Tingley.iterPoint_pos_iff line 88
Source documentation
Exact boundary compatibility of the coordinate labelling rule.
```
theorem iterPoint_pos_iff (m k : ℕ) (v : IterVertex m k) (i : Fin (m + 1)) :
    0 < iterPoint m k v i ↔ i ∈ iterCarrier m k v := by
…
```
Mentions: OAI.Tingley.IterVertex, OAI.Tingley.iterPoint, OAI.Tingley.iterCarrier
theorem OAI.Tingley.norm_sub_le_one_of_mem_stdSimplex line 93
Source documentation
Any two probability vectors have distance at most one in the ambient sup norm.
```
theorem norm_sub_le_one_of_mem_stdSimplex {I : Type*} [Fintype I]
    {x y : I → ℝ} (hx : x ∈ probabilitySimplexSet I) (hy : y ∈ probabilitySimplexSet I) :
    ‖x - y‖ ≤ 1 := by
…
```
Mentions: OAI.Tingley.probabilitySimplexSet
theorem OAI.Tingley.iterPoint_mesh line 107
Source documentation
The mesh of each actual level-k face is bounded by the kth power of the barycentric contraction factor. No face coverage assertion is assumed.
```
theorem iterPoint_mesh (m : ℕ) :
    ∀ (k : ℕ) (s : Finset (IterVertex m k)), s ∈ iterComplex m k →
      ∀ u ∈ s, ∀ v ∈ s,
        ‖iterPoint m k u - iterPoint m k v‖ ≤
          ((m : ℝ) / (m + 1 : ℝ)) ^ k := by
…
```
Mentions: OAI.Tingley.IterVertex, OAI.Tingley.iterComplex, OAI.Tingley.iterPoint