Two-sided diffusivity bounds at levels m-1 and m (Lemma r.LeBron, step (c))

For 2 ≤ m ≤ M and Λ large, c₁ ε_{m-1}^{q(β+γ)} ≤ κ_j ≤ 1 for j ∈ {m-1, m}. Sources: the diffusivity recursion (l_recurse) for j < M, the permitted interval for j = M, and the supergeometric comparison ε_m ≥ ½ ε_{m-1}^q.

noncomputable def AVenhance.Infra.FullTheorem.lebronP (β : ℝ) : ℝ

The exponent P = q (β + γ) of Lemma r.LeBron.

Equations

• AVenhance.Infra.FullTheorem.lebronP β = AVenhance.q β * (β + AVenhance.gamma β)

theorem AVenhance.Infra.FullTheorem.epsilon_succ_ge {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {n : ℕ} (hn : 1 ≤ n) : 1 / 2 * epsilon β Λ n ^ q β ≤ epsilon β Λ (n + 1)

ε_{n+1} ≥ ½ ε_n^q for n ≥ 1.

theorem AVenhance.Infra.FullTheorem.epsilon_rpow_succ_ge {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {n : ℕ} (hn : 1 ≤ n) {s : ℝ} (hs : 0 ≤ s) : (1 / 2) ^ s * epsilon β Λ n ^ (q β * s) ≤ epsilon β Λ (n + 1) ^ s

ε_{n+1}^s ≥ (1/2)^s ε_n^{q s} for n ≥ 1, s ≥ 0.

theorem AVenhance.Infra.FullTheorem.epsilon_rpow_le_inv {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {n : ℕ} (hn : 1 ≤ n) {s : ℝ} (hs : 1 ≤ s) : epsilon β Λ n ^ s ≤ (↑Λ)⁻¹

ε_n^s ≤ 1/Λ for n ≥ 1, s ≥ 1.

theorem AVenhance.Infra.FullTheorem.epsilon_rpow_le_inv_rpow {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {n : ℕ} (hn : 1 ≤ n) {s : ℝ} (hs : 0 ≤ s) : epsilon β Λ n ^ s ≤ (↑Λ)⁻¹ ^ s

ε_n^s ≤ (1/Λ)^s for n ≥ 1, s ≥ 0.

theorem AVenhance.Infra.FullTheorem.two_mul_inv_rpow_le_one {s : ℝ} (hs : 0 < s) {Λ : ℝ} (hΛ0 : 0 < Λ) (hΛ : 2 ^ (1 / s) ≤ Λ) : 2 * Λ⁻¹ ^ s ≤ 1

c · Λ^{-s} ≤ 1 once Λ ≥ c^{1/s}, in the form needed for the top level.

theorem AVenhance.Infra.FullTheorem.kappaSeq_level {β C₀ c Cl : ℝ} (hl : ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (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) ≤ Cl * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β))) (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hx : I.Cxi ≤ C₀) (hh : I.Chat ≤ C₀) (hCl : Cl ≤ ↑I.Λ) (hΛs : 2 ^ (1 / (β - gamma β)) ≤ ↑I.Λ) {κ : ℝ} (hκ : κ ∈ permissibleSet β I.Λ) {M : ℕ} (hM : 1 ≤ M) (hκM : κ ∈ permittedInterval β I.Λ M) {j : ℕ} (hj : 1 ≤ j) (hjM : j ≤ M) : min c (1 / 2) * epsilon β I.Λ j ^ (β + gamma β) ≤ I.kappaSeq κ M j ∧ I.kappaSeq κ M j ≤ 1

One level 1 ≤ j ≤ M: min(c,½) ε_j^{β+γ} ≤ κ_j ≤ 1, for Λ large.

theorem AVenhance.Infra.FullTheorem.kappaSeq_window (β C₀ : ℝ) : ∃ (c₁ : ℝ) (Λ₁ : ℝ), 0 < 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 → ∀ (j : ℕ), j = m - 1 ∨ j = m → c₁ * epsilon β I.Λ (m - 1) ^ lebronP β ≤ I.kappaSeq κ M j ∧ I.kappaSeq κ M j ≤ 1

Diffusivity window for j ∈ {m-1, m}: c₁ ε_{m-1}^{P} ≤ κ_j ≤ 1, P = q(β+γ).