Coarse-graining support:

Support.Deterministic.CoarsePoincareRHS.FinalTheorems.NoteStepAndConstants

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.sq_cubeBesovNegativeVectorSeminormTwo_le_intrinsicGlobalEnergyForce_noteConstants {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 (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R 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 ≤ coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s 5 0 * (5 * s⁻¹) + coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s (120 * s⁻¹) 0 * (5 * s⁻¹)

theorem HCPolySupport.sq_cubeBesovNegativeVectorSeminormTwo_le_intrinsicGlobalEnergyForce_noteConstants_expanded {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 (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R 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 {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 (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R 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