Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CoerciveSmooth

Coarse-graining support: Support.Sobolev.Foundations.CoerciveSmooth #

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

Smooth coercive core #

This file records the derivative-side smooth compact-support estimate that compares the full L² norm of the Fréchet derivative with the coordinate gradient sum already packaged in gradientCoordL2NormSum.

source
theorem HCPolySupport.H1Function.fderivL2Norm_le_gradientCoordL2NormSum_ofContDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) :
have u := ofContDiff hU ⋯ hf_supp; (MeasureTheory.eLpNorm (fderiv ℝ f) 2 MeasureTheory.volume).toReal ≤ u.gradientCoordL2NormSum

Smooth compactly supported functions supported in U have full Fréchet derivative L² norm controlled by the coordinate-gradient sum in the project's H¹ API.

source
theorem HCPolySupport.H1Function.valueL2Norm_le_sobolevConst_mul_gradientCoordL2NormSum_ofContDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (hBounded : IsBoundedDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) (hd : 2 < d) :
have u := ofContDiff hU ⋯ hf_supp; ‖u.toScalarL2‖ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst ℝ MeasureTheory.volume U 2 2) * u.gradientCoordL2NormSum

In dimensions d ≥ 3, smooth compactly supported functions supported in a bounded domain satisfy the coercive L² estimate with the coordinate-gradient sum on the right.