Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.LocalNoteTerms.Intrinsic #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativeBesovSeminormTwo_le_descendantMean_add_intrinsicError_two
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
{η : ℝ}
(hs : 0 < s)
(hη : 0 < η)
(hη_lt : η < 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
(hchildBdd :
∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u))
:
cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorSeminormTwo R s u ^ 2) + coarsePoincareRHSIntrinsicAbsorbedLocalError Q a g u s η
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.negativeBesovSeminormSquare_le_discount_add_intrinsicError
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{n : ℕ}
{a : CoeffField d}
{g u : Vec d → Vec d}
{lam Lam s : ℝ}
(hs : 0 < s)
(hu_potential : IsPotentialOn (cubeSet Q) u)
(hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x)
(hR : R ∈ descendantsAtDepth Q n)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hLocalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g))
:
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s (coarsePoincareRHSNoteEta s)