DyadicLineRoots.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Only a controlled total length of root cells meets a bounded interval.

theorem OAI.LipschitzHilbert.DyadicLineGrid.index_mono line 15
def OAI.LipschitzHilbert.DyadicLineGrid.rootBand line 20
theorem OAI.LipschitzHilbert.DyadicLineGrid.mem_rootBand_of_mem_interval line 23
theorem OAI.LipschitzHilbert.DyadicLineGrid.interval_subset_rootBand line 27
theorem OAI.LipschitzHilbert.DyadicLineGrid.rootBand_total_length line 35
Source documentation
The roots meeting a bounded interval have total length at most the interval length plus two root lengths.
```
theorem rootBand_total_length (q k : ℤ) {a b : ℝ} (hab : a ≤ b) :
    (∑ j ∈ rootBand q k a b, volume.real (cell q k j)) ≤ b - a + 2 * scale k := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.rootBand, OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.scale
theorem OAI.LipschitzHilbert.DyadicLineGrid.exists_root_scale line 54
Source documentation
A largest scale exists within a factor two of any positive requested length. Applied to 6H, it gives exactly the source range [6H,12H).
```
theorem exists_root_scale {H : ℝ} (hH : 0 < H) :
    ∃ k : ℤ, 6 * H ≤ scale k ∧ scale k < 12 * H := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale