Coarse-graining support:

Support.Deterministic.CoarsePoincareRHS.AveragedLocal.LocalizedEnergyForce

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

theorem HCPolySupport.coarsePoincareRHSRn_le_intrinsicLocalizedEnergyForce_of_localBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) {s lam Lam η : ℝ} (n : ℕ) {θ CE CF B : ℝ} (hs : 0 < s) (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) (habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η) (hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ) (hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE) (hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF) (hCE_nonneg : 0 ≤ CE) (hCF_nonneg : 0 ≤ CF) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => coarsePoincareRHSLocalCenteredForceSeminorm R g s ^ 2) ≤ B) (hlocal : ∀ R ∈ descendantsAtDepth Q n, cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η) : coarsePoincareRHSRn Q s u n ≤ θ * coarsePoincareRHSRn Q s u (n + 1) + CE * (2 * coarsePoincareRHSParentHalfCoeff Q a s n * cubeAverage Q (coefficientEnergyDensity a u)) + CF * (coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n ^ 2 * B)

theorem HCPolySupport.coarsePoincareRHSRn_le_intrinsicLocalizedEnergyForce_of_forceAverageBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) {s lam Lam η : ℝ} (n : ℕ) {θ CE CF B : ℝ} (hs : 0 < s) (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) (habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η) (hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ) (hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE) (hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF) (hCE_nonneg : 0 ≤ CE) (hCF_nonneg : 0 ≤ CF) (havg_nonneg : ∀ 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)) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ B) (hlocal : ∀ R ∈ descendantsAtDepth Q n, cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η) : coarsePoincareRHSRn Q s u n ≤ θ * coarsePoincareRHSRn Q s u (n + 1) + CE * (2 * coarsePoincareRHSParentHalfCoeff Q a s n * cubeAverage Q (coefficientEnergyDensity a u)) + CF * (coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n ^ 2 * B)