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

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

Scale geometry for Section 5.7 bad-pair estimates

This file records the elementary arithmetic facts used to simplify the deterministic scales after shifting by the annealed entry scale.

theorem HCPolySupport.Book.Ch05.Section57.nat_cast_add_sub_of_le {q m : ℕ} (hqm : q ≤ m) : ↑q + ↑(m - q) = ↑m

theorem HCPolySupport.Book.Ch05.Section57.nat_cast_sub_add_sub_of_le {n q m : ℕ} (hnq : n ≤ q) (hqm : q ≤ m) : ↑(m - q) + ↑(q - n) = ↑(m - n)

theorem HCPolySupport.Book.Ch05.Section57.int_toNat_nat_add_sub_nat_add_of_le {N n ℓ : ℕ} (hℓn : ℓ ≤ n) : (↑(N + n) - ↑(N + ℓ)).toNat = n - ℓ

theorem HCPolySupport.Book.Ch05.Section57.descendantsAtScale_originCube_nat_shift_card {d N m n : ℕ} (hnm : n ≤ m) : (descendantsAtScale (originCube d ↑(N + m)) ↑(N + n)).card = (3 ^ d) ^ (m - n)

theorem HCPolySupport.Book.Ch05.Section57.descendantsAtScale_originCube_nat_card {d m n : ℕ} (hnm : n ≤ m) : (descendantsAtScale (originCube d ↑m) ↑n).card = (3 ^ d) ^ (m - n)

theorem HCPolySupport.Book.Ch05.Section57.log_descendantsAtScale_originCube_nat_shift_card {d N m n : ℕ} (hnm : n ≤ m) : Real.log ↑(descendantsAtScale (originCube d ↑(N + m)) ↑(N + n)).card = ↑(m - n) * Real.log ↑(3 ^ d)

theorem HCPolySupport.Book.Ch05.Section57.log_descendantsAtScale_originCube_nat_card {d m n : ℕ} (hnm : n ≤ m) : Real.log ↑(descendantsAtScale (originCube d ↑m) ↑n).card = ↑(m - n) * Real.log ↑(3 ^ d)

theorem HCPolySupport.Book.Ch05.Section57.three_mul_log_three_pow_dim_pos {d : ℕ} [NeZero d] : 0 < 3 * Real.log ↑(3 ^ d)

theorem HCPolySupport.Book.Ch05.Section57.three_mul_log_normalizedProbeIndex_univ_card_pos {d : ℕ} [NeZero d] : 0 < 3 * Real.log ↑Finset.univ.card

theorem HCPolySupport.Book.Ch05.Section57.three_mul_log_descendantsAtScale_originCube_nat_shift_card_eq {d N m n : ℕ} (hnm : n ≤ m) : 3 * Real.log ↑(descendantsAtScale (originCube d ↑(N + m)) ↑(N + n)).card = ↑(m - n) * (3 * Real.log ↑(3 ^ d))

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_mul_log_descendantsAtScale_originCube_nat_shift_card {d : ℕ} [NeZero d] {τ : ℝ} {N m n : ℕ} (hnm : n < m) : (3 * Real.log ↑(descendantsAtScale (originCube d ↑(N + m)) ↑(N + n)).card) ^ τ⁻¹ = ↑(m - n) ^ τ⁻¹ * (3 * Real.log ↑(3 ^ d)) ^ τ⁻¹

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_mul_log_descendantsAtScale_originCube_nat_shift_card_le_parent {d : ℕ} [NeZero d] {τ : ℝ} (hτ : 0 < τ) {N m n : ℕ} (hnm : n < m) : (3 * Real.log ↑(descendantsAtScale (originCube d ↑(N + m)) ↑(N + n)).card) ^ τ⁻¹ ≤ ↑m ^ τ⁻¹ * (3 * Real.log ↑(3 ^ d)) ^ τ⁻¹

theorem HCPolySupport.Book.Ch05.Section57.shiftedEnvelopeDenominator_le_parentPower {d : ℕ} [NeZero d] {τ R K C θ : ℝ} (hτ : 0 < τ) (hR : 0 ≤ R) (hK : 0 ≤ K) (hC : 0 ≤ C) {N m n : ℕ} (hnm : n < m) : have D := descendantsAtScale (originCube d ↑(N + m)) ↑(N + n); have S := Finset.univ; R * (K * ((3 * Real.log ↑S.card) ^ τ⁻¹ * ((3 * Real.log ↑D.card) ^ τ⁻¹ * (C * θ ^ 2)))) ≤ R * (K * ((3 * Real.log ↑S.card) ^ τ⁻¹ * ((3 * Real.log ↑(3 ^ d)) ^ τ⁻¹ * (C * θ ^ 2)))) * ↑m ^ τ⁻¹

theorem HCPolySupport.Book.Ch05.Section57.shiftedEnvelopeDenominator_le_parentAddOnePower {d : ℕ} [NeZero d] {τ R K C θ : ℝ} (hτ : 0 < τ) (hR : 0 ≤ R) (hK : 0 ≤ K) (hC : 0 ≤ C) {N m n : ℕ} (hnm : n < m) : have D := descendantsAtScale (originCube d ↑(N + m)) ↑(N + n); have S := Finset.univ; R * (K * ((3 * Real.log ↑S.card) ^ τ⁻¹ * ((3 * Real.log ↑D.card) ^ τ⁻¹ * (C * θ ^ 2)))) ≤ R * (K * ((3 * Real.log ↑S.card) ^ τ⁻¹ * ((3 * Real.log ↑(3 ^ d)) ^ τ⁻¹ * (C * θ ^ 2)))) * (↑m + 1) ^ τ⁻¹