Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.LocalScaledDatumEnergy

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

Normalized energy bookkeeping for the scaled comparison datum

The local harmonic-replacement construction controls its zero-trace correction in the raw Hilbert L² realization. This file transports that estimate to the normalized measure of the same axis cube. Both sides acquire exactly the same normalizing factor, so the datum is naturally the scaled field sigma0⁻¹ • hilbertifyVecField H; in particular no volume or dimension factor is introduced.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_hilbertify_grad_two_eq_ofReal_norm_gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : MeasureTheory.eLpNorm (hilbertifyVecField u.grad) 2 (MeasureTheory.volume.restrict U) = ENNReal.ofReal ‖u.gradToHilbertVectorL2‖

The raw restricted Hilbert L² norm of an H¹ gradient is exactly its Hilbert-valued eLpNorm.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_hilbertifyVecField_two_eq_ofReal_norm_toHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} {H : Vec d → Vec d} (hH : MemVectorL2 U H) : MeasureTheory.eLpNorm (hilbertifyVecField H) 2 (MeasureTheory.volume.restrict U) = ENNReal.ofReal ‖toHilbertVectorL2OfVecField hH‖

The raw restricted Hilbert L² norm of a plain vector datum is exactly the eLpNorm of its Hilbert realization.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalized_eLpNorm_harmonicCorrection_le_scaledDatum {d : ℕ} (z : Vec d) {L sigma0 : ℝ} (hL : 0 < L) (hsigma0 : 0 < sigma0) (w : H1Function (axisCube z L)) {H : Vec d → Vec d} (hH : MemVectorL2 (axisCube z L) H) (henergy : ‖w.gradToHilbertVectorL2‖ ≤ sigma0⁻¹ * ‖toHilbertVectorL2OfVecField hH‖) : MeasureTheory.eLpNorm (hilbertifyVecField w.grad) 2 (axisCubeNormalizedMeasure z L) ≤ MeasureTheory.eLpNorm (sigma0⁻¹ • hilbertifyVecField H) 2 (axisCubeNormalizedMeasure z L)

On a positive axis cube, the local harmonic-replacement energy estimate becomes the exact normalized L² estimate for the datum scaled by sigma0⁻¹. The normalizing volume factor is common to both sides and hence cancels without a dimension loss.

theorem HCPolySupport.CubeCalderonZygmund.memHilbertVectorL2_axisCubeNormalizedMeasure {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) {F : Vec d → HilbertVec d} (hF : MemHilbertVectorL2 (axisCube z L) F) : MeasureTheory.MemLp F 2 (axisCubeNormalizedMeasure z L)

A Hilbert-vector L² field on an axis cube is also L² for its normalized measure. This is only a finite rescaling of the restricted volume measure.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalized_eLpNorm_two_sub_le {d : ℕ} (z : Vec d) {L : ℝ} {F G : Vec d → HilbertVec d} : MeasureTheory.eLpNorm (F - G) 2 (axisCubeNormalizedMeasure z L) ≤ MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure z L) + MeasureTheory.eLpNorm G 2 (axisCubeNormalizedMeasure z L)

Minkowski's inequality in the normalized measure of a cube.