Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapFinitePPDESplitting

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

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

Exact-overlap finite-p PDE splitting #

The smooth overlap average gives a paired H¹/W¹ᵖ divergence datum. This file combines that datum with the constant-coefficient cube estimates: the original zero-trace solution is compared to the solution driven by the smooth average, and the latter gradient receives a finite-W¹ᵖ representative.

source
theorem HCPolySupport.exists_exactOverlapFiniteP_pdeSplitting (d : ℕ) [NeZero d] (q : FiniteLpExponent) :
∃ C < ⊤, ∀ (m : ℤ) (j : ℕ) (P : SmoothOverlapPartition (originCube d 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 → ∃ (v : H10Function (openCubeSet (originCube d m))) (V : CubeVectorW1pFunction (originCube d m) q), CubeDirichletDivergenceProblem (originCube d m) v (P.averagingField h) ∧ V.toField = v.grad ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (w.grad x - v.grad x)) q.exponent (normalizedCubeMeasure (originCube d m)) ≤ C * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (h x - P.averagingField h x)) q.exponent (normalizedCubeMeasure (originCube d m)) ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat (V.jacobian x)) q.exponent (normalizedCubeMeasure (originCube d m)) ≤ C * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat ((P.averagingCompetitorW1p h q).jacobian x)) q.exponent (normalizedCubeMeasure (originCube d m))

On every origin cube, a zero-trace solution splits off the smooth overlap average. The constants depend only on the fixed dimension and finite exponent, and are chosen before the cube, averaging depth, partition, datum, and supplied solution.