Coarse-graining support: Support.Besov.Poincare.HarmonicGradient.LocalEstimate #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Final Local Estimate Adapter for Vector Poincare #
theorem
HCPolySupport.CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate.to_localEstimate
{d : ℕ}
{Q : TriadicCube d}
{C : ℝ}
{u : Vec d → ℝ}
{G : Vec d → Vec d}
{M : ℕ}
(hproj : CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C u G M)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hC : 0 ≤ C)
:
CubeLocalMultiscalePoincareVectorEstimate Q (3 / 2 * C * 3 ^ (↑d + 1)) u G M
Convert a vector projected dual estimate into the corresponding vector
local-multiscale estimate at the inflated note constant. The proof
splits the right-hand sum coordinatewise and reuses the scalar bridges
cubeBesovDualMeanZeroSeminorm_le_note_constant_mul_cubeBesovCircNorm and
cubeBesovCircNorm_projection_le_three_halves_mul_cubeBesovCircPartialNorm_of_memLp.