Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.WeakHessianFiniteP

Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.WeakHessianFiniteP #

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

Finite-p aggregation for weak Hessians #

This file packages rowwise Euclidean L^p control of a weak Hessian into the project's Hilbert matrix carrier. The norm estimate retains the exact finite exponent and bounds the matrix norm by the finite sum of its row norms.

source
theorem HCPolySupport.HasWeakHessianOn.hessianHilbertMat_memLp_of_rows {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (q : FiniteLpExponent) (μ : MeasureTheory.Measure (Vec d)) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) q.exponent μ) :
MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent μ

Rowwise Euclidean L^p membership packages into matrix-valued L^p membership.

source
theorem HCPolySupport.HasWeakHessianOn.eLpNorm_hessianHilbertMat_le_sum_rows {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (q : FiniteLpExponent) (μ : MeasureTheory.Measure (Vec d)) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) q.exponent μ) :
MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent μ ≤ ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) q.exponent μ

The matrix-valued finite-p norm of a weak Hessian is bounded by the finite sum of the Euclidean finite-p norms of its rows.

source
theorem HCPolySupport.HasWeakHessianOn.hessianHilbertMat_memLp_normalizedCubeMeasure_of_rows {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (q : FiniteLpExponent) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure Q)) :
MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure Q)

Normalized-cube specialization of HasWeakHessianOn.hessianHilbertMat_memLp_of_rows.

source
theorem HCPolySupport.HasWeakHessianOn.eLpNorm_hessianHilbertMat_normalizedCubeMeasure_le_sum_rows {d : ℕ} (Q : TriadicCube d) {v : H1Function (openCubeSet Q)} (H : HasWeakHessianOn (openCubeSet Q) v) (q : FiniteLpExponent) (hrows : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure Q)) :
MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat fun (i j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure Q) ≤ ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => H.hess i j x) q.exponent (normalizedCubeMeasure Q)

Normalized-cube specialization of the finite-p row-sum estimate.