SourceWhitneyIntervals.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Horizontal Whitney cells for the ordinary tree estimate. An allowed cell has no tile of shorter length whose center meets its triple. A maximal allowed cell obtains its concrete witness from its parent.

def OAI.LipschitzHilbert.SourceWhitney.center line 14
def OAI.LipschitzHilbert.SourceWhitney.Allowed line 16
def OAI.LipschitzHilbert.SourceWhitney.Whitney line 19
theorem OAI.LipschitzHilbert.SourceWhitney.point_center_bound line 22
theorem OAI.LipschitzHilbert.SourceWhitney.center_parent_bound line 32
theorem OAI.LipschitzHilbert.SourceWhitney.allowed_of_parent line 45
theorem OAI.LipschitzHilbert.SourceWhitney.short_tile_separation line 57
theorem OAI.LipschitzHilbert.SourceWhitney.parent_witness line 66
theorem OAI.LipschitzHilbert.SourceWhitney.parent_index line 82
Source documentation
The index of a point at the next scale is exactly its parent index.
```
theorem parent_index (k : ℤ) (z : ℝ) :
    parent 0 k (index 0 k z) = index 0 (k+1) z :=
…
```

theorem OAI.LipschitzHilbert.SourceWhitney.allowed_at_point_mono line 88

Source documentation

Being allowed passes from a larger cell to every smaller cell it meets.

theorem allowed_at_point_mono {ι : Type*} (tiles : Finset ι) (x ell : ι → ℝ)
    {k l : ℤ} (hkl : k ≤ l) (z : ℝ)
    (h : Allowed tiles x ell l (index 0 l z)) :
    Allowed tiles x ell k (index 0 k z) := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Allowed

theorem OAI.LipschitzHilbert.SourceWhitney.whitney_disjoint line 101

Source documentation

Distinct maximal allowed cells are disjoint at all scales.

theorem whitney_disjoint {ι : Type*} (tiles : Finset ι) (x ell : ι → ℝ)
    {k l i j : ℤ} (hi : Whitney tiles x ell k i)
    (hj : Whitney tiles x ell l j) (hne : (k,i) ≠ (l,j)) :
    Disjoint (cell 0 k i) (cell 0 l j) := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney

theorem OAI.LipschitzHilbert.SourceWhitney.scale_mono line 125

theorem OAI.LipschitzHilbert.SourceWhitney.exists_small_scale line 129

Source documentation

A finite family of positive tile lengths has a common strictly smaller scale.

theorem exists_small_scale {ι : Type*} (tiles : Finset ι) (ell : ι → ℝ)
    (hpos : ∀ i ∈ tiles, 0 < ell i) :
    ∃ k : ℤ, ∀ i ∈ tiles, scale k < ell i := by
…

theorem OAI.LipschitzHilbert.SourceWhitney.exists_whitney_cover line 147
Source documentation
Every real point lies in a maximal allowed interval. The upper scale is obtained from one actual tile, rather than an assumed global cutoff.
```
theorem exists_whitney_cover {ι : Type*} (tiles : Finset ι) (x ell : ι → ℝ)
    (hne : tiles.Nonempty) (hpos : ∀ i ∈ tiles, 0 < ell i) (z : ℝ) :
    ∃ k j, Whitney tiles x ell k j ∧ z ∈ cell 0 k j := by
…
```
Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney