Coarse-graining support: Support.Sobolev.Foundations.WeakHessianEuclidean

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

Euclidean norms for weak Hessians

This module gives the coordinate weak-Hessian carrier its canonical Euclidean (Frobenius) pointwise magnitude and its volume-normalized L² norm on cubes. The pre-existing coordinate-ℓ¹ norm remains available for estimates proved before this Euclidean interface was introduced.

noncomputable def HCPolySupport.matrixFrobeniusMagnitude {d : ℕ} (A : Mat d) : ℝ

Frobenius magnitude of a real matrix.

Equations

• HCPolySupport.matrixFrobeniusMagnitude A = √(∑ i : Fin d, ∑ j : Fin d, A i j ^ 2)

theorem HCPolySupport.matrixFrobeniusMagnitude_nonneg {d : ℕ} (A : Mat d) : 0 ≤ matrixFrobeniusMagnitude A

theorem HCPolySupport.sq_matrixFrobeniusMagnitude {d : ℕ} (A : Mat d) : matrixFrobeniusMagnitude A ^ 2 = ∑ i : Fin d, ∑ j : Fin d, A i j ^ 2

@[simp]

theorem HCPolySupport.matrixFrobeniusMagnitude_zero {d : ℕ} : matrixFrobeniusMagnitude 0 = 0

theorem HCPolySupport.matrixFrobeniusMagnitude_eq_norm_hilbertMat_ofMat {d : ℕ} (A : Mat d) : matrixFrobeniusMagnitude A = ‖HilbertMat.ofMat A‖

The explicit matrix Frobenius magnitude agrees with the norm of the project's Euclidean Hilbert matrix realization.

theorem HCPolySupport.matrixFrobeniusMagnitude_le_sum_abs {d : ℕ} (A : Mat d) : matrixFrobeniusMagnitude A ≤ ∑ i : Fin d, ∑ j : Fin d, |A i j|

noncomputable def HCPolySupport.HasWeakHessianOn.frobeniusMagnitude {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) : Vec d → ℝ

Pointwise matrix Frobenius magnitude of the weak Hessian carrier.

Equations

• H.frobeniusMagnitude x = HCPolySupport.matrixFrobeniusMagnitude fun (i j : Fin d) => H.hess i j x

theorem HCPolySupport.HasWeakHessianOn.sq_frobeniusMagnitude {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (x : Vec d) : H.frobeniusMagnitude x ^ 2 = ∑ i : Fin d, ∑ j : Fin d, H.hess i j x ^ 2

The pointwise square of frobeniusMagnitude is the sum of the squares of all weak Hessian coordinates.

theorem HCPolySupport.HasWeakHessianOn.hess_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (i j : Fin d) : MeasureTheory.MemLp (H.hess i j) 2 (normalizedCubeMeasure Q)

Each weak Hessian coordinate is square-integrable for normalized cube volume whenever its carrier domain is that open cube.

theorem HCPolySupport.HasWeakHessianOn.frobeniusMagnitude_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : MeasureTheory.MemLp H.frobeniusMagnitude 2 (normalizedCubeMeasure Q)

The pointwise Frobenius magnitude of a weak Hessian is in normalized L² on every cube on which the carrier is defined.

theorem HCPolySupport.HasWeakHessianOn.integral_frobeniusMagnitude_sq_eq_sum_integral {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : ∫ (x : Vec d), H.frobeniusMagnitude x ^ 2 ∂normalizedCubeMeasure Q = ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), H.hess i j x ^ 2 ∂normalizedCubeMeasure Q

theorem HCPolySupport.HasWeakHessianOn.integral_hess_sq_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (i j : Fin d) : ∫ (x : Vec d), H.hess i j x ^ 2 ∂normalizedCubeMeasure Q = (cubeVolume Q)⁻¹ * ‖H.hessCoordToScalarL2 i j‖ ^ 2

noncomputable def HCPolySupport.HasWeakHessianOn.frobeniusMagnitudeNormalizedLpNorm {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : ℝ

The proof-carrying normalized L² value of the pointwise Frobenius magnitude, on the safe half-open carrier of a cube.

Equations

• HCPolySupport.HasWeakHessianOn.frobeniusMagnitudeNormalizedLpNorm Q H = (HCPolySupport.cubeBoundedMeasurableDomain Q).normalizedLpNorm 2 H.frobeniusMagnitude ⋯

theorem HCPolySupport.HasWeakHessianOn.frobeniusMagnitudeNormalizedLpNorm_eq_integral {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : frobeniusMagnitudeNormalizedLpNorm Q H = (∫ (x : Vec d), H.frobeniusMagnitude x ^ 2 ∂normalizedCubeMeasure Q) ^ (1 / 2)

Literal manuscript formula for the proof-carrying normalized Frobenius L² value.

theorem HCPolySupport.HasWeakHessianOn.frobeniusMagnitudeNormalizedLpNorm_sq {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : frobeniusMagnitudeNormalizedLpNorm Q H ^ 2 = (cubeVolume Q)⁻¹ * ∑ i : Fin d, ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖ ^ 2

noncomputable def HCPolySupport.HasWeakHessianOn.frobeniusNormalizedL2 {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : ℝ

The volume-normalized L² Frobenius norm of a weak Hessian on an open cube. The inverse square-root volume factor is explicit.

Equations

• HCPolySupport.HasWeakHessianOn.frobeniusNormalizedL2 Q H = (HCPolySupport.cubeVolume Q)⁻¹ ^ (1 / 2) * √(∑ i : Fin d, ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖ ^ 2)

theorem HCPolySupport.HasWeakHessianOn.frobeniusNormalizedL2_sq {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : frobeniusNormalizedL2 Q H ^ 2 = (cubeVolume Q)⁻¹ * ∑ i : Fin d, ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖ ^ 2

Squared characterization of the normalized Frobenius L² norm.

theorem HCPolySupport.HasWeakHessianOn.sqrt_sum_sq_hessCoordToScalarL2_le_hessianCoordL2NormSum {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) : √(∑ i : Fin d, ∑ j : Fin d, ‖H.hessCoordToScalarL2 i j‖ ^ 2) ≤ H.hessianCoordL2NormSum

The Hilbert sum of coordinate L² norms is bounded by their ℓ¹ sum.

theorem HCPolySupport.HasWeakHessianOn.frobeniusNormalizedL2_le_volumeNormalized_hessianCoordL2NormSum {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : frobeniusNormalizedL2 Q H ≤ (cubeVolume Q)⁻¹ ^ (1 / 2) * H.hessianCoordL2NormSum

Bridge from the Frobenius norm to the older volume-normalized coordinate ℓ¹ Hessian norm.

theorem HCPolySupport.HasWeakHessianOn.frobeniusNormalizedL2_eq_frobeniusMagnitudeNormalizedLpNorm {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) : frobeniusNormalizedL2 Q H = frobeniusMagnitudeNormalizedLpNorm Q H

The coordinate Hilbert-sum realization is exactly the proof-carrying normalized L² norm of the pointwise Frobenius magnitude.

theorem HCPolySupport.HasWeakHessianOn.frobeniusNormalizedL2_eq_of_hasWeakHessianOn {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H K : HasWeakHessianOn (openCubeSet Q) v) : frobeniusNormalizedL2 Q H = frobeniusNormalizedL2 Q K

The normalized Frobenius L² value does not depend on the particular weak-Hessian representative of an H¹ function on an open cube.