MonotoneShellCriterion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Monotone scalar shell reconstruction

This is the analytic reconstruction needed in all dimensions. The measures remain one-dimensional original-distance pushforwards. Decreasing measures may approach their limit arbitrarily slowly; only the approximating shell errors and shell energies are summable.

def OAI.PlanarFalconer.movingShellL1Error line 19
theorem OAI.PlanarFalconer.movingShellL1Error_norm_summable line 23
def OAI.PlanarFalconer.monotoneVariationTerm line 29

theorem OAI.PlanarFalconer.monotone_shell_tests_tendsto line 35

Source documentation

Distributional limit of the shells of the varying monotone measures.

theorem monotone_shell_tests_tendsto (α : ℕ → FiniteMeasure ℝ)
    (τ : FiniteMeasure ℝ) (hα : Antitone (fun n => (α n : Measure ℝ)))
    (hle : ∀ n, (τ : Measure ℝ) ≤ α n)
    (hmass : Tendsto (fun n => ((α n : Measure ℝ) - τ).real univ) atTop (𝓝 0))
    (φ : 𝓢(ℝ, ℂ)) :
    Tendsto (fun M => ∑ j ∈ Finset.range M,
      ∫ x, φ x * kernelMeasureConvolution (sourceShellKernel j) (α j) x) atTop
      (𝓝 (schwartzLpTest 1 φ (∑' n, monotoneVariationTerm α n) +
        ((∫ x, φ x ∂(τ : Measure ℝ)) - schwartzLpTest 1 φ (dyadicLowTerm 0 τ)))) := by
…

Mentions: OAI.PlanarFalconer.kernelMeasureConvolution, OAI.PlanarFalconer.sourceShellKernel, OAI.PlanarFalconer.schwartzLpTest, OAI.PlanarFalconer.monotoneVariationTerm, OAI.PlanarFalconer.dyadicLowTerm

theorem OAI.PlanarFalconer.monotone_shell_criterion line 80

Source documentation

The monotone shell criterion for the positive approximants used in the manuscript. The hypotheses are summability and mass convergence, with no rate imposed on the monotone limit.

theorem monotone_shell_criterion (α τ : ℕ → FiniteMeasure ℝ)
    (μ : FiniteMeasure ℝ) (hα : Antitone (fun n => (α n : Measure ℝ)))
    (hle : ∀ n, (μ : Measure ℝ) ≤ α n)
    (hmass : Tendsto (fun n => ((α n : Measure ℝ) - μ).real univ) atTop (𝓝 0))
    (herror : Summable (fun n => (variationDistance (α n) (τ (n+1))).toReal))
    (hshell : Summable (fun n => ‖shellL2Term τ n‖)) :
    (μ : Measure ℝ) ≪ volume := by
…

Mentions: OAI.PlanarFalconer.variationDistance, OAI.PlanarFalconer.shellL2Term

theorem OAI.PlanarFalconer.monotone_shell_criterion_of_power_bounds line 135

Source documentation

The power-decay form used by the distance measures. Finite initial scales do not affect the conclusion.

theorem monotone_shell_criterion_of_power_bounds (α τ : ℕ → FiniteMeasure ℝ)
    (μ : FiniteMeasure ℝ) (hα : Antitone (fun n => (α n : Measure ℝ)))
    (hle : ∀ n, (μ : Measure ℝ) ≤ α n)
    (hmass : Tendsto (fun n => ((α n : Measure ℝ) - μ).real univ) atTop (𝓝 0))
    {η γ Ctv Cshell : ℝ} (hη : 0 < η) (hγ : 0 < γ)
    (hCtv : 0 < Ctv) (hCshell : 0 < Cshell) (N₀ : ℕ)
    (herror : ∀ n ≥ N₀, variationDistance (α n) (τ (n+1)) ≤
      ENNReal.ofReal (Ctv * (2 : ℝ)^(-η * (n : ℝ))))
    (hshell : ∀ N ≥ N₀, shellEnergy (τ N) N ≤ Cshell * (2 : ℝ)^(-γ * (N : ℝ))) :
    (μ : Measure ℝ) ≪ volume := by
…

Mentions: OAI.PlanarFalconer.variationDistance, OAI.PlanarFalconer.shellEnergy