DyadicCharacterBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit scale decay for the dyadic supported-history estimate

theorem OAI.Ostmann.dyadic_character_numeric_bound line 12

theorem OAI.Ostmann.dyadic_character_cost line 47

Source documentation

All six concrete loss factors may be charged to one polynomial exponent. The short-prime atom and the long/short gap remain outside that exponent.

theorem dyadic_character_cost (N CP CQ M R B P : ℝ)
    (_hN : 0 ≤ N) (hCP : 0 ≤ CP) (hCQ : 0 ≤ CQ) (hM : 0 ≤ M) (hR : 0 ≤ R)
    (hB : 0 ≤ B) (hP : 0 ≤ P)
    (bN : N ≤ Real.exp P) (bCP : CP ≤ Real.exp P) (bCQ : CQ ≤ Real.exp P)
    (bM : M ≤ Real.exp P) (bR : R ≤ Real.exp P) (bB : B ≤ Real.exp P) :
    2 * N * CP * CQ * B ^ 2 ≤ Real.exp (Real.log 2 + 6 * P) ∧
      2 * N * CP * M * R * B ^ 2 ≤ Real.exp (Real.log 2 + 6 * P) := by
…

theorem OAI.Ostmann.eventual_dyadic_character_decay line 71

Source documentation

The finite dyadic estimate implies the required double-exponential smallness uniformly over every allowed collection of numerical parameters.

theorem eventual_dyadic_character_decay (C z α β γ c : ℝ) (d : ℕ)
    (hC : 0 ≤ C) (hz : 0 ≤ z) (hα : 0 < α) (hαβ : α < β)
    (hγβ : γ < β) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ (m N CP CQ M R B a b q : ℝ) (w : ℂ),
      0 ≤ m → m ≤ z * L → 0 ≤ N → 0 ≤ CP → 0 ≤ CQ → 0 ≤ M → 0 ≤ R →
      Real.exp (c * Real.exp (α * L)) ≤ b → Real.exp (Real.exp (β * L)) ≤ a →
      0 ≤ q → q ≤ Real.exp (Real.exp (γ * L)) →
      2 * N * CP * CQ * B ^ 2 ≤ Real.exp (C * (1 + m) ^ d) →
      2 * N * CP * M * R * B ^ 2 ≤ Real.exp (C * (1 + m) ^ d) →
      ‖w‖ ^ 2 ≤ N * CP *
        (CQ * b⁻¹ * (2 * B ^ 2) + M * (R * (2 * a⁻¹ * B ^ 2)) * q ^ 2) →
      ‖w‖ ≤ Real.exp (-(c / 4) * Real.exp (α * L)) := by
…