Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.LocalStep.HarmonicStepping #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_cubeBesovNegativeVectorPartialSeminormTwo_succ_le_descendantsAverage_add_harmonic_zero
{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))
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(N : ℕ)
(s : ℝ)
:
cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + (cubeBesovNegativeVectorPartialSeminormTwo Q s 0 fun (x : Vec d) => w.toH1.grad x) ^ 2
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_cubeBesovNegativeVectorPartialSeminormTwo_succ_le_descendantsAverage_add_harmonic_energy
{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))
(s : ℝ)
(hs : 0 < s)
(N : ℕ)
(energy : Vec d → ℝ)
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hgrad : CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x) energy)
(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)
:
cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + (geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q energy
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeAverage_coefficientEnergyDensity_harmonic_le_two_mul_add
{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 : ℝ}
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hu : MemVectorL2 (cubeSet Q) u)
:
cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x) ≤ 2 * cubeAverage Q (coefficientEnergyDensity a u) + 2 * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x)
Coefficient-energy version of the elementary split estimate
w = u - grad rho.
This is the local algebraic replacement for the older Euclidean
vecNormSq split. The ellipticity hypotheses only certify that the
symmetric coefficient quadratic form is non-negative/integrable; the estimate
itself has the universal constant 2.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativePartialSeminormTwo_succ_le_childMean_add_energy_add_correctorEnergy
{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)
(N : ℕ)
(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)
:
cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativePartialSeminormTwo_succ_le_childMean_add_energy
{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)
(N : ℕ)
(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)
{Eρ : ℝ}
(hρenergy : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ Eρ)
:
cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * Eρ