Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapFinitePFullCZ

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

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

Global finite-p exact-overlap Calderón--Zygmund estimate #

The one-depth exact-overlap estimate is summed with the source scale weights, then rooted at the finite exponent. The coefficient scale is removed by rescaling the datum before applying the one-depth result.

source
theorem HCPolySupport.exists_exactOverlapFiniteP_full_cz (d : ℕ) [NeZero d] (q : FiniteLpExponent) :
∃ C < ⊤, ∀ (m : ℤ) (sigma0 : ℝ) (s : ↑FractionalOrder) (h : CubeEuclideanWspL2Field (originCube d m) s q) (w : H10Function (openCubeSet (originCube d m))), 0 < sigma0 → IsCenteredCubeH10ScalarDivergenceSolution m sigma0 w h.toLpTwo → cubeEuclideanPositiveBesovOverlapESeminorm (originCube d m) s q w.grad ≤ C * (ENNReal.ofReal sigma0)⁻¹ * cubeEuclideanPositiveBesovOverlapESeminorm (originCube d m) s q h.toField

The global exact-overlap finite-p Calderón--Zygmund estimate for a supplied centered-cube divergence solution. Its constant is fixed before the cube scale, fractional order, coefficient scale, datum, and solution.