Coarse-graining support: Support.Deterministic.WeakFluxRHS.FluxStepping #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.MeanZeroNeumannCorrectorData.sq_cubeBesovNegativeVectorPartialSeminormTwo_flux_succ_le_descendantsAverage_add_harmonic_zero
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu_mem : MemVectorL2 (cubeSet Q) u)
(hg : MemVectorL2 (cubeSet Q) g)
(N : ℕ)
(s : ℝ)
:
(cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) =>
(cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + (cubeBesovNegativeVectorPartialSeminormTwo Q s 0 fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) ^ 2
Flux version of the elementary local step: after subtracting the centered Neumann corrector, the top-scale flux average is the harmonic remainder's flux average.
theorem
HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeVectorPartial_flux_succ_le_descendantsEnergy
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
(s : ℝ)
(hs : 0 < s)
(N : ℕ)
(energy : Vec d → ℝ)
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu_mem : MemVectorL2 (cubeSet Q) u)
(hg : MemVectorL2 (cubeSet Q) g)
(henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x)
(henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume)
(hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) energy)
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x)
:
(cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) =>
(cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + (geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * cubeAverage Q energy
Flux local step with the harmonic top-scale term bounded by the q = 2
flux coarse Poincare energy control.