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

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

theorem HCPolySupport.coarsePoincareRHSNoteStepCoeff_nonneg (s : ℝ) : 0 ≤ coarsePoincareRHSNoteStepCoeff s

theorem HCPolySupport.coarsePoincareRHSFiniteSumRatio_noteStepCoeff_eq (s : ℝ) : coarsePoincareRHSFiniteSumRatio s (coarsePoincareRHSNoteStepCoeff s) = Real.rpow 3 (-s / 2)

theorem HCPolySupport.coarsePoincareRHSForceFiniteSumRatio_noteStepCoeff_eq (s : ℝ) : coarsePoincareRHSForceFiniteSumRatio s (coarsePoincareRHSNoteStepCoeff s) = Real.rpow 3 (-(3 * s / 2))

theorem HCPolySupport.coarsePoincareRHSFiniteSumRatio_noteStepCoeff_nonneg (s : ℝ) : 0 ≤ coarsePoincareRHSFiniteSumRatio s (coarsePoincareRHSNoteStepCoeff s)

theorem HCPolySupport.coarsePoincareRHSFiniteSumRatio_noteStepCoeff_lt_one {s : ℝ} (hs : 0 < s) : coarsePoincareRHSFiniteSumRatio s (coarsePoincareRHSNoteStepCoeff s) < 1

theorem HCPolySupport.coarsePoincareRHSForceFiniteSumRatio_nonneg_of_finiteSumRatio_nonneg {s θ : ℝ} (hr_nonneg : 0 ≤ coarsePoincareRHSFiniteSumRatio s θ) : 0 ≤ coarsePoincareRHSForceFiniteSumRatio s θ

theorem HCPolySupport.coarsePoincareRHSForceFiniteSumRatio_lt_one_of_finiteSumRatio_lt_one {s θ : ℝ} (hs : 0 < s) (hr_nonneg : 0 ≤ coarsePoincareRHSFiniteSumRatio s θ) (hr_lt_one : coarsePoincareRHSFiniteSumRatio s θ < 1) : coarsePoincareRHSForceFiniteSumRatio s θ < 1

theorem HCPolySupport.coarsePoincareRHSNoteEta_pos {s : ℝ} (hs : 0 < s) : 0 < coarsePoincareRHSNoteEta s

theorem HCPolySupport.coarsePoincareRHSNoteEta_lt_half {s : ℝ} (hs : 0 < s) : coarsePoincareRHSNoteEta s < 1 / 2

theorem HCPolySupport.one_sub_coarsePoincareRHSAbsorbedRnCoeff_noteEta_eq {s : ℝ} (hs : 0 < s) : 1 - coarsePoincareRHSAbsorbedRnCoeff (coarsePoincareRHSNoteEta s) = Real.rpow 3 (-s / 2)

theorem HCPolySupport.one_sub_coarsePoincareRHSAbsorbedRnCoeff_noteEta_pos {s : ℝ} (hs : 0 < s) : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff (coarsePoincareRHSNoteEta s)

theorem HCPolySupport.coarsePoincareRHSAbsorbedEnergyCoeff_noteEta_eq {s : ℝ} (hs : 0 < s) : coarsePoincareRHSAbsorbedEnergyCoeff (coarsePoincareRHSNoteEta s) = 2 - Real.rpow 3 (-s / 2)

theorem HCPolySupport.coarsePoincareRHSNoteEnergyEnvelope_eq {s : ℝ} (hs : 0 < s) : coarsePoincareRHSNoteEnergyEnvelope s = (Real.rpow 3 (-s / 2))⁻¹ * (2 - Real.rpow 3 (-s / 2))

theorem HCPolySupport.coarsePoincareRHSAbsorbedForceCoeff_noteEta_eq {s : ℝ} (hs : 0 < s) : coarsePoincareRHSAbsorbedForceCoeff (coarsePoincareRHSNoteEta s) = 2 * (2 - Real.rpow 3 (-s / 2)) + 2 * (2 - Real.rpow 3 (-s / 2)) * (1 - Real.rpow 3 (-s / 2))⁻¹

theorem HCPolySupport.coarsePoincareRHSNoteForceEnvelope_eq {s : ℝ} (hs : 0 < s) : coarsePoincareRHSNoteForceEnvelope s = (Real.rpow 3 (-s / 2))⁻¹ * (2 * (2 - Real.rpow 3 (-s / 2)) + 2 * (2 - Real.rpow 3 (-s / 2)) * (1 - Real.rpow 3 (-s / 2))⁻¹)

theorem HCPolySupport.inv_rpow_three_neg_half_eq_rpow_half (s : ℝ) : (Real.rpow 3 (-s / 2))⁻¹ = Real.rpow 3 (s / 2)

theorem HCPolySupport.rpow_three_half_mul_rpow_three_neg_half_eq_one (s : ℝ) : Real.rpow 3 (s / 2) * Real.rpow 3 (-s / 2) = 1

theorem HCPolySupport.coarsePoincareRHSNoteEnergyEnvelope_eq_two_mul_rpow_half_sub_one {s : ℝ} (hs : 0 < s) : coarsePoincareRHSNoteEnergyEnvelope s = 2 * Real.rpow 3 (s / 2) - 1

theorem HCPolySupport.coarsePoincareRHSNoteForceEnvelope_eq_rpow_half_mul {s : ℝ} (hs : 0 < s) : coarsePoincareRHSNoteForceEnvelope s = Real.rpow 3 (s / 2) * (2 * (2 - Real.rpow 3 (-s / 2)) + 2 * (2 - Real.rpow 3 (-s / 2)) * (1 - Real.rpow 3 (-s / 2))⁻¹)

theorem HCPolySupport.rpow_three_half_le_three_of_le_two {s : ℝ} (hs_le : s ≤ 2) : Real.rpow 3 (s / 2) ≤ 3

theorem HCPolySupport.coarsePoincareRHSNoteEnergyEnvelope_le_five {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 2) : coarsePoincareRHSNoteEnergyEnvelope s ≤ 5

theorem HCPolySupport.coarsePoincareRHSNoteForceEnvelope_le_twentyfour_mul_inv_one_sub {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 2) : coarsePoincareRHSNoteForceEnvelope s ≤ 24 * (1 - Real.rpow 3 (-s / 2))⁻¹

theorem HCPolySupport.one_half_le_log_three : 1 / 2 ≤ Real.log 3

theorem HCPolySupport.inv_one_sub_rpow_three_neg_half_le_five_inv {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : (1 - Real.rpow 3 (-s / 2))⁻¹ ≤ 5 * s⁻¹

theorem HCPolySupport.inv_one_sub_rpow_three_neg_three_half_le_five_inv {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : (1 - Real.rpow 3 (-(3 * s / 2)))⁻¹ ≤ 5 * s⁻¹

theorem HCPolySupport.inv_one_sub_rpow_three_neg_le_five_inv {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : (1 - Real.rpow 3 (-s))⁻¹ ≤ 5 * s⁻¹

theorem HCPolySupport.inv_geometricDiscount_two_le_five_inv {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : (geometricDiscount s 2)⁻¹ ≤ 5 * s⁻¹

theorem HCPolySupport.coarsePoincareRHSNoteForceEnvelope_le_oneTwenty_mul_inv {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : coarsePoincareRHSNoteForceEnvelope s ≤ 120 * s⁻¹

theorem HCPolySupport.coarsePoincareRHS_noteEta_discount_le_noteStepCoeff {s : ℝ} (hs : 0 < s) : (1 - coarsePoincareRHSAbsorbedRnCoeff (coarsePoincareRHSNoteEta s))⁻¹ * coarsePoincareRHSDiscount s ≤ coarsePoincareRHSNoteStepCoeff s