Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.AbsorbedErrors

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

theorem HCPolySupport.coarsePoincareRHSDepthWeight_mul_intrinsicWeightedLocalizedEnergyForceErrorSum_eq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s θ CE CF : ℝ) (B : ℕ → ℝ) (m N : ℕ) : coarsePoincareRHSDepthWeight s m * coarsePoincareRHSIntrinsicWeightedLocalizedEnergyForceErrorSum Q a u s θ CE CF B m N = coarsePoincareRHSSIntrinsicWeightedLocalizedEnergyForceErrorSum Q a u s θ CE CF B m N

theorem HCPolySupport.coarsePoincareRHSIntrinsicAbsorbedLocalError_eq_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) : coarsePoincareRHSIntrinsicAbsorbedLocalError Q a g u s η = coarsePoincareRHSAbsorbedEnergyCoeff η * coarsePoincareRHSIntrinsicLocalEnergyError Q a u s + coarsePoincareRHSAbsorbedRnCoeff η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + coarsePoincareRHSAbsorbedForceCoeff η * coarsePoincareRHSIntrinsicLocalForceError Q a g s

theorem HCPolySupport.coarsePoincareRHSIntrinsicAbsorbedErrorAverage_eq_componentAverages {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) (n : ℕ) : coarsePoincareRHSIntrinsicAbsorbedErrorAverage Q a g u s η n = coarsePoincareRHSAbsorbedEnergyCoeff η * coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n + coarsePoincareRHSAbsorbedRnCoeff η * coarsePoincareRHSRn Q s u n + coarsePoincareRHSAbsorbedForceCoeff η * coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n

theorem HCPolySupport.coarsePoincareRHSRn_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (n : ℕ) : 0 ≤ coarsePoincareRHSRn Q s u n

theorem HCPolySupport.coarsePoincareRHSSn_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (n : ℕ) : 0 ≤ coarsePoincareRHSSn Q s u n