ReachedMasks.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing reached masks after passing to positive energy

A reached anchor mask is spatially constant on its descendant cell. It can therefore be taken outside that endpoint transform. Its bounded angular factor is removed only from the positive independent energy.

theorem OAI.Falconer.endpointTransform_angular_factor line 17
theorem OAI.Falconer.DyadicCube.endpointTransform_reached_factor line 31
theorem OAI.Falconer.sphereMoment_factor_le line 44

theorem OAI.Falconer.independentAngularEnergy_remove_factors line 69

Source documentation

Removing two reached angular factors costs only their squared sup norms. Every unreached spatial mask remains inside its endpoint transform.

theorem independentAngularEnergy_remove_factors {d : ℕ} (a v : ℝ) (Ψ : ℝ → ℝ)
    [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure v Ψ)]
    (U V : ℝ × Sphere d → ℂ) (hU : Measurable U) (hV : Measurable V)
    (m n : Sphere d → ℂ) (hm : Measurable m) (hn : Measurable n)
    {B C D E : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 0 ≤ D) (hE : 0 ≤ E)
    (hmB : ∀ w, ‖m w‖ ≤ B) (hnC : ∀ w, ‖n w‖ ≤ C)
    (hUD : ∀ z, ‖U z‖ ≤ D) (hVE : ∀ z, ‖V z‖ ≤ E) :
    independentAngularEnergy a v Ψ (fun z => m z.2 * U z) (fun z => n z.2 * V z) ≤
      (B^2*C^2) * independentAngularEnergy a v Ψ U V := by
…

Mentions: OAI.PlanarFalconer.sourceAngularShellMeasure, OAI.Falconer.Sphere, OAI.Falconer.independentAngularEnergy