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

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

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_apply_univ_eq_eLpNorm_two_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (μ : MeasureTheory.Measure α) (hf : MeasureTheory.AEStronglyMeasurable f μ) : (sqWeightedMeasure f μ) Set.univ = MeasureTheory.eLpNorm f 2 μ ^ 2

Total square-weighted mass is exactly the square of the L² eLpNorm. This identity needs a.e. strong measurability but no integrability assumption.

Quantitative L² energy of one weak-Hessian row

The coordinate L² data in HasWeakHessianOn control each Euclidean Hilbert realization of a Hessian row. The estimates below retain the older coordinate-ℓ1 energy hessianCoordL2NormSum, which is the quantity supplied by the quantitative weak-H² theory.

theorem HCPolySupport.HasWeakHessianOn.hessianHilbertRow_memLp_two {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : MeasureTheory.MemLp (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) 2 (volumeMeasureOn U)

A Hilbertified Hessian row belongs to raw L² on the carrier domain.

theorem HCPolySupport.HasWeakHessianOn.eLpNorm_hess_eq_ofReal_norm_hessCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i j : Fin d) : MeasureTheory.eLpNorm (fun (x : Vec d) => H.hess i j x) 2 (volumeMeasureOn U) = ENNReal.ofReal ‖H.hessCoordToScalarL2 i j‖

A Hessian coordinate's raw eLpNorm is the extended-real realization of the norm stored in hessCoordToScalarL2.

theorem HCPolySupport.HasWeakHessianOn.eLpNorm_hessianHilbertRow_two_le {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : MeasureTheory.eLpNorm (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) 2 (volumeMeasureOn U) ≤ ENNReal.ofReal H.hessianCoordL2NormSum

The raw Euclidean L² norm of one Hessian row is bounded by the total coordinate L² energy recorded by the weak-Hessian witness.

theorem HCPolySupport.HasWeakHessianOn.toReal_eLpNorm_hessianHilbertRow_two_le {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : (MeasureTheory.eLpNorm (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) 2 (volumeMeasureOn U)).toReal ≤ H.hessianCoordL2NormSum

Real-valued form of the raw one-row L² estimate.

theorem HCPolySupport.HasWeakHessianOn.sqWeightedMeasure_hessianHilbertRow_apply_univ_le {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) : (CubeCalderonZygmund.sqWeightedMeasure (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) (volumeMeasureOn U)) Set.univ ≤ ENNReal.ofReal (H.hessianCoordL2NormSum ^ 2)

The total raw square-weighted mass of one Hilbertified Hessian row is bounded by the square of hessianCoordL2NormSum.

theorem HCPolySupport.HasWeakHessianOn.hessianHilbertRow_memLp_two_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (i : Fin d) : MeasureTheory.MemLp (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) 2 (normalizedCubeMeasure Q)

On a cube, a Hilbertified Hessian row belongs to normalized L².

theorem HCPolySupport.HasWeakHessianOn.eLpNorm_hessianHilbertRow_two_normalizedCubeMeasure_le {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (i : Fin d) : MeasureTheory.eLpNorm (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) 2 (normalizedCubeMeasure Q) ≤ ENNReal.ofReal ((cubeVolume Q)⁻¹ ^ (1 / 2) * H.hessianCoordL2NormSum)

The normalized Euclidean L² norm of one Hessian row has the expected inverse-square-root volume factor.

theorem HCPolySupport.HasWeakHessianOn.toReal_eLpNorm_hessianHilbertRow_two_normalizedCubeMeasure_le {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (i : Fin d) : (MeasureTheory.eLpNorm (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) 2 (normalizedCubeMeasure Q)).toReal ≤ (cubeVolume Q)⁻¹ ^ (1 / 2) * H.hessianCoordL2NormSum

Real-valued form of the normalized one-row L² estimate.

theorem HCPolySupport.HasWeakHessianOn.sqWeightedMeasure_hessianHilbertRow_normalizedCubeMeasure_apply_univ_le {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (i : Fin d) : (CubeCalderonZygmund.sqWeightedMeasure (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x) (normalizedCubeMeasure Q)) Set.univ ≤ ENNReal.ofReal (((cubeVolume Q)⁻¹ ^ (1 / 2) * H.hessianCoordL2NormSum) ^ 2)

The normalized total square-weighted mass of one Hessian row is controlled by the square of the volume-normalized weak-H² energy.

theorem HCPolySupport.HasWeakHessianOn.indicator_hessianHilbertRow_memLp_two {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) (hU : MeasurableSet U) : MeasureTheory.MemLp (U.indicator (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x)) 2 MeasureTheory.volume

A measurable-domain zero extension of one Hessian row belongs to global L².

theorem HCPolySupport.HasWeakHessianOn.sqWeightedMeasure_indicator_hessianHilbertRow_apply_univ_le {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) (hU : MeasurableSet U) : (CubeCalderonZygmund.sqWeightedMeasure (U.indicator (hilbertifyVecField fun (x : Vec d) (j : Fin d) => H.hess i j x)) MeasureTheory.volume) Set.univ ≤ ENNReal.ofReal (H.hessianCoordL2NormSum ^ 2)

The global square-weighted mass of a Hessian row extended by zero is controlled by its local weak-H² energy.