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

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

Normalized finite-p norms on axis cubes

This module records the ENNReal bridge from a normalized axis-cube eLpNorm to its powered local integral. The local comparison argument uses the raw set integral after this bridge; no real-valued toReal conversion is needed here.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eLpNorm_rpow_exponent_eq_lintegral_enorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) (L : ℝ) (p : FiniteLpExponent) (F : Vec d → E) (hF : MeasureTheory.AEStronglyMeasurable F (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm F p.exponent (axisCubeNormalizedMeasure z L) ^ p.exponent.toReal = ∫⁻ (x : Vec d), ‖F x‖ₑ ^ p.exponent.toReal ∂axisCubeNormalizedMeasure z L

The pth power of a finite eLpNorm is its defining norm-power lintegral.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_lintegral_enorm_rpow_eq_lintegral_ofReal_norm_rpow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) (L : ℝ) (p : FiniteLpExponent) (F : Vec d → E) : ∫⁻ (x : Vec d), ‖F x‖ₑ ^ p.exponent.toReal ∂axisCubeNormalizedMeasure z L = ∫⁻ (x : Vec d), ENNReal.ofReal (‖F x‖ ^ p.exponent.toReal) ∂axisCubeNormalizedMeasure z L

The norm-power integrand has the source-facing ofReal spelling.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_lintegral_ofReal_norm_rpow_eq_normalized_setLIntegral {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (p : FiniteLpExponent) (F : Vec d → E) : ∫⁻ (x : Vec d), ENNReal.ofReal (‖F x‖ ^ p.exponent.toReal) ∂axisCubeNormalizedMeasure z L = ENNReal.ofReal (L ^ d)⁻¹ * ∫⁻ (x : Vec d) in axisCube z L, ENNReal.ofReal (‖F x‖ ^ p.exponent.toReal)

The normalized local norm-power integral is exactly the normalized raw volume integral over a positive axis cube.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eLpNorm_rpow_exponent_eq_normalized_setLIntegral {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (p : FiniteLpExponent) (F : Vec d → E) (hF : MeasureTheory.AEStronglyMeasurable F (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm F p.exponent (axisCubeNormalizedMeasure z L) ^ p.exponent.toReal = ENNReal.ofReal (L ^ d)⁻¹ * ∫⁻ (x : Vec d) in axisCube z L, ENNReal.ofReal (‖F x‖ ^ p.exponent.toReal)

The powered normalized finite-p norm is the normalized raw local norm-power integral.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eLpNorm_rpow_exponent_lt_top {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) (L : ℝ) (p : FiniteLpExponent) (F : Vec d → E) (hF : MeasureTheory.MemLp F p.exponent (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm F p.exponent (axisCubeNormalizedMeasure z L) ^ p.exponent.toReal < ⊤

MemLp supplies the finiteness required when the powered norm is used in an ENNReal inequality.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_ae_eq_closedBall_axisCubeCenter {d : ℕ} [NeZero d] (z : Vec d) {L : ℝ} (hL : 0 < L) : axisCube z L =ᵐ[MeasureTheory.volume] Metric.closedBall (axisCubeCenter z L) (L / 2)

The open axis cube has the expected closed sup-ball realization.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_setLIntegral_eq_of_ae_eq {d : ℕ} (z : Vec d) (L : ℝ) (B : Set (Vec d)) (hB : axisCube z L =ᵐ[MeasureTheory.volume] B) (f : Vec d → ENNReal) : ∫⁻ (x : Vec d) in axisCube z L, f x = ∫⁻ (x : Vec d) in B, f x

A raw local lintegral is invariant under replacing an axis cube by an a.e.-equal set, in particular by its closed sup-ball realization.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eLpNorm_rpow_exponent_eq_normalized_closedBallLIntegral {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (p : FiniteLpExponent) (F : Vec d → E) (hF : MeasureTheory.AEStronglyMeasurable F (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm F p.exponent (axisCubeNormalizedMeasure z L) ^ p.exponent.toReal = ENNReal.ofReal (L ^ d)⁻¹ * ∫⁻ (x : Vec d) in Metric.closedBall (axisCubeCenter z L) (L / 2), ENNReal.ofReal (‖F x‖ ^ p.exponent.toReal)

The powered norm bridge written over the closed sup-ball associated to a positive axis cube.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eLpNorm_two_sq_eq_normalized_setLIntegral {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (F : Vec d → E) (hF : MeasureTheory.AEStronglyMeasurable F (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure z L) ^ 2 = ENNReal.ofReal (L ^ d)⁻¹ * ∫⁻ (x : Vec d) in axisCube z L, ENNReal.ofReal (‖F x‖ ^ 2)

The squared normalized L² norm is the normalized raw squared-energy integral on a positive axis cube.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eLpNorm_two_sq_eq_normalized_closedBallLIntegral {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (F : Vec d → E) (hF : MeasureTheory.AEStronglyMeasurable F (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure z L) ^ 2 = ENNReal.ofReal (L ^ d)⁻¹ * ∫⁻ (x : Vec d) in Metric.closedBall (axisCubeCenter z L) (L / 2), ENNReal.ofReal (‖F x‖ ^ 2)

The squared normalized L² norm has the same closed-ball integral form.