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

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

theorem HCPolySupport.coarsePoincareRHSParentHalfCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) (n : ℕ) : 0 ≤ coarsePoincareRHSParentHalfCoeff Q a s n

theorem HCPolySupport.coarsePoincareRHSGlobalForceBound_nonneg {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) : 0 ≤ coarsePoincareRHSGlobalForceBound Q g s n

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalEnergyBase_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s CE : ℝ} (hs : 0 < s) (hCE_nonneg : 0 ≤ CE) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (m : ℕ) : 0 ≤ coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE m

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalEnergyBase_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s CE : ℝ) (n : ℕ) : coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE (n + 1) = coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE n

The depth-scaled global energy base is independent of the starting depth.

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalEnergyBase_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s CE : ℝ) (m : ℕ) : coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE m = coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE 0

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalEnergyBase_zero_noteConstants_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) : coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s 5 0 * (5 * s⁻¹) ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u)

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalEnergyBase_noteConstants_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (m : ℕ) : coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s 5 m * (5 * s⁻¹) ≤ 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a u)

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalForceBase_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) {CF : ℝ} (hCF_nonneg : 0 ≤ CF) (m : ℕ) : 0 ≤ coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF m

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalForceBase_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s CF : ℝ) (n : ℕ) : coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF (n + 1) = Real.rpow 3 (-s) * coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF n

The depth-scaled global force base decays by one 3^{-s} factor.

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalForceBase_le_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s CF : ℝ} (hs_nonneg : 0 ≤ s) (hCF_nonneg : 0 ≤ CF) (m : ℕ) : coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF m ≤ coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF 0

theorem HCPolySupport.coarsePoincareRHSSIntrinsicGlobalForceBase_zero_noteConstants_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s (120 * s⁻¹) 0 * (5 * s⁻¹) ≤ 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.coarsePoincareRHSSIntrinsicGlobalForceBase_noteConstants_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (m : ℕ) : coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s (120 * s⁻¹) m * (5 * s⁻¹) ≤ 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.coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum_eq_base_mul_geomSum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s θ CE : ℝ) (m N : ℕ) : coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum Q a u s θ CE m N = coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE m * ∑ k ∈ Finset.range N, coarsePoincareRHSFiniteSumRatio s θ ^ k

theorem HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum_le_base_mul_inv_one_sub {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s θ CE : ℝ) (m N : ℕ) (hr_nonneg : 0 ≤ coarsePoincareRHSFiniteSumRatio s θ) (hr_lt_one : coarsePoincareRHSFiniteSumRatio s θ < 1) (hbase_nonneg : 0 ≤ coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE m) : coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum Q a u s θ CE m N ≤ coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE m * (1 - coarsePoincareRHSFiniteSumRatio s θ)⁻¹

theorem HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum_le_base_mul_inv_one_sub_of_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s θ CE : ℝ} (m N : ℕ) (hs : 0 < s) (hCE_nonneg : 0 ≤ CE) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (hr_nonneg : 0 ≤ coarsePoincareRHSFiniteSumRatio s θ) (hr_lt_one : coarsePoincareRHSFiniteSumRatio s θ < 1) : coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum Q a u s θ CE m N ≤ coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s CE m * (1 - coarsePoincareRHSFiniteSumRatio s θ)⁻¹

theorem HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum_eq_base_mul_geomSum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s θ CF : ℝ) (m N : ℕ) : coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum Q a g s θ CF m N = coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF m * ∑ k ∈ Finset.range N, coarsePoincareRHSForceFiniteSumRatio s θ ^ k

theorem HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum_le_base_mul_inv_one_sub {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s θ CF : ℝ) (m N : ℕ) (hr_nonneg : 0 ≤ coarsePoincareRHSForceFiniteSumRatio s θ) (hr_lt_one : coarsePoincareRHSForceFiniteSumRatio s θ < 1) (hbase_nonneg : 0 ≤ coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF m) : coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum Q a g s θ CF m N ≤ coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF m * (1 - coarsePoincareRHSForceFiniteSumRatio s θ)⁻¹

theorem HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum_le_base_mul_inv_one_sub_of_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s θ CF : ℝ} (m N : ℕ) (hCF_nonneg : 0 ≤ CF) (hr_nonneg : 0 ≤ coarsePoincareRHSForceFiniteSumRatio s θ) (hr_lt_one : coarsePoincareRHSForceFiniteSumRatio s θ < 1) : coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum Q a g s θ CF m N ≤ coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s CF m * (1 - coarsePoincareRHSForceFiniteSumRatio s θ)⁻¹