DyadicMassReindex.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Converting outward Gaussian shells to inward dyadic mass envelopes

theorem OAI.RegularPointCoordinates.outward_radius_eq_ancestor line 17
Source documentation
The ancestor radius in an outward shell is exactly the corresponding fixed-root dyadic radius.
```
theorem outward_radius_eq_ancestor {s R : ℝ} {N j : ℕ}
    (hR : (2 : ℝ) ^ N * s = R) (hj : j ≤ N) :
    (2 : ℝ) ^ (N - j) * s = R / (2 : ℝ) ^ j := by
…
```

theorem OAI.RegularPointCoordinates.outward_sum_eq_inward_sum line 28

Source documentation

Reversing the finite shell sum produces the geometric convolution of the actual masses at the fixed-root dyadic radii.

theorem outward_sum_eq_inward_sum (f : ℝ → ℝ) (β : ℝ) {s R : ℝ} (N : ℕ)
    (hR : (2 : ℝ) ^ N * s = R) :
    (∑ j ∈ Finset.range (N + 1), β ^ j * f (2 ^ j * s)) =
      ∑ j ∈ Finset.range (N + 1), β ^ (N - j) * f (R / 2 ^ j) := by
…

theorem OAI.RegularPointCoordinates.dyadic_square_le_three_quarters line 41
Source documentation
The scalar regularizer is also bounded by the same geometric background envelope when the outer radius is fixed.
```
theorem dyadic_square_le_three_quarters {s R : ℝ} (hs : 0 ≤ s) (N : ℕ)
    (hR : (2 : ℝ) ^ N * s = R) :
    s ^ 2 ≤ R ^ 2 * (3 / 4 : ℝ) ^ N := by
…
```