Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.CenteredCubeFractionalCZFullNorm

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

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

Full-norm fractional Calderón--Zygmund estimate on centered cubes #

The homogeneous fractional estimate and the normalized finite-L^p estimate combine into the source-facing inhomogeneous fractional-Sobolev estimate. The combination is carried out at the powered full norm, so its constant is uniform in the cube, fractional order, and coefficient scale.

source
theorem HCPolySupport.centeredCubeH10ScalarDivergence_fractional_cz_full (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 → cubeEuclideanWspFullENorm (originCube d m) s q w.grad ≤ C * (ENNReal.ofReal sigma0)⁻¹ * cubeEuclideanWspFullENorm (originCube d m) s q h.toField

A supplied zero-trace centered-cube divergence solution with fractional L² ∩ L^q datum satisfies the full fractional-Sobolev Calderón--Zygmund estimate. The constant is fixed before all scale, order, datum, and solution parameters.