Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.AssemblyScales

scale facts for the main-theorem assembly The choice of the threshold Λ₀ making #

∑ C ε_j^δ ≤ 1/2, the centre κ^{(M)} = ε_M^{2β/(q+1)} of the M-th permitted interval, its convergence to 0⁺, and the eventual smallness of η_M/κ^{(M)} for η_M = C ε_{M+1}^β.

source
theorem AVenhance.Infra.Section5.RelativeError.epsilon_tendsto_zero {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) :
Filter.Tendsto (fun (m : ℕ) => epsilon β Λ m) Filter.atTop (nhds 0)

ε_m → 0.

source
theorem AVenhance.Infra.Section5.RelativeError.epsilon_rpow_le {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {δ : ℝ} (hδ : 0 ≤ δ) (k : ℕ) :
epsilon β Λ k ^ δ ≤ (↑Λ ^ (-δ)) ^ k

ε_k^δ ≤ (Λ^{-δ})^k.

source
theorem AVenhance.Infra.Section5.RelativeError.exists_lambda_threshold (β C : ℝ) (hβ : 1 < β) (hβ' : β < 4 / 3) (hC : 1 ≤ C) :
∃ (Λ₀ : ℝ), ∀ (Λ : ℕ), Λ₀ ≤ ↑Λ → 2 ^ 7 ≤ Λ ∧ C ≤ ↑Λ ∧ ∀ (j : ℕ), 1 ≤ j → ∀ (n : ℕ), C * ∑ i ∈ Finset.range n, epsilon β Λ (j + i) ^ delta β ≤ 1 / 2

The threshold on Λ: Λ ≥ 2^7, C ≤ Λ, and C ∑_{i<n} ε_{j+i}^δ ≤ 1/2 for all j ≥ 1.

source
noncomputable def AVenhance.Infra.Section5.RelativeError.kappaCentre (β : ℝ) (Λ M : ℕ) :
ℝ

The centre ε_M^{2β/(q+1)} of the M-th permitted interval.

Equations
Instances For
    source
    theorem AVenhance.Infra.Section5.RelativeError.kappaCentre_pos {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (M : ℕ) :
    0 < kappaCentre β Λ M
    source
    theorem AVenhance.Infra.Section5.RelativeError.kappaCentre_mem_permittedInterval {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (M : ℕ) :
    kappaCentre β Λ M ∈ permittedInterval β Λ M
    source
    theorem AVenhance.Infra.Section5.RelativeError.kappaCentre_mem_permissibleSet {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {M : ℕ} (hM : 1 ≤ M) :
    kappaCentre β Λ M ∈ permissibleSet β Λ
    source
    theorem AVenhance.Infra.Section5.RelativeError.kappaCentre_tendsto {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) :
    Filter.Tendsto (fun (M : ℕ) => kappaCentre β Λ M) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

    κ^{(M)} → 0⁺.

    source
    theorem AVenhance.Infra.Section5.RelativeError.stream_tail_exponent_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) :
    0 < q β * β - 2 * β / (q β + 1)

    The exponent qβ - 2β/(q+1) is positive.

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

    The supergeometric constant is nonnegative.

    source
    theorem AVenhance.Infra.Section5.RelativeError.epsilon_succ_le {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {M : ℕ} (hM : 1 ≤ M) :
    epsilon β Λ (M + 1) ≤ (1 + Ingredients.supergeoConstant β) * epsilon β Λ M ^ q β

    ε_{M+1} ≤ (1+A) ε_M^q for M ≥ 1.

    source
    theorem AVenhance.Infra.Section5.RelativeError.eta_div_kappaCentre_eventually {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {Ctail : ℝ} (hCt : 0 ≤ Ctail) :
    ∀ᶠ (M : ℕ) in Filter.atTop, Ctail * epsilon β Λ (M + 1) ^ β / kappaCentre β Λ M ≤ 1 / 10

    Eventually Ctail ε_{M+1}^β / κ^{(M)} ≤ 1/10.