DyadicLineCover.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform interval cover by the nested one-third dyadic grids.

theorem OAI.LipschitzHilbert.DyadicLineGrid.unit_interval_cover line 14

Source documentation

The elementary one-third covering step at a fixed scale.

theorem unit_interval_cover {a b δ : ℝ} (hδ0 : 1 / 3 ≤ δ) (hδ1 : δ ≤ 2 / 3)
    (hlen : b - a < 1 / 3) :
    (∃ j : ℤ, Icc a b ⊆ Ico (j : ℝ) (j + 1)) ∨
      ∃ j : ℤ, Icc a b ⊆ Ico ((j : ℝ) + δ) (j + 1 + δ) := by
…

theorem OAI.LipschitzHilbert.DyadicLineGrid.fixed_scale_interval_cover line 33
Source documentation
Each interval shorter than one third of a grid cell fits in one cell of the ordinary or alternating one-third grid.
```
theorem fixed_scale_interval_cover (k : ℤ) {a b : ℝ} (hlen : b - a < scale k / 3) :
    ∃ q ∈ ({0, 1} : Finset ℤ), ∃ j : ℤ, Icc a b ⊆ cell q k j := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale, OAI.LipschitzHilbert.DyadicLineGrid.cell
theorem OAI.LipschitzHilbert.DyadicLineGrid.interval_cover line 87
Source documentation
A positive-length interval is contained in a dyadic interval of length at most six times its own, with one of two fixed nested grids.
```
theorem interval_cover {a b : ℝ} (hab : a < b) :
    ∃ q ∈ ({0, 1} : Finset ℤ), ∃ k j : ℤ,
      Icc a b ⊆ cell q k j ∧ scale k ≤ 6 * (b - a) := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.scale