Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.FinalTheorems.ExpandedAndElliptic #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.sq_negativeBesovSeminormTwo_le_intrinsicGlobalEnergyForce
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s (coarsePoincareRHSNoteEta s))
:
cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2
theorem
HCPolySupport.coarsePoincareRHSSn_le_intrinsicGlobalEnergyForce_noteConstants_expanded_of_isEllipticFieldOn
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s (coarsePoincareRHSNoteEta s))
(m : ℕ)
:
coarsePoincareRHSSn Q s u m ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2
theorem
HCPolySupport.negativeBesovSeminormTwo_le_sqrt_intrinsicGlobalEnergyForce
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s (coarsePoincareRHSNoteEta s))
:
cubeBesovNegativeVectorSeminormTwo Q s u ≤ √(250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)
theorem
HCPolySupport.sq_negativeBesovSeminormTwo_le_intrinsicGlobalEnergyForce_of_parent_potential
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu_potential : IsPotentialOn (cubeSet Q) u)
(hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
:
cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2
theorem
HCPolySupport.negativeBesovSeminormTwo_le_sqrt_intrinsicGlobalEnergyForce_of_parent_potential
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu_potential : IsPotentialOn (cubeSet Q) u)
(hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
:
cubeBesovNegativeVectorSeminormTwo Q s u ≤ √(250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)
theorem
HCPolySupport.coarsePoincareRHSSn_le_intrinsicGlobalEnergyForce
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu_potential : IsPotentialOn (cubeSet Q) u)
(hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(m : ℕ)
:
coarsePoincareRHSSn Q s u m ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u) + 15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2