DyadicCenters.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual dyadic centers as one translated integer grid

The graph packing estimates apply to centers of descendants of the original parent cube. Their integer labels and common translation are identified exactly, in every ambient dimension.

def OAI.Falconer.dyadicCode line 17
theorem OAI.Falconer.dyadicCode_bounds line 21
theorem OAI.Falconer.DyadicCube.descendant_origin line 29
theorem OAI.Falconer.DyadicCube.descendant_center line 45
theorem OAI.Falconer.dyadicCode_injective_at_depth line 54
theorem OAI.Falconer.DyadicCube.descendant_center_grid line 70
Source documentation
The translation includes half a child side. Its contribution cancels in every displacement used by the retained graph.
```
theorem DyadicCube.descendant_center_grid {d n : ℕ} (Q : DyadicCube d)
    (p : List (Fin d → Bool)) (hp : p.length = n) :
    (Q.descendant p).center =
      WithLp.toLp 2 (fun i => Q.origin i + (Q.side / (2 : ℝ)^n)/2) +
        scaledGridPoint ((2 : ℝ)^n / Q.side) (dyadicCode p) := by
…
```
Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.DyadicCube.center, OAI.Falconer.scaledGridPoint, OAI.Falconer.dyadicCode
theorem OAI.Falconer.DyadicCube.center_sub_eq_grid_sub line 80