FluxComparisonCZ #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Fractional Calderón--Zygmund flux comparison on centered cubes #
This is the source-facing assembly of the Chapter 3 deterministic duality argument. The public theorem below is deliberately kept to the exact manuscript hypotheses: the Dirichlet adjoint solve, fractional Calderón--Zygmund estimate, smooth-dual passage, and descendant localization are all internal proof steps.
noncomputable def
HCPolySupport.Book.Ch03.ABK26.smoothTestToCubeEuclideanWspL2Field
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
(h : CubeEuclideanWspSmoothTest Q s p)
:
CubeEuclideanWspL2Field Q s p
View a smooth fractional Sobolev test as a fractional Sobolev field with an L² bound.
Equations
- HCPolySupport.Book.Ch03.ABK26.smoothTestToCubeEuclideanWspL2Field h = { toField := h.toField, euclideanMemLp := ⋯, euclideanMemWsp := ⋯, euclideanMemL2 := ⋯ }
Instances For
noncomputable def
HCPolySupport.Book.Ch03.ABK26.smoothTestToCubeEuclideanL2LpField
{d : ℕ}
{Q : TriadicCube d}
{s : ↑FractionalOrder}
{p : FiniteLpExponent}
(h : CubeEuclideanWspSmoothTest Q s p)
:
View a smooth fractional Sobolev test as a field with L² and Lp bounds.
Equations
- HCPolySupport.Book.Ch03.ABK26.smoothTestToCubeEuclideanL2LpField h = { toField := h.toField, euclideanMemLp := ⋯, euclideanMemL2 := ⋯ }
Instances For
theorem
HCPolySupport.Book.Ch03.ABK26.exists_centeredCubeFluxComparison_cz
(d : ℕ)
(hd : 2 ≤ d)
(p : FiniteLpExponent)
:
∃ C < ⊤,
∀ (m n : ℤ) (hnm : n < m) (a : Ch02.CoeffOn (Ch02.cubeDomain (originCube d m))) (sigma0 : ℝ),
0 < sigma0 →
∀ (s : ↑FractionalOrder) (u v : H1Function (openCubeSet (originCube d m))),
IsCenteredCubeFluxBalanced m a sigma0 u v →
HasCenteredCubeH10Difference m u v →
centeredCubeFluxComparisonSmoothDualLHS m a sigma0 u v s p ≤ C * ENNReal.ofReal (Real.rpow 3 (↑s * ↑(m - n))) * centeredCubeLocalFluxDefectSmoothDualLpAverage m n hnm a sigma0 u s p