Scale arithmetic for e.left.to.show

Source: enhance.tex 7250-7320 (e.kappam, e.expqunt, e.corrm), 8466-8510 (flux-size step), 8780-8830 (τ''/τ'), 8588-8630 (ergodic exponent). Pure parameter lemmas: the two-sided bounds of the l_recurse for m < M are combined with the one-sided terminal estimate l_recurse_top at m = M.

theorem AVenhance.Infra.Section5.LeftToShow.Scales.eps_pos {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} : 0 < epsilon β Λ m

theorem AVenhance.Infra.Section5.LeftToShow.Scales.eps_le_one {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} : epsilon β Λ m ≤ 1

theorem AVenhance.Infra.Section5.LeftToShow.Scales.supergeoConstant_nonneg {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 ≤ Ingredients.supergeoConstant β

theorem AVenhance.Infra.Section5.LeftToShow.Scales.gamma_lt_beta {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : gamma β < β

theorem AVenhance.Infra.Section5.LeftToShow.Scales.a_mul_rpow_eq {β : ℝ} {Λ m : ℕ} (hx : 0 < epsilon β Λ m) (γ : ℝ) : a β Λ m * epsilon β Λ m ^ (2 + γ) = epsilon β Λ m ^ (β + γ)

a_m ε_m^(2+γ) = ε_m^(β+γ).

theorem AVenhance.Infra.Section5.LeftToShow.Scales.a_mul_sq_eq {β : ℝ} {Λ m : ℕ} (hx : 0 < epsilon β Λ m) : a β Λ m * epsilon β Λ m ^ 2 = epsilon β Λ m ^ β

a_m ε_m² = ε_m^β.

theorem AVenhance.Infra.Section5.LeftToShow.Scales.amplitude_div_scale {β x γ c : ℝ} (hx : 0 < x) (hc : 0 < c) : (x ^ (β - 2)) ^ 2 * x ^ 4 / (c * x ^ (β + γ)) = 1 / c * x ^ (β - γ)

theorem AVenhance.Infra.Section5.LeftToShow.Scales.eps_le_const_mul_pred_pow {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 2 ≤ m) : epsilon β Λ m ≤ (1 + Ingredients.supergeoConstant β) * epsilon β Λ (m - 1) ^ q β

Successive scales: ε_m ≤ (1 + A) ε_{m-1}^q for m ≥ 2.

theorem AVenhance.Infra.Section5.LeftToShow.Scales.length_power_pred {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 2 ≤ m) : epsilon β Λ m ^ (β - gamma β) ≤ (1 + Ingredients.supergeoConstant β) ^ (β - gamma β) * epsilon β Λ (m - 1) ^ (β + gamma β)

ε_m^{β-γ} ≤ (1+A)^{β-γ} ε_{m-1}^{β+γ}.

noncomputable def AVenhance.Infra.Section5.LeftToShow.Scales.scalesK (β c C : ℝ) : ℝ

The explicit scale constant of left_to_show_scales, depending only on β and the l_recurse constants c < C.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.LeftToShow.Scales.kappaPrimeEndpointExpratConstant_nonneg {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 ≤ Section3.kappaPrimeEndpointExpratConstant β

theorem AVenhance.Infra.Section5.LeftToShow.Scales.scalesK_ge_one {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {c C : ℝ} (hc : 0 < c) (hcC : c < C) : 1 ≤ scalesK β c C

theorem AVenhance.Infra.Section5.LeftToShow.Scales.scales_core {β : ℝ} (I : Ingredients β) {c C : ℝ} (hc : 0 < c) (hcC : c < C) {κ : ℝ} (hκ : 0 < κ) {M : ℕ} (hM : 1 ≤ M) (hperm : κ ∈ permittedInterval β I.Λ M) (hA5 : ∀ (m : ℕ), 1 ≤ m → m < M → c * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β)) ≤ I.kappaAt κ m (M - m) ∧ I.kappaAt κ m (M - m) ≤ C * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β))) (hA5' : ∀ (m : ℕ), 2 ≤ m → m < M → epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ≤ C * epsilon β I.Λ (m - 1) ^ (4 * delta β)) {m : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) : 0 < I.kappaSeq κ M m ∧ I.kappaSeq κ M m ≤ I.kappaSeq κ M (m - 1) ∧ I.kappaSeq κ M (m - 1) ≤ scalesK β c C ∧ a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaSeq κ M m ≤ scalesK β c C * I.kappaSeq κ M (m - 1) ∧ epsilon β I.Λ m ^ 2 / (I.kappaSeq κ M m * tau β I.Λ m) ≤ scalesK β c C * epsilon β I.Λ (m - 1) ^ (2 * delta β) ∧ a β I.Λ m * epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m ≤ scalesK β c C * epsilon β I.Λ m ^ (-gamma β) ∧ epsilon β I.Λ m ≤ scalesK β c C * epsilon β I.Λ (m - 1) ^ q β

Core estimates at one scale 2 ≤ m ≤ M, from the diffusivity bounds for m < M and the one-sided terminal bounds at m = M.

theorem AVenhance.Infra.Section5.LeftToShow.left_to_show_scales (β C₀ : ℝ) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → 0 < I.kappaSeq κ M m ∧ I.kappaSeq κ M m ≤ I.kappaSeq κ M (m - 1) ∧ I.kappaSeq κ M (m - 1) ≤ K ∧ AVenhance.a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaSeq κ M m ≤ K * I.kappaSeq κ M (m - 1) ∧ epsilon β I.Λ m ^ 2 / (I.kappaSeq κ M m * tau β I.Λ m) ≤ K * epsilon β I.Λ (m - 1) ^ (2 * delta β) ∧ AVenhance.a β I.Λ m * epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m ≤ K * epsilon β I.Λ m ^ (-gamma β) ∧ epsilon β I.Λ m ≤ K * epsilon β I.Λ (m - 1) ^ q β

Scale package (e.kappam, e.expqunt, e.corrm, s.indy#flux-size) for 2 ≤ m ≤ M, with the one-sided handling at m = M.

theorem AVenhance.Infra.Section5.LeftToShow.epsilon_le_inv_Lambda {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 1 ≤ m) : epsilon β Λ m ≤ (↑Λ)⁻¹

ε_{m-1} is small for Λ large (m ≥ 2).

theorem AVenhance.Infra.Section5.LeftToShow.Scales.eps_le_inv_128 {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 1 ≤ m) : epsilon β Λ m ≤ 1 / 128

theorem AVenhance.Infra.Section5.LeftToShow.epsilon_pred_pow_q_div_two_le {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 2 ≤ m) : epsilon β Λ (m - 1) ^ q β / 2 ≤ epsilon β Λ m

Lower supergeometric bound (from epsilon_supergeo, using ε_{m-1} ≤ 1/128).

theorem AVenhance.Infra.Section5.LeftToShow.left_to_show_condition (β C₀ : ℝ) : ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → epsilon β I.Λ m ^ 2 ≤ I.kappaSeq κ M m * tau β I.Λ m / 2

e.condition for κ = κ_m once Λ is large (needed by l.flux.to.energy).

theorem AVenhance.Infra.Section5.LeftToShow.tauPP_div_tauP_eq {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (m : ℕ) : tauPP β Λ m / tauP β Λ m = 4 * ↑⌈epsilon β Λ (m - 1) ^ (-delta β)⌉₊ + 1

τ''_m / τ'_m = 4 ⌈ε_{m-1}^{-δ}⌉ + 1.

theorem AVenhance.Infra.Section5.LeftToShow.Scales.four_ceil_add_one_le {x : ℝ} (hx : 5 / 2 ≤ x) : 4 * ↑⌈x⌉₊ + 1 ≤ 6 * x

Elementary ceiling estimate: 4⌈x⌉ + 1 ≤ 6x once x ≥ 5/2.

theorem AVenhance.Infra.Section5.LeftToShow.four_tauPP_reciprocal_nat {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 1 ≤ m) : ∃ (N : ℕ), 0 < N ∧ ↑N * (4 * tauPP β Λ m) = 1

1 is an integer number of periods 4τ''_m of JHat_m.

theorem AVenhance.Infra.Section5.LeftToShow.four_tauPP_eq_nat_mul_four_tau {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {m : ℕ} (hm : 1 ≤ m) : ∃ (n : ℕ), 4 * tauPP β Λ m = ↑n * (4 * tau β Λ m)

4τ''m is a multiple of 4τ_m (period of 𝐣{m,n}).

theorem AVenhance.Infra.Section5.LeftToShow.ergodic_gap_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < q β - 1 - gamma β / 2

Exponent gap of the ergodic frequency: q - 1 - γ/2 = (q-1)(1 - β/(2(q+1))) > 0.

theorem AVenhance.Infra.Section5.LeftToShow.exp_neg_le_factorial_div_pow {y : ℝ} (hy : 0 < y) (n : ℕ) : Real.exp (-y) ≤ ↑n.factorial / y ^ n

e^{-y} ≤ n!/yⁿ.

theorem AVenhance.Infra.Section5.LeftToShow.exp_neg_rpow_le_rpow {p K P : ℝ} (hp : 0 < p) (hK : 0 < K) (_hP : 0 ≤ P) : ∃ (K' : ℝ), 0 < K' ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → Real.exp (-(ε ^ (-p) / K)) ≤ K' * ε ^ P

Super-polynomial smallness: for p > 0, the factor e^{-ε^{-p}/K} beats any power.

theorem AVenhance.Infra.Section5.LeftToShow.mul_pow_le_pow_mul_self {C x : ℝ} {N : ℕ} (hC : 0 ≤ C) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hN : 1 ≤ N) : (C * x) ^ N ≤ C ^ N * x

Trading (C x)^N for x when 0 ≤ x ≤ 1 and N ≥ 1 (used for the e.JJhat remainder).