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

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

theorem HCPolySupport.real_le_of_forall_le_add_of_tendsto_zero {X A : ℝ} {T : ℕ → ℝ} (hT : Filter.Tendsto T Filter.atTop (nhds 0)) (h : ∀ (N : ℕ), X ≤ T N + A) : X ≤ A

theorem HCPolySupport.tendsto_pow_mul_of_nonneg_bddAbove {r : ℝ} {F : ℕ → ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hF_nonneg : ∀ (N : ℕ), 0 ≤ F N) (hF_bdd : BddAbove (Set.range F)) : Filter.Tendsto (fun (N : ℕ) => r ^ N * F N) Filter.atTop (nhds 0)

theorem HCPolySupport.coarsePoincareRHSDepthWeight_succ (s : ℝ) (n : ℕ) : coarsePoincareRHSDepthWeight s (n + 1) = coarsePoincareRHSStepDiscount s * coarsePoincareRHSDepthWeight s n

theorem HCPolySupport.coarsePoincareRHSDepthWeight_eq_rpow_mul_succ (s : ℝ) (n : ℕ) : coarsePoincareRHSDepthWeight s n = Real.rpow 3 s * coarsePoincareRHSDepthWeight s (n + 1)

theorem HCPolySupport.coarsePoincareRHSDepthWeight_mul_theta_pow_eq_scaledStepCoeff_mul (s θ : ℝ) (m N : ℕ) : coarsePoincareRHSDepthWeight s m * θ ^ N = coarsePoincareRHSScaledStepCoeff s θ ^ N * coarsePoincareRHSDepthWeight s (m + N)

theorem HCPolySupport.coarsePoincareRHSDepthWeight_mul_parentHalfCoeff_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : coarsePoincareRHSDepthWeight s (n + 1) * coarsePoincareRHSParentHalfCoeff Q a s (n + 1) = coarsePoincareRHSDepthWeight s n * coarsePoincareRHSParentHalfCoeff Q a s n

theorem HCPolySupport.coarsePoincareRHSParentHalfCoeff_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : coarsePoincareRHSParentHalfCoeff Q a s (n + 1) = Real.rpow 3 s * coarsePoincareRHSParentHalfCoeff Q a s n

theorem HCPolySupport.coarsePoincareRHSIntrinsicParentHalfForceMultiplier_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s (n + 1) = Real.rpow 3 s * coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n

theorem HCPolySupport.coarsePoincareRHSGlobalForceBound_succ {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) : coarsePoincareRHSGlobalForceBound Q g s (n + 1) = Real.rpow 3 (-2 * s) * coarsePoincareRHSGlobalForceBound Q g s n

theorem HCPolySupport.coarsePoincareRHSIntrinsicForceFactor_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) : coarsePoincareRHSDepthWeight s (n + 1) * (coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s (n + 1) ^ 2 * coarsePoincareRHSGlobalForceBound Q g s (n + 1)) = Real.rpow 3 (-s) * (coarsePoincareRHSDepthWeight s n * (coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n ^ 2 * coarsePoincareRHSGlobalForceBound Q g s n))

theorem HCPolySupport.coarsePoincareRHSWeightedDepthParentHalfCoeff_eq_base_mul_ratio_pow {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s θ : ℝ) (m k : ℕ) : coarsePoincareRHSScaledStepCoeff s θ ^ k * (coarsePoincareRHSDepthWeight s (m + k) * coarsePoincareRHSParentHalfCoeff Q a s (m + k)) = coarsePoincareRHSDepthWeight s m * coarsePoincareRHSParentHalfCoeff Q a s m * coarsePoincareRHSFiniteSumRatio s θ ^ k

theorem HCPolySupport.coarsePoincareRHSIntrinsicWeightedForceFactor_eq_base_mul_ratio_pow {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s θ : ℝ) (m k : ℕ) : coarsePoincareRHSScaledStepCoeff s θ ^ k * (coarsePoincareRHSDepthWeight s (m + k) * (coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s (m + k) ^ 2 * coarsePoincareRHSGlobalForceBound Q g s (m + k))) = coarsePoincareRHSDepthWeight s m * (coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s m ^ 2 * coarsePoincareRHSGlobalForceBound Q g s m) * coarsePoincareRHSForceFiniteSumRatio s θ ^ k