Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Ingredients.EpsilonConsequences

Decay and separation consequences of the length scales.

source
theorem AVenhance.Infra.Ingredients.EpsilonConsequences.qpow_ge_linear {q : ℝ} (hq : 1 < q) (m : ℕ) :
1 + ↑m * (q - 1) ≤ q ^ m
source
theorem AVenhance.Infra.Ingredients.EpsilonConsequences.epsilon_le_lambda_pow_aux {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) :
epsilon β Λ m ≤ ↑Λ ^ (-↑m)
source
noncomputable def AVenhance.Infra.Ingredients.EpsilonConsequences.epsilonBase (β : ℝ) (Λ m : ℕ) :
ℝ

Supergeometric base whose reciprocal determines the spatial scale.

Equations
Instances For
    source
    theorem AVenhance.Infra.Ingredients.EpsilonConsequences.qpow_ge_q {q : ℝ} (hq : 1 < q) {m : ℕ} (hm : 1 ≤ m) :
    q ≤ q ^ m
    source
    theorem AVenhance.Infra.Ingredients.EpsilonConsequences.log_lambda_ge_one {Λ : ℕ} (hΛ : 2 ^ 7 ≤ Λ) :
    1 ≤ Real.log ↑Λ
    source
    theorem AVenhance.Infra.Ingredients.EpsilonConsequences.epsilon_base_growth {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) :
    epsilonBase β Λ (m + 1) ≥ ↑Λ * (epsilonBase β Λ m + 1)
    source
    theorem AVenhance.Infra.Ingredients.EpsilonConsequences.exp_le_one_add_mul_exp {x : ℝ} :
    Real.exp x ≤ 1 + x * Real.exp x
    source
    noncomputable def AVenhance.Infra.Ingredients.supergeoConstant (β : ℝ) :
    ℝ

    The β-dependent upper factor correcting the false uniform 10 in e.supergeo (1077-1084).

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Ingredients.epsilon_supergeo {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) :
      (1 - 10 * epsilon β Λ m) * epsilon β Λ m ^ q β ≤ epsilon β Λ (m + 1) ∧ epsilon β Λ (m + 1) ≤ (1 + supergeoConstant β * epsilon β Λ m) * epsilon β Λ m ^ q β

      e.supergeo (1077-1084): the supergeometric scale comparison with the upper error constant corrected.

      source
      theorem AVenhance.Infra.Ingredients.epsilon_le_lambda_pow {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) :
      epsilon β Λ m ≤ ↑Λ ^ (-↑m)

      e.minsep (1069-1073): ε_m ≤ Λ⁻ᵐ, hence ε_m ≤ 2⁻⁷ᵐ.

      source
      theorem AVenhance.Infra.Ingredients.epsilon_minsep {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) :
      ↑Λ * epsilon β Λ (m + 1) ≤ epsilon β Λ m

      e.minsep (1069-1073): successive length scales are separated by at least the prescribed factor Λ.