Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapFinitePOneDepthCZ

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

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

One-depth finite-p Calderon--Zygmund overlap estimate #

This is the one-depth analytic closure: the exact overlap energy of the gradient of a cube Dirichlet divergence solution is controlled by that of its datum, uniformly in the root scale and overlap depth.

source
theorem HCPolySupport.exists_exactOverlapFiniteP_oneDepth_cz (d : ℕ) [NeZero d] (q : FiniteLpExponent) :
∃ C < ⊤, ∀ (m : ℤ) (j : ℕ) (h : Vec d → Vec d), MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h x)) 2 (normalizedCubeMeasure (originCube d m)) → MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (h x)) q.exponent (normalizedCubeMeasure (originCube d m)) → ∀ (w : H10Function (openCubeSet (originCube d m))), CubeDirichletDivergenceProblem (originCube d m) w h → cubeEuclideanPositiveBesovOverlapDepthENorm (originCube d m) q w.grad j ^ q.exponent.toReal ≤ C * cubeEuclideanPositiveBesovOverlapDepthENorm (originCube d m) q h j ^ q.exponent.toReal

One exact-overlap depth of the finite-p gradient energy of a cube Dirichlet divergence solution is controlled by the corresponding depth of its datum, uniformly in both the root scale and the depth.