Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.CubeEmbedding.LimitFiniteP

Coarse-graining support: Support.Sobolev.CubeEmbedding.LimitFiniteP #

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

Finite-p coordinate GNS input for cube localization #

This module records the coordinate form of the ambient finite-p Gagliardo--Nirenberg--Sobolev theorem. It is the analytic estimate applied to compactly supported smooth folded approximants in the cube localization step.

source
theorem HCPolySupport.clm_norm_le_sum_basisVec_finiteLp {d : ℕ} (T : Vec d →L[ℝ] ℝ) :
‖T‖ ≤ ∑ i : Fin d, ‖T (basisVec i)‖

The operator norm of a scalar functional on Vec d is bounded by its values on the coordinate basis.

source
theorem HCPolySupport.gns_coord_finiteLp {d : ℕ} (hd : 0 < d) (p q : FiniteLpExponent) (hp : p.exponent.toReal < ↑d) (hpq : q.exponent.toReal⁻¹ = p.exponent.toReal⁻¹ - (↑d)⁻¹) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ 1 ψ) (hcs : HasCompactSupport ψ) :
MeasureTheory.eLpNorm ψ q.exponent MeasureTheory.volume ≤ ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ MeasureTheory.volume ↑p.exponent.toNNReal) * ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ ψ x) (basisVec i)) p.exponent MeasureTheory.volume

Coordinate form of the ambient finite-p GNS inequality.

The finite-exponent cube embedding #

source
theorem HCPolySupport.cubeSobolevEmbedding_finiteLp {d : ℕ} (hd : 0 < d) (p : FiniteLpExponent) (hp : p.exponent.toReal < ↑d) :
∃ (C : NNReal), 0 < C ∧ ∀ (q : FiniteLpExponent), q.exponent.toReal⁻¹ = p.exponent.toReal⁻¹ - (↑d)⁻¹ → ∀ (z : Vec d) (L : ℝ), 0 < L → ∀ (u : W1pFunction (axisCube z L) p.exponent), MeasureTheory.eLpNorm u.toFun q.exponent (volumeMeasureOn (axisCube z L)) ≤ ↑C * (∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) p.exponent (volumeMeasureOn (axisCube z L)) + ENNReal.ofReal L⁻¹ * MeasureTheory.eLpNorm u.toFun p.exponent (volumeMeasureOn (axisCube z L)))

The finite-exponent axis-cube Sobolev inequality. The constant is chosen before the cube, its scale, and the Sobolev function; its displayed formula uses only the dimension and the input exponent.