MonotoneShellVariation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The monotone-variation step in the shell reconstruction

The proof of the manuscript's asm:monotone-shell uses summable positive measure increments ζₙ = αₙ − αₙ₊₁. After interchanging a finite sum of Fourier bands with these increments, the correction is ∑' n, (Q (min n M) - Qbase) (ζ n). It converges in any Banach space by the uniform bounds for the low-pass operators. No rate of convergence of αₙ to α∞ is required.

theorem OAI.Falconer.summable_antitone_mass_increments line 26
Source documentation
Positive increments of a decreasing, nonnegative sequence are summable. For the shell lemma, m n is the total mass of α n.
```
theorem summable_antitone_mass_increments (m : ℕ → ℝ)
    (hm : Antitone m) (hpos : ∀ n, 0 ≤ m n) :
    Summable (fun n => m n - m (n + 1)) := by
…
```
theorem OAI.Falconer.lowpass_difference_bound line 44

theorem OAI.Falconer.sum_bands_before_increment line 57

Source documentation

Finite telescoping of the low-pass differences at one fixed increment.

theorem sum_bands_before_increment (Q : ℕ → E →L[ℝ] F) (z : E) (n M : ℕ) :
    (∑ j ∈ Finset.range M, if j ≤ n then (Q (j + 1) - Q j) z else 0) =
      (Q (min (n + 1) M) - Q 0) z := by
…

theorem OAI.Falconer.finite_band_variation_identity line 73

Source documentation

The finite-band identity of the monotone shell argument. The outer band sum is finite; the inner increment sum is absolutely convergent.

theorem finite_band_variation_identity [CompleteSpace E]
    (Q : ℕ → E →L[ℝ] F) (z : ℕ → E)
    (hz : Summable (fun n => ‖z n‖)) (M : ℕ) :
    (∑ j ∈ Finset.range M,
      (Q (j + 1) - Q j) (∑' n, if j ≤ n then z n else 0)) =
    ∑' n, (Q (min (n + 1) M) - Q 0) (z n) := by
…

theorem OAI.Falconer.summable_lowpass_variation line 99

Source documentation

Absolute convergence of the variation correction from summable increments.

theorem summable_lowpass_variation (Q : ℕ → E →L[ℝ] F) (Qbase : E →L[ℝ] F)
    {C : ℝ} (hQ : ∀ n, ‖Q n‖ ≤ C) (hbase : ‖Qbase‖ ≤ C)
    (z : ℕ → E) (hz : Summable (fun n => ‖z n‖)) :
    Summable (fun n => (Q n - Qbase) (z n)) := by
…

theorem OAI.Falconer.truncated_lowpass_variation_tendsto line 108

Source documentation

The triangular partial corrections converge in norm. This is precisely the limit used after the finite-band identity in asm:variation-tail.

theorem truncated_lowpass_variation_tendsto
    (Q : ℕ → E →L[ℝ] F) (Qbase : E →L[ℝ] F)
    {C : ℝ} (hQ : ∀ n, ‖Q n‖ ≤ C) (hbase : ‖Qbase‖ ≤ C)
    (z : ℕ → E) (hz : Summable (fun n => ‖z n‖)) :
    Tendsto (fun M : ℕ => ∑' n, (Q (min n M) - Qbase) (z n)) atTop
      (𝓝 (∑' n, (Q n - Qbase) (z n))) := by
…

theorem OAI.Falconer.finite_band_variation_tendsto line 124

Source documentation

The finite sum of bands applied to the decreasing tails has a norm limit, with no quantitative assumption on the rate at which those tails vanish.

theorem finite_band_variation_tendsto [CompleteSpace E]
    (Q : ℕ → E →L[ℝ] F) {C : ℝ} (hQ : ∀ n, ‖Q n‖ ≤ C)
    (z : ℕ → E) (hz : Summable (fun n => ‖z n‖)) :
    Tendsto (fun M => ∑ j ∈ Finset.range M,
      (Q (j + 1) - Q j) (∑' n, if j ≤ n then z n else 0)) atTop
      (𝓝 (∑' n, (Q (n + 1) - Q 0) (z n))) := by
…