Radius bookkeeping for the analytic derivative induction.

noncomputable def AVenhance.Infra.Section4.thetaAnalyticRadiusBase (c : ℝ) : ℝ

Base scale in the temperature analyticity radius bound.

Equations

• AVenhance.Infra.Section4.thetaAnalyticRadiusBase c = max (2 ^ 15 / √c) (2 ^ 9)

noncomputable def AVenhance.Infra.Section4.thetaAnalyticRadius (c e γ R : ℝ) : ℝ

Analytic radius bound combining the spatial scale and the initial radius.

Equations

• AVenhance.Infra.Section4.thetaAnalyticRadius c e γ R = max (AVenhance.Infra.Section4.thetaAnalyticRadiusBase c * e ^ (-1 - γ / 2)) (2 / R)

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_a_epsilon_sq_div_kappa {β κ c : ℝ} {m : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) : a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 / κ ≤ c⁻¹ * epsilon β I.Λ (m - 1) ^ (-gamma β)

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_stream_coeff_over_kappa_factorial {β κ c : ℝ} {m q : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) : thetaPotentialDerivativeCoefficient I q / κ / ↑q.factorial ≤ 2 ^ 5 / c * epsilon β I.Λ (m - 1) ^ (-gamma β) * (2 ^ 8 / epsilon β I.Λ (m - 1)) ^ q

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_radius_ratio {e γ A L : ℝ} {q : ℕ} (he : 0 < e) (he1 : e ≤ 1) (hγ : 0 ≤ γ) (hA : 2 ^ 9 ≤ A) (hL : A * e ^ (-1 - γ / 2) ≤ L) (hq : 2 ≤ q) : e ^ (-γ) * (2 ^ 8 / (e * L)) ^ q ≤ (2 ^ 8 / A) ^ 2 * (1 / 2) ^ (q - 2)

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_potential_two_eq {β : ℝ} {m : ℕ} (I : Ingredients β) (he : 0 < epsilon β I.Λ (m - 1)) : thetaPotentialDerivativeCoefficient I 2 = 2 ^ 22 * a β I.Λ (m - 1)

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_sqrt_potential_two_over_kappa {β κ c : ℝ} {m : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) : √(thetaPotentialDerivativeCoefficient I 2 / κ) ≤ 2 ^ 11 / √c * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_q1_factorial_scale {β κ c R₀ : ℝ} {m n : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) (hn : 1 ≤ n) : have e := epsilon β I.Λ (m - 1); have L := thetaAnalyticRadius c e (gamma β) R₀; 4 * √(↑n * thetaPotentialDerivativeCoefficient I 2 / κ) * ↑(n - 1).factorial * L ^ (n - 1) ≤ 1 / 4 * ↑n.factorial * L ^ n

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_shifted_half_geometric_sum (n : ℕ) (hn : 1 ≤ n) : (∑ q ∈ Finset.range (n + 1), if 2 ≤ q then (1 / 2) ^ (q - 2) else 0) ≤ 2

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_high_term_radius_bound {β κ c R₀ : ℝ} {m n q : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) (hnq : 2 ≤ q) (hqle : q ≤ n) (hA : 2 ^ 9 ≤ thetaAnalyticRadiusBase c) (hL : thetaAnalyticRadiusBase c * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2) ≤ thetaAnalyticRadius c (epsilon β I.Λ (m - 1)) (gamma β) R₀) : have e := epsilon β I.Λ (m - 1); have γ := gamma β; have A := thetaAnalyticRadiusBase c; have L := thetaAnalyticRadius c e γ R₀; 4 * ↑(n.choose q) * (thetaPotentialDerivativeCoefficient I q / κ) * ↑(n - q).factorial * L ^ (n - q) ≤ ↑n.factorial * L ^ n * (2 ^ 7 / c * (2 ^ 8 / A) ^ 2 * (1 / 2) ^ (q - 2))

theorem AVenhance.Infra.Section4.ThetaAnalyticScale.theta_qhigh_factorial_scale {β κ c R₀ : ℝ} {m n : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) (hn : 1 ≤ n) : have e := epsilon β I.Λ (m - 1); have L := thetaAnalyticRadius c e (gamma β) R₀; (4 * ∑ q ∈ Finset.range (n + 1), if 2 ≤ q then ↑(n.choose q) * (thetaPotentialDerivativeCoefficient I q / κ) * ↑(n - q).factorial * L ^ (n - q) else 0) ≤ 1 / 4 * ↑n.factorial * L ^ n

theorem AVenhance.Infra.Section4.theta_analytic_radius_scales_of_A5 {β κ c R₀ : ℝ} {m : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κ) : have e := epsilon β I.Λ (m - 1); have γ := gamma β; have L := thetaAnalyticRadius c e γ R₀; 0 < κ ∧ 0 < L ∧ 2 / R₀ ≤ L ∧ (∀ (n : ℕ), 1 ≤ n → 4 * √(↑n * thetaPotentialDerivativeCoefficient I 2 / κ) * ↑(n - 1).factorial * L ^ (n - 1) ≤ 1 / 4 * ↑n.factorial * L ^ n) ∧ ∀ (n : ℕ), 1 ≤ n → (4 * ∑ q ∈ Finset.range (n + 1), if 2 ≤ q then ↑(n.choose q) * (thetaPotentialDerivativeCoefficient I q / κ) * ↑(n - q).factorial * L ^ (n - q) else 0) ≤ 1 / 4 * ↑n.factorial * L ^ n