Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.CenteredCubeFractionalGradientMemLp

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

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

Finite-exponent gradient membership for fractional divergence data #

This file packages the supplied-solution Calderón--Zygmund estimate as a literal normalized-cube L^q membership witness for the given H¹₀ gradient.

source
theorem HCPolySupport.centeredCubeH10ScalarDivergence_grad_memLp (d : ℕ) [NeZero d] (q : FiniteLpExponent) (m : ℤ) (sigma0 : ℝ) (s : ↑FractionalOrder) (h : CubeEuclideanWspL2Field (originCube d m) s q) (w : H10Function (openCubeSet (originCube d m))) (hsigma0 : 0 < sigma0) (hsolution : IsCenteredCubeH10ScalarDivergenceSolution m sigma0 w h.toLpTwo) :
MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (w.grad x)) q.exponent (normalizedCubeMeasure (originCube d m))

A supplied zero-trace centered-cube divergence solution driven by fractional L² ∩ L^q data has a literal normalized-cube L^q gradient.