CellDyadicScales.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Comparing lattice generations with dyadic descendants

One lattice generation contracts the radius by 64, hence corresponds to six dyadic halvings. Dividing a dyadic depth by six separates a whole lattice generation from a bounded remainder, giving uniform comparisons of the two scales.

theorem OAI.RieszRectifiability.latticeRadius_eq_descendantRadius line 20
Source documentation
Advancing t lattice generations is exactly 6 * t dyadic halvings.
```
theorem latticeRadius_eq_descendantRadius (R : ℝ) (k t : ℕ) :
    latticeRadius R (k + t) = descendantRadius (latticeRadius R k) (6 * t) := by
…
```
Mentions: OAI.RieszRectifiability.latticeRadius, OAI.RieszRectifiability.descendantRadius
theorem OAI.RieszRectifiability.descendantRadius_cell_remainder line 27
Source documentation
The remainder modulo six records the dyadic contraction within a lattice generation.
```
theorem descendantRadius_cell_remainder (R H : ℝ) (k j : ℕ) :
    descendantRadius (H * latticeRadius R k) j =
      H * latticeRadius R (k + j / 6) / (2 : ℝ) ^ (j % 6) := by
…
```
Mentions: OAI.RieszRectifiability.descendantRadius, OAI.RieszRectifiability.latticeRadius

theorem OAI.RieszRectifiability.descendantRadius_cell_bounds line 38

Source documentation

Positive dyadic descendant radii lie between fixed multiples of the matching lattice scale.

theorem descendantRadius_cell_bounds (R H : ℝ) (hR : 0 < R) (hH : 0 < H) (k j : ℕ) :
    (H / 64) * latticeRadius R (k + j / 6) ≤ descendantRadius (H * latticeRadius R k) j ∧
      descendantRadius (H * latticeRadius R k) j ≤ H * latticeRadius R (k + j / 6) := by
…

Mentions: OAI.RieszRectifiability.latticeRadius, OAI.RieszRectifiability.descendantRadius