Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.OverlapCubeVectorNormalized #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Vector finite-p Poincare estimates on overlap cubes #
The scalar overlap-cube estimate is transported here to the normalized vector
carrier used by the finite-p Calderon--Zygmund layer.
theorem
HCPolySupport.exists_overlapCubeVector_normalized_poincare_constant
{d : ℕ}
[NeZero d]
(q : FiniteLpExponent)
:
∃ (C : ENNReal),
C ≠ ⊤ ∧ ∀ (Q : TriadicCube d) (j : ℕ),
∀ S ∈ ScalarOverlap.centersAtDepth Q j,
∀ (V : CubeVectorW1pFunction Q q),
MeasureTheory.eLpNorm
(fun (x : Vec d) => HilbertVec.ofVec (V.toField x - ScalarOverlap.cubeAverageVec S V.toField)) q.exponent
(ScalarOverlap.normalizedCubeMeasure S) ≤ C * ENNReal.ofReal (overlapCubeScaleFactor S) * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat (V.jacobian x)) q.exponent
(ScalarOverlap.normalizedCubeMeasure S)
The normalized finite-p Poincare estimate for vector fields on one
retained overlap cube.