Coarse-graining support:

Support.Deterministic.CoarsePoincareRHS.AveragedLocal.ComponentBoundsBasic

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

theorem HCPolySupport.coarsePoincareRHSRn_le_discount_next_add_intrinsicAbsorbedErrorAverage_of_localBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) (n : ℕ) (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 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn Q s u (n + 1) + coarsePoincareRHSIntrinsicAbsorbedErrorAverage Q a g u s η n

theorem HCPolySupport.coarsePoincareRHSRn_le_intrinsicComponentErrors_of_localBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) (n : ℕ) (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 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn Q s u (n + 1) + (coarsePoincareRHSAbsorbedEnergyCoeff η * coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n + coarsePoincareRHSAbsorbedRnCoeff η * coarsePoincareRHSRn Q s u n + coarsePoincareRHSAbsorbedForceCoeff η * coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n)

theorem HCPolySupport.coarsePoincareRHSRn_intrinsicAbsorptionReady_le_of_localBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) (n : ℕ) (hlocal : ∀ R ∈ descendantsAtDepth Q n, cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η) : (1 - coarsePoincareRHSAbsorbedRnCoeff η) * coarsePoincareRHSRn Q s u n ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn Q s u (n + 1) + coarsePoincareRHSAbsorbedEnergyCoeff η * coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n + coarsePoincareRHSAbsorbedForceCoeff η * coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n

theorem HCPolySupport.coarsePoincareRHSRn_le_invAbsorptionCoeff_mul_intrinsicErrors_of_localBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) (n : ℕ) (habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η) (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 ≤ (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * (coarsePoincareRHSDiscount s * coarsePoincareRHSRn Q s u (n + 1) + coarsePoincareRHSAbsorbedEnergyCoeff η * coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n + coarsePoincareRHSAbsorbedForceCoeff η * coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n)

theorem HCPolySupport.coarsePoincareRHSRn_le_intrinsicComponentBounds_of_localBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) (n : ℕ) {θ CE CF : ℝ} (habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η) (hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ) (hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE) (hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF) (hnext_nonneg : 0 ≤ coarsePoincareRHSRn Q s u (n + 1)) (hE_nonneg : 0 ≤ coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n) (hF_nonneg : 0 ≤ coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n) (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 * coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n + CF * coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n