Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.CenteredCubeFractionalCZ

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

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

Fractional Calderón--Zygmund estimate on centered cubes #

This module packages the supplied zero-trace cube solution with the literal Euclidean fractional-Sobolev field carried by its gradient.

source
theorem HCPolySupport.centeredCubeH10ScalarDivergence_fractional_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 → ∃ (gradW : CubeEuclideanWspField (originCube d m) s q), gradW.toField = w.grad ∧ cubeEuclideanWspESeminorm (originCube d m) s q gradW.toField ≤ C * (ENNReal.ofReal sigma0)⁻¹ * cubeEuclideanWspESeminorm (originCube d m) s q h.toField

A supplied zero-trace centered-cube divergence solution with fractional L² ∩ L^q datum has a literal fractional-Sobolev gradient, with a constant uniform in the cube scale, coefficient scale, and fractional order.