DyadicLineMaximal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Maximal bad intervals exist below a fixed largest dyadic scale.

def OAI.LipschitzHilbert.DyadicLineGrid.MaximalBad line 14
theorem OAI.LipschitzHilbert.DyadicLineGrid.exists_maximalBad line 19
Source documentation
Every bad interval has a maximal bad ancestor before the prescribed largest scale. No choice from an uncountable interval family is involved.
```
theorem exists_maximalBad {q top k j : ℤ} {bad : ℤ → ℤ → Prop}
    (hktop : k ≤ top) (hbad : bad k j) :
    ∃ l i, MaximalBad q top bad l i ∧ cell q k j ⊆ cell q l i := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.MaximalBad, OAI.LipschitzHilbert.DyadicLineGrid.cell
theorem OAI.LipschitzHilbert.DyadicLineGrid.maximalBad_disjoint line 47
Source documentation
Within one bin, distinct maximal bad intervals are disjoint.
```
theorem maximalBad_disjoint {q top k l i j : ℤ} {bad : ℤ → ℤ → Prop}
    (hi : MaximalBad q top bad k i) (hj : MaximalBad q top bad l j)
    (hne : (k, i) ≠ (l, j)) : Disjoint (cell q k i) (cell q l j) := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.MaximalBad, OAI.LipschitzHilbert.DyadicLineGrid.cell