FilteredShellEndgame.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Final reconstruction for filtered original-distance measures

The two analytic hypotheses below are the restoration estimate and shell summability. The conclusion uses the positive intersection of the original pair filters, with no projection of distances.

theorem OAI.Falconer.positive_volume_of_filtered_shells line 20

Source documentation

The endgame of asm:completion, in a form permitting the decreasing pair filters of the all-dimensional manuscript.

theorem positive_volume_of_filtered_shells {X : Type*} [MeasurableSpace X]
    (f : X → ℝ) (hf : Measurable f) (ρ : Measure X) [IsFiniteMeasure ρ]
    (G : ℕ → Set X) (hG : ∀ n, MeasurableSet (G n)) (hmono : Antitone G)
    (D : Set ℝ) (hD : MeasurableSet D)
    (hcarry : ρ (f ⁻¹' Dᶜ) = 0) (hpositive : 0 < ρ (⋂ n, G n))
    (τ : ℕ → FiniteMeasure ℝ)
    (herror : Summable (fun n =>
      (PlanarFalconer.variationDistance
        ⟨filteredPushforward f ρ (G n), inferInstance⟩ (τ (n+1))).toReal))
    (hshell : Summable (fun n => ‖PlanarFalconer.shellL2Term τ n‖)) :
    0 < volume D := by
…

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