RemovalSteps #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Removing a stopping time on a rare event #
These are the measure-theoretic Cauchy--Schwarz estimates used in ABK26
e.remove.stop.mean and in the second-moment removal step. If two random
variables agree off a measurable event, their means differ by a square-root
moment term plus the deterministic bound for the stopped variable on that
event.
theorem
Algsuperdiff.Section5.Provider.norm_integral_sub_le_moment_on_event
{Omega : Type u_1}
{E : Type u_2}
[MeasurableSpace Omega]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(mu : MeasureTheory.Measure Omega)
[MeasureTheory.IsProbabilityMeasure mu]
{X Y : Omega → E}
(hX : MeasureTheory.Integrable X mu)
(hY : MeasureTheory.Integrable Y mu)
(hXsq : MeasureTheory.Integrable (fun (omega : Omega) => ‖X omega‖ ^ 2) mu)
{A : Set Omega}
(hA : MeasurableSet A)
(heq : ∀ omega ∉ A, X omega = Y omega)
{B : ℝ}
(hYbound : ∀ᵐ (omega : Omega) ∂mu, omega ∈ A → ‖Y omega‖ ≤ B)
:
Mean removal on a rare event. If X = Y off A, the difference of
their means is controlled by the second moment of X and a pointwise bound on
Y on A. This is the abstract C4 estimate.