Coarse-graining support: Support.Book.Ch05.Theorems.Section57.ScaleCompression

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

Deterministic scale compression

This file contains scalar estimates used to compress the explicit quantitative minimal-scale threshold to the manuscript exp(C log^2(2 + thetaHat)) form.

theorem HCPolySupport.Book.Ch05.Section57.log_max_one_le_log_two_add {θ : ℝ} (hθ : 0 ≤ θ) : Real.log (max 1 θ) ≤ Real.log (2 + θ)

theorem HCPolySupport.Book.Ch05.Section57.log_two_add_sq_ge_quarter {θ : ℝ} (hθ : 0 ≤ θ) : 1 / 4 ≤ Real.log (2 + θ) ^ 2

theorem HCPolySupport.Book.Ch05.Section57.log_two_add_le_two_mul_sq {θ : ℝ} (hθ : 0 ≤ θ) : Real.log (2 + θ) ≤ 2 * Real.log (2 + θ) ^ 2

theorem HCPolySupport.Book.Ch05.Section57.rpow_max_one_le_exp_logSq {θ p : ℝ} (hθ : 0 ≤ θ) (hp : 0 ≤ p) : max 1 θ ^ p ≤ Real.exp (2 * p * Real.log (2 + θ) ^ 2)

theorem HCPolySupport.Book.Ch05.Section57.const_mul_rpow_max_one_le_exp_logSq {A θ p : ℝ} (hA : 0 < A) (hθ : 0 ≤ θ) (hp : 0 ≤ p) : A * max 1 θ ^ p ≤ Real.exp ((4 * max 0 (Real.log A) + 2 * p) * Real.log (2 + θ) ^ 2)

theorem HCPolySupport.Book.Ch05.Section57.max_one_mul_sq_le_const_mul_max_one_sq {A θ : ℝ} (hθ : 0 ≤ θ) : max 1 (A * θ ^ 2) ≤ max 1 A * max 1 θ ^ 2

theorem HCPolySupport.Book.Ch05.Section57.rpow_max_one_mul_sq_le_const_mul_rpow {A θ r : ℝ} (hθ : 0 ≤ θ) (hr : 0 ≤ r) : max 1 (A * θ ^ 2) ^ r ≤ max 1 A ^ r * max 1 θ ^ (2 * r)

theorem HCPolySupport.Book.Ch05.Section57.rpow_max_one_le_rpow_max_one_of_exponent_le {θ p q : ℝ} (hpq : p ≤ q) : max 1 θ ^ p ≤ max 1 θ ^ q

theorem HCPolySupport.Book.Ch05.Section57.mixedBottomTailDenominator_mul_sq_le_const_mul_rpow {A B θ η τ σ : ℝ} (hθ : 0 ≤ θ) (hη : 0 < η) (hτ : 0 ≤ τ) (hσ : 0 ≤ σ) : have rτ := τ / η; have rσ := σ / η; have C := max (max 1 A ^ rτ) (max 1 B ^ rσ); mixedBottomTailDenominator (A * θ ^ 2) (B * θ ^ 2) η τ σ ≤ C * max 1 θ ^ (2 * max rτ rσ)

theorem HCPolySupport.Book.Ch05.Section57.selectedBlead_mul_sq_le_const_mul_rpow {A B θ η τ σ U V : ℝ} (hθ : 0 ≤ θ) (hη : 0 < η) (hτ : 0 ≤ τ) (hσ : 0 ≤ σ) (hU : 0 ≤ U) (hV : 0 ≤ V) : have rτ := τ / η; have rσ := σ / η; have Cden := max (max 1 A ^ rτ) (max 1 B ^ rσ); have p := 2 * max rτ rσ; have C := Cden * max U V; max (mixedBottomTailDenominator (A * θ ^ 2) (B * θ ^ 2) η τ σ * U) (mixedBottomTailDenominator (A * θ ^ 2) (B * θ ^ 2) η τ σ * V) ≤ C * max 1 θ ^ p

theorem HCPolySupport.Book.Ch05.Section57.two_rpow_neg_lt_one {η : ℝ} (hη : 0 < η) : 2 ^ (-η) < 1

theorem HCPolySupport.Book.Ch05.Section57.gap_two_mul_rpow_eq {B η : ℝ} (hB : 0 < B) : B ^ (-η) - (2 * B) ^ (-η) = B ^ (-η) * (1 - 2 ^ (-η))

theorem HCPolySupport.Book.Ch05.Section57.gap_two_mul_rpow_pos {B η : ℝ} (hB : 0 < B) (hη : 0 < η) : 0 < B ^ (-η) - (2 * B) ^ (-η)

theorem HCPolySupport.Book.Ch05.Section57.max_zero_neg_log_gap_two_mul_le {B η : ℝ} (hB : 1 ≤ B) (hη : 0 < η) : max 0 (-Real.log (B ^ (-η) - (2 * B) ^ (-η))) ≤ η * Real.log B + max 0 (-Real.log (1 - 2 ^ (-η)))

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_natCeil_le_three_mul_exp {y : ℝ} (hy : 0 ≤ y) : Real.rpow 3 ↑⌈y⌉₊ ≤ 3 * Real.exp (Real.log 3 * y)

theorem HCPolySupport.Book.Ch05.Section57.pow_three_natCeil_le_three_mul_exp {y : ℝ} (hy : 0 ≤ y) : 3 ^ ⌈y⌉₊ ≤ 3 * Real.exp (Real.log 3 * y)