Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapScalarPComparison

Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapScalarPComparison #

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

Exact scalar overlap comparison at arbitrary finite exponent #

This module transports the established finite-depth scalar overlap estimates to the exact diagonal overlap seminorm through its exact p-power identity.

source
theorem HCPolySupport.exactOverlapScalarPSeminorm_rpow_le_gagliardo {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (p : FiniteLpExponent) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (humeas : Measurable u) (hmem : MeasureTheory.MemLp u p.exponent (normalizedCubeMeasure Q)) :
exactOverlapFiniteSeminorm (exactOverlapScalarPParameters s p) Q u hu ^ p.exponent.toReal ≤ 2 * 3 ^ d * Gagliardo.cubeGagliardoESeminorm Q (↑s) p.exponent u ^ p.exponent.toReal

Exact scalar overlap Besov-to-Gagliardo comparison at an arbitrary finite exponent, with the constant from the finite-depth estimate.

source
theorem HCPolySupport.gagliardo_rpow_le_exactOverlapScalarPSeminorm {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (p : FiniteLpExponent) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (humeas : Measurable u) (hmem : MeasureTheory.MemLp u p.exponent (normalizedCubeMeasure Q)) :
Gagliardo.cubeGagliardoESeminorm Q (↑s) p.exponent u ^ p.exponent.toReal ≤ Gagliardo.gagliardoBesovLowerConstant d ^ p.exponent.toReal * exactOverlapFiniteSeminorm (exactOverlapScalarPParameters s p) Q u hu ^ p.exponent.toReal

Gagliardo-to-exact-scalar-overlap comparison at an arbitrary finite exponent, with the constant from the established shell estimate.