Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.ClosedBallNormalizedL2

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

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

Exact closed-ball / normalized-cube L² bridge #

The stopping construction records a real normalized squared energy on closed sup-metric balls. The local harmonic comparison uses the ENNReal eLpNorm on the a.e.-equal open axis cube. This file identifies the two normalizations without a geometric comparison constant.

source
theorem HCPolySupport.CubeCalderonZygmund.stoppingAxisCube_eLpNorm_two_sq_eq_ofReal_closedBallL2Energy {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (x : Vec d) {S r : ℝ} (hS : 0 < S) (hr : 0 < r) (F : Vec d → E) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (Metric.closedBall x (S * r)))) :
MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure (stoppingAxisCubeCorner x S r) (stoppingAxisCubeSide S r)) ^ 2 = ENNReal.ofReal (closedBallL2Energy F x (S * r))

The squared normalized cube L² seminorm is exactly the ofReal of the closed-ball squared energy at the corresponding stopping scale.

source
theorem HCPolySupport.CubeCalderonZygmund.stoppingAxisCube_eLpNorm_two_eq_ofReal_sqrt_closedBallL2Energy {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (x : Vec d) {S r : ℝ} (hS : 0 < S) (hr : 0 < r) (F : Vec d → E) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (Metric.closedBall x (S * r)))) :
MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure (stoppingAxisCubeCorner x S r) (stoppingAxisCubeSide S r)) = ENNReal.ofReal √(closedBallL2Energy F x (S * r))

The normalized cube L² seminorm is exactly the square root of the closed-ball squared energy at the corresponding stopping scale.

source
theorem HCPolySupport.CubeCalderonZygmund.stoppingAxisCube_eLpNorm_two_eq_ofReal_sqrt_closedBallL2Energy_of_memLp {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (x : Vec d) {S r : ℝ} (hS : 0 < S) (hr : 0 < r) (F : Vec d → E) (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) :
MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure (stoppingAxisCubeCorner x S r) (stoppingAxisCubeSide S r)) = ENNReal.ofReal √(closedBallL2Energy F x (S * r))

The global L² assumption supplies the local integrability needed by the exact stopping-cube energy bridge.

source
theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_eLpNorm_two_eq_ofReal_sqrt_closedBallL2Energy {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (x : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) (F : Vec d → E) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (Metric.closedBall x (stoppingComparisonParentMultiplier n * r)))) :
MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure (stoppingComparisonParentCorner x r n) (stoppingComparisonParentSide r n)) = ENNReal.ofReal √(closedBallL2Energy F x (stoppingComparisonParentMultiplier n * r))

The exact L² bridge at the harmonic comparison parent.