Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.DiscountBounds

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

Finite-exponent multiscale ellipticity: discount scalar bounds

theorem HCPolySupport.Book.Ch02.book_geometricDiscount_nonneg {s q : ℝ} (hsq : 0 ≤ s * q) : 0 ≤ geometricDiscount s q

theorem HCPolySupport.Book.Ch02.book_geometricDiscount_pos {s q : ℝ} (hsq : 0 < s * q) : 0 < geometricDiscount s q

theorem HCPolySupport.Book.Ch02.geometricDiscount_le_two_mul {s q : ℝ} (hsq : 0 ≤ s * q) : geometricDiscount s q ≤ 2 * (s * q)

theorem HCPolySupport.Book.Ch02.two_mul_self_rpow_two_div_le_exp_four {q : ℝ} (hq : 1 ≤ q) : (2 * q).rpow (2 / q) ≤ Real.exp 4

theorem HCPolySupport.Book.Ch02.geometricDiscount_rpow_two_div_le_exp_four_mul {s q : ℝ} (hs : 0 < s) (hq : 1 ≤ q) : (geometricDiscount s q).rpow (2 / q) ≤ Real.exp 4 * s.rpow (2 / q)

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

theorem HCPolySupport.Book.Ch02.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.Book.Ch02.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.Book.Ch02.inv_geometricDiscount_le_five_inv {s p : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hp : 1 ≤ p) : (geometricDiscount s p)⁻¹ ≤ 5 * s⁻¹

theorem HCPolySupport.Book.Ch02.geometricDiscount_rpow_neg_two_div_le_twentyFive_mul {s p : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hp : 1 ≤ p) : (geometricDiscount s p).rpow (-2 / p) ≤ 25 * s.rpow (-2 / p)

theorem HCPolySupport.Book.Ch02.geometricDiscount_change_exponent_factor_le {s p q : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hp : 1 ≤ p) (hpq : p ≤ q) : (geometricDiscount s q).rpow (2 / q) * (geometricDiscount s p).rpow (-2 / p) ≤ 25 * Real.exp 4 * s.rpow (2 / q - 2 / p)