Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaTailControl

Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaTailControl #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

The control measure for the one-ball good-λ estimate #

The local stopping-ball estimate has two lower-level weighted tails on its right-hand side. This file packages precisely their sum as a measure. The evaluation lemmas below are deliberately stated on measurable sets, which is what the Vitali assembly consumes; no measurability is hidden in the definition of the restricted measures.

source
noncomputable def HCPolySupport.CubeCalderonZygmund.oneStoppingBallTailControl {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (eps level : ℝ) :
MeasureTheory.Measure (Vec d)

The two lower-level square-weighted tails which control a stopping ball.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.CubeCalderonZygmund.oneStoppingBallTailControl_apply {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (eps level : ℝ) {B : Set (Vec d)} (hB : MeasurableSet B) :
    (oneStoppingBallTailControl f g eps level) B = (sqWeightedMeasure f MeasureTheory.volume) ({x : Vec d | level / 2 < ‖f x‖} ∩ B) + ENNReal.ofReal (eps⁻¹ ^ 2) * (sqWeightedMeasure g MeasureTheory.volume) ({x : Vec d | eps * level / 2 < ‖g x‖} ∩ B)

    Evaluation of the one-ball control measure on a measurable set. The intersection order agrees exactly with the lower tails in sqWeightedMeasure_oneStoppingBall_le.

    source
    theorem HCPolySupport.CubeCalderonZygmund.oneStoppingBallTailControl_apply_ambient {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) (eps level : ℝ) {U : Set (Vec d)} (hU : MeasurableSet U) :
    (oneStoppingBallTailControl f g eps level) U = (sqWeightedMeasure f MeasureTheory.volume) ({x : Vec d | level / 2 < ‖f x‖} ∩ U) + ENNReal.ofReal (eps⁻¹ ^ 2) * (sqWeightedMeasure g MeasureTheory.volume) ({x : Vec d | eps * level / 2 < ‖g x‖} ∩ U)

    The ambient-set specialization of oneStoppingBallTailControl_apply.

    source
    theorem HCPolySupport.CubeCalderonZygmund.nullMeasurableSet_oneStoppingBall_f_tail {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] (f : Vec d → F) (level : ℝ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
    MeasureTheory.NullMeasurableSet {x : Vec d | level / 2 < ‖f x‖} MeasureTheory.volume

    The first lower-tail set is volume-null-measurable when the field is almost-everywhere strongly measurable.

    source
    theorem HCPolySupport.CubeCalderonZygmund.nullMeasurableSet_oneStoppingBall_g_tail {d : ℕ} {G : Type u_1} [NormedAddCommGroup G] (g : Vec d → G) (eps level : ℝ) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) :
    MeasureTheory.NullMeasurableSet {x : Vec d | eps * level / 2 < ‖g x‖} MeasureTheory.volume

    The scaled second lower-tail set is volume-null-measurable when the field is almost-everywhere strongly measurable.