SourceThreeGridCover.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A literal three-grid covering lemma for the nested alternating one-third grids. It supplies the interval comparison in the maximal kernel estimate.

theorem OAI.LipschitzHilbert.DyadicLineGrid.shift_signed_third line 12
theorem OAI.LipschitzHilbert.DyadicLineGrid.signed_third_in_range line 15
theorem OAI.LipschitzHilbert.DyadicLineGrid.exists_three_grid_cover line 21
Source documentation
A closed interval of radius less than one sixth of a grid cell fits in a cell of one of the three fixed nested grids.
```
theorem exists_three_grid_cover (k : ℤ) (c r : ℝ) (_hr : 0≤r)
    (hsmall : 6*r<scale k) :
    ∃ q∈Finset.Icc (-1) 1, ∃ j : ℤ, Icc (c-r) (c+r)⊆cell q k j := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale, OAI.LipschitzHilbert.DyadicLineGrid.cell
theorem OAI.LipschitzHilbert.DyadicLineGrid.exists_comparable_three_grid_cover line 71
Source documentation
The covering cell has length at most six times the interval length.
```
theorem exists_comparable_three_grid_cover (c r : ℝ) (hr : 0<r) :
    ∃ q∈Finset.Icc (-1) 1, ∃ k j : ℤ,
      Icc (c-r) (c+r)⊆cell q k j ∧ scale k≤12*r := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.scale