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

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

Local Hilbert-vector bridges for the comparison step

The local harmonic replacement is formulated with the weak PDE datum in the plain Vec d carrier, while the good-lambda tails are Hilbert-vector valued. This module records the exact restriction, norm, and a.e.-transport bridges between those two interfaces. In particular, the inverse Hilbert-vector map is used only to prepare the weak datum, so no dimension factor is introduced there.

theorem HCPolySupport.CubeCalderonZygmund.memVectorL2_of_memLp_hilbertifyVecField {d : ℕ} {B : Set (Vec d)} {H : Vec d → Vec d} (hH : MeasureTheory.MemLp (hilbertifyVecField H) 2 MeasureTheory.volume) : MemVectorL2 B H

A globally square-integrable Hilbert-vector realization yields an L² plain-vector datum on every local set.

theorem HCPolySupport.CubeCalderonZygmund.memHilbertVectorL2_restrict_of_memLp_hilbertifyVecField {d : ℕ} {B : Set (Vec d)} {H : Vec d → Vec d} (hH : MeasureTheory.MemLp (hilbertifyVecField H) 2 MeasureTheory.volume) : MemHilbertVectorL2 B (hilbertifyVecField H)

The local Hilbert-valued field inherits square integrability by measure restriction.

theorem HCPolySupport.CubeCalderonZygmund.norm_toHilbertVectorL2OfVecField_eq_eLpNorm_toReal {d : ℕ} {B : Set (Vec d)} {H : Vec d → Vec d} (hH : MemVectorL2 B H) : ‖toHilbertVectorL2OfVecField hH‖ = (MeasureTheory.eLpNorm (hilbertifyVecField H) 2 (MeasureTheory.volume.restrict B)).toReal

The norm of the Hilbert-vector L² representative is exactly the real value of the Hilbert-valued eLpNorm.

theorem HCPolySupport.CubeCalderonZygmund.norm_sq_toHilbertVectorL2OfVecField_eq_lintegral_enorm {d : ℕ} {B : Set (Vec d)} {H : Vec d → Vec d} (hH : MemVectorL2 B H) : ‖toHilbertVectorL2OfVecField hH‖ ^ 2 = (∫⁻ (x : Vec d) in B, ‖hilbertifyVecField H x‖ₑ ^ 2).toReal

The squared local Hilbert L² norm is the finite real value of its raw squared norm integral.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_hilbertifyVecField_restrict_lt_top {d : ℕ} {B : Set (Vec d)} {H : Vec d → Vec d} (hH : MemVectorL2 B H) : MeasureTheory.eLpNorm (hilbertifyVecField H) 2 (MeasureTheory.volume.restrict B) < ⊤

The Hilbert-valued local eLpNorm in the preceding bridge is finite.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_eq_of_ae_eq_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {B : Set α} {F G : α → E} (hFG : F =ᵐ[μ.restrict B] G) : sqWeightedMeasure F (μ.restrict B) = sqWeightedMeasure G (μ.restrict B)

Restricted a.e. equality transports the square-weighted measure built from the two local representatives.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_apply_inter_eq_of_ae_eq_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {B T : Set α} (hB : MeasurableSet B) {F G : α → E} (hFG : F =ᵐ[μ.restrict B] G) : (sqWeightedMeasure F μ) (T ∩ B) = (sqWeightedMeasure G μ) (T ∩ B)

On a measurable local set, restricted a.e. equality transports the original square-weighted measure on every subset of that set.

theorem HCPolySupport.CubeCalderonZygmund.local_lintegral_norm_rpow_eq_of_ae_eq_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {B : Set α} {F G : α → E} (q : ℝ) (hFG : F =ᵐ[μ.restrict B] G) : ∫⁻ (x : α) in B, ENNReal.ofReal (‖F x‖ ^ q) ∂μ = ∫⁻ (x : α) in B, ENNReal.ofReal (‖G x‖ ^ q) ∂μ

A local norm-power lintegral is invariant under restricted a.e. equality.

theorem HCPolySupport.CubeCalderonZygmund.local_lintegral_sub_norm_sq_eq_of_ae_eq_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {B : Set α} {F G V : α → E} (hFG : F =ᵐ[μ.restrict B] G) : ∫⁻ (x : α) in B, ENNReal.ofReal (‖F x - V x‖ ^ 2) ∂μ = ∫⁻ (x : α) in B, ENNReal.ofReal (‖G x - V x‖ ^ 2) ∂μ

The local squared difference integral is invariant when its first field is replaced by a restricted-a.e.-equal representative.

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

Minkowski's triangle inequality on the normalized measure of an axis cube, in the Hilbert-valued form consumed by the comparison argument.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalized_eLpNorm_two_const_smul {d : ℕ} (z : Vec d) (L c : ℝ) (F : Vec d → HilbertVec d) : MeasureTheory.eLpNorm (c • F) 2 (axisCubeNormalizedMeasure z L) = ‖c‖ₑ * MeasureTheory.eLpNorm F 2 (axisCubeNormalizedMeasure z L)

Scalar multiplication has its exact expected effect on the normalized axis-cube Hilbert L² eLpNorm.

theorem HCPolySupport.CubeCalderonZygmund.norm_toHilbertVectorL2OfVecField_add_le_axisCube {d : ℕ} (z : Vec d) (L : ℝ) {F G : Vec d → Vec d} (hF : MemVectorL2 (axisCube z L) F) (hG : MemVectorL2 (axisCube z L) G) : ‖toHilbertVectorL2OfVecField ⋯‖ ≤ ‖toHilbertVectorL2OfVecField hF‖ + ‖toHilbertVectorL2OfVecField hG‖

The corresponding triangle inequality for the typed local Hilbert L² representatives of two vector fields on an axis cube.