High-contrast homogenization: Provider.PolynomialHomogenization.CubeFractionalNormBridge

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Fractional square norms on triadic cubes

This file identifies the normalized Euclidean fractional norms at exponent two with the square quantities used by the high-contrast estimates.

theorem HCPolySupport.HighContrast.normalizedEuclideanLpENorm_two_sq_eq_eVolumeAverage {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => euclideanNorm (F x)) (normalizedCubeMeasure Q)) : (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm 2 F ^ 2 = eVolumeAverage (openCubeSet Q) fun (x : Vec d) => ENNReal.ofReal (vecNormSq (F x))

theorem HCPolySupport.HighContrast.cubeEuclideanWspESeminorm_two_sq_eq_fracSeminormSq {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (F : Vec d → Vec d) (hFmeas : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (openCubeSet Q))) : cubeEuclideanWspESeminorm Q s FiniteLpExponent.two F ^ 2 = fracSeminormSq (openCubeSet Q) (↑s) F

theorem HCPolySupport.HighContrast.cubeEuclideanWspFullENorm_two_sq_eq_hsNormSq {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (F : Vec d → Vec d) (hFmeas : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (openCubeSet Q))) : cubeEuclideanWspFullENorm Q s FiniteLpExponent.two F ^ 2 = hsNormSq (openCubeSet Q) (↑s) F