MonotoneLowpass.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Low-pass terms for the decreasing-measure shell argument

The Schwartz Fourier cutoffs represent the low-pass terms of shell reconstruction. The L¹ bound is uniform in the dyadic cutoff index.

theorem OAI.PlanarFalconer.sourceShellLowpass_compact line 17
def OAI.PlanarFalconer.dyadicLowpassSchwartz line 25
theorem OAI.PlanarFalconer.dyadicLowpassSchwartz_apply line 29
def OAI.PlanarFalconer.dyadicLowKernel line 32
theorem OAI.PlanarFalconer.dyadicLowKernel_dilate line 35
theorem OAI.PlanarFalconer.dyadicLowKernel_integrable line 46
theorem OAI.PlanarFalconer.dyadicLowKernel_continuous line 49
theorem OAI.PlanarFalconer.dyadicLowKernel_uniform_L1 line 52
def OAI.PlanarFalconer.dyadicLowTerm line 61
theorem OAI.PlanarFalconer.dyadicLowTerm_norm_le line 67
theorem OAI.PlanarFalconer.dyadicLowTerm_test line 77

theorem OAI.PlanarFalconer.summable_dyadicLowTerm_decrements line 87

Source documentation

Uniform low-pass bounds make the variation series absolutely convergent. The increments here are the actual positive differences of finite measures.

theorem summable_dyadicLowTerm_decrements (α : ℕ → FiniteMeasure ℝ)
    (hα : Antitone (fun n => (α n : Measure ℝ))) :
    Summable (fun n => ‖dyadicLowTerm (n + 1)
      ⟨(α n : Measure ℝ) - α (n + 1), inferInstance⟩ -
      dyadicLowTerm 0 ⟨(α n : Measure ℝ) - α (n + 1), inferInstance⟩‖) := by
…

Mentions: OAI.PlanarFalconer.dyadicLowTerm

theorem OAI.PlanarFalconer.dyadicLowTerm_add line 112
Source documentation
Convolution preserves sums of finite positive measures in L¹.
```
theorem dyadicLowTerm_add (n : ℕ) (μ ν : FiniteMeasure ℝ) :
    dyadicLowTerm n (μ + ν) = dyadicLowTerm n μ + dyadicLowTerm n ν := by
…
```
Mentions: OAI.PlanarFalconer.dyadicLowTerm

theorem OAI.PlanarFalconer.dyadicLowTerm_sub_of_le line 140

Source documentation

The positive measure difference is sent to the difference of low-pass terms.

theorem dyadicLowTerm_sub_of_le (n : ℕ) (μ ν : FiniteMeasure ℝ)
    (h : (ν : Measure ℝ) ≤ μ) :
    dyadicLowTerm n ⟨(μ : Measure ℝ) - ν, inferInstance⟩ =
      dyadicLowTerm n μ - dyadicLowTerm n ν := by
…

Mentions: OAI.PlanarFalconer.dyadicLowTerm

theorem OAI.PlanarFalconer.dyadicLowTerm_summation_by_parts line 154

Source documentation

Finite summation by parts in the actual L¹ space of low-pass convolutions. The final term is a single low-pass difference applied to the remaining tail.

theorem dyadicLowTerm_summation_by_parts (α : ℕ → FiniteMeasure ℝ)
    (hα : Antitone (fun n => (α n : Measure ℝ))) (M : ℕ) :
    (∑ j ∈ Finset.range M, (dyadicLowTerm (j + 1) (α j) - dyadicLowTerm j (α j))) =
      (∑ n ∈ Finset.range M,
        (dyadicLowTerm (n + 1) ⟨(α n : Measure ℝ) - α (n + 1), inferInstance⟩ -
        dyadicLowTerm 0 ⟨(α n : Measure ℝ) - α (n + 1), inferInstance⟩)) +
      (dyadicLowTerm M (α M) - dyadicLowTerm 0 (α M)) := by
…

Mentions: OAI.PlanarFalconer.dyadicLowTerm

theorem OAI.PlanarFalconer.dyadicLowTerm_test_tendsto line 175
Source documentation
The dyadic cutoffs converge to the original measure in Schwartz tests.
```
theorem dyadicLowTerm_test_tendsto (τ : FiniteMeasure ℝ) (φ : 𝓢(ℝ, ℂ)) :
    Tendsto (fun n => schwartzLpTest 1 φ (dyadicLowTerm n τ)) atTop
      (𝓝 (∫ x, φ x ∂(τ : Measure ℝ))) := by
…
```
Mentions: OAI.PlanarFalconer.schwartzLpTest, OAI.PlanarFalconer.dyadicLowTerm
theorem OAI.PlanarFalconer.dyadicLowTerm_band_test line 187
Source documentation
The difference of adjacent cutoff tests is exactly the existing shell kernel test, with no change to the Fourier convention.
```
theorem dyadicLowTerm_band_test (n : ℕ) (τ : FiniteMeasure ℝ) (φ : 𝓢(ℝ, ℂ)) :
    schwartzLpTest 1 φ (dyadicLowTerm (n + 1) τ - dyadicLowTerm n τ) =
      ∫ x, φ x * kernelMeasureConvolution (sourceShellKernel n) τ x := by
…
```
Mentions: OAI.PlanarFalconer.schwartzLpTest, OAI.PlanarFalconer.dyadicLowTerm, OAI.PlanarFalconer.kernelMeasureConvolution, OAI.PlanarFalconer.sourceShellKernel

theorem OAI.PlanarFalconer.dyadicLowTerm_tail_tendsto line 204

Source documentation

A decreasing family's remaining tail vanishes after any varying cutoff, provided only that its mass tends to zero.

theorem dyadicLowTerm_tail_tendsto (α : ℕ → FiniteMeasure ℝ) (τ : FiniteMeasure ℝ)
    (hle : ∀ n, (τ : Measure ℝ) ≤ α n)
    (hmass : Tendsto (fun n => ((α n : Measure ℝ) - τ).real univ) atTop (𝓝 0))
    (k : ℕ → ℕ) :
    Tendsto (fun n => dyadicLowTerm (k n) (α n) - dyadicLowTerm (k n) τ)
      atTop (𝓝 0) := by
…

Mentions: OAI.PlanarFalconer.dyadicLowTerm