Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeBesovPoincare.W12Embedding

Coarse-graining support: Support.Sobolev.Foundations.CubeBesovPoincare.W12Embedding #

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

Triadic-cube W^{1,2} to positive Besov embedding #

This module exposes the exact source-facing normalized W^{1,2} estimate. The local Poincare estimate and the normalized descendant-energy partition are assembled by the generic finite-depth B^1_{2,∞} aggregation lemma.

source
noncomputable def HCPolySupport.cubeBesovW12EmbeddingConstant (d : ℕ) :
ℝ

Dimensional constant for the triadic-cube W^{1,2} → B^1_{2,∞} embedding.

Equations
Instances For
    source
    theorem HCPolySupport.cubeBesovW12EmbeddingConstant_nonneg (d : ℕ) :
    0 ≤ cubeBesovW12EmbeddingConstant d
    source
    theorem HCPolySupport.cubeBesovPartialSeminormTop_one_two_le_normalizedW1pSeminorm {d : ℕ} (Q : TriadicCube d) (N : ℕ) (u : W1pFunction (openCubeSet Q) 2) :
    cubeBesovPartialSeminormTop Q 1 2 N u.toFun ≤ cubeBesovW12EmbeddingConstant d * BoundedMeasurableDomain.NormalizedW1pKernel.seminorm (⋯.toBoundedMeasurableDomain ⋯) 2 cubeBesovPartialSeminormTop_one_two_le_normalizedW1pSeminorm._proof_1 cubeBesovPartialSeminormTop_one_two_le_normalizedW1pSeminorm._proof_2 u

    Triadic-cube Poincare embedding of the normalized W^{1,2} unit ball into the positive Besov B^1_{2,∞} ball. Scale-free constant.