SourceShortDyadicBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The short-tree estimates are summed over dyadic lengths with constants independent of the number of retained scales.

theorem OAI.LipschitzHilbert.SourceWhitney.finite_dyadic_length_sum line 14

Source documentation

Any finite selection of dyadic lengths below R has sum at most 2R.

theorem finite_dyadic_length_sum (L R : ℝ) (hR : 0≤R)
    (S : Finset ℕ) (hbound : ∀ j∈S, L/(2:ℝ)^j≤R) :
    (∑ j∈S, L/(2:ℝ)^j) ≤ 2*R := by
…

theorem OAI.LipschitzHilbert.SourceWhitney.finite_dyadic_decay_sum line 56

Source documentation

The far-strip gain survives summation of every selected length.

theorem finite_dyadic_decay_sum (L R r : ℝ) (hL : 0<L) (hR : 0≤R) (hr : 0<r)
    (S : Finset ℕ) (hbound : ∀ j∈S, L/(2:ℝ)^j≤R) :
    (∑ j∈S, (L/(2:ℝ)^j)*((L/(2:ℝ)^j)/r)^2) ≤ 2*R*(R/r)^2 := by
…

theorem OAI.LipschitzHilbert.SourceWhitney.fin_short_dyadic_length_sum line 68
Source documentation
The same short-length sum in the finite scale indexing used by packets.
```
theorem fin_short_dyadic_length_sum (N : ℕ) (L R : ℝ) (hR : 0≤R) :
    (∑ j : Fin N, if L/(2:ℝ)^j.val≤R then L/(2:ℝ)^j.val else 0) ≤ 2*R := by
…
```

theorem OAI.LipschitzHilbert.SourceWhitney.fin_dyadic_decay_sum line 77

Source documentation

All packet lengths together retain a quadratic far-strip gain.

theorem fin_dyadic_decay_sum (N : ℕ) (L r : ℝ) (hL : 0<L) (hr : 0<r) :
    (∑ j : Fin N, (L/(2:ℝ)^j.val)*((L/(2:ℝ)^j.val)/r)^2) ≤ 2*L*(L/r)^2 := by
…

theorem OAI.LipschitzHilbert.SourceWhitney.finite_large_scale_square_sum line 86
Source documentation
The squared ratios from a fixed length to larger dyadic lengths have a uniformly bounded sum, also when the dyadic levels are negative.
```
theorem finite_large_scale_square_sum (L : ℝ) (hL : 0<L)
    (S : Finset ℤ) (hscale : ∀ k∈S, L≤DyadicLineGrid.scale k) :
    (∑ k∈S, (L/DyadicLineGrid.scale k)^2) ≤ 2 := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale