Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapFinitePPoincareDepth

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

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

Finite-p overlap Poincaré assembly at one depth #

This module assembles the normalized vector overlap-cube Poincaré estimate over one retained depth. All constants are chosen before the cube, depth, and vector field.

source
theorem HCPolySupport.exists_cubeEuclideanPositiveBesovOverlapDepthENorm_rpow_le {d : ℕ} [NeZero d] (q : FiniteLpExponent) :
∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (Q : TriadicCube d) (j : ℕ) (V : CubeVectorW1pFunction Q q), cubeEuclideanPositiveBesovOverlapDepthENorm Q q V.toField j ^ q.exponent.toReal ≤ C * ENNReal.ofReal (cubeScaleFactor Q / 3 ^ j) ^ q.exponent.toReal * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat (V.jacobian x)) q.exponent (normalizedCubeMeasure Q) ^ q.exponent.toReal

One-depth powered overlap Poincaré assembly for an arbitrary cube-vector finite-W¹ᵖ field.