SingleHistoryRates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the single-history leaf frequency cost

theorem OAI.Ostmann.single_leaf_frequency_cancellation line 15

Source documentation

Unlike the two-history comparison, this cancels every leading copy of Delta against the squared level-zero weight.

theorem single_leaf_frequency_cancellation (r V : ℕ) (Δ m K : ℝ)
    (hV : (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m)) :
    (2 * (V : ℝ)) ^ r * Real.exp (-(r : ℝ) * Δ + K) ≤
      Real.exp ((r : ℝ) * Real.sqrt m + r * Real.log 2 + K) := by
…

theorem OAI.Ostmann.single_leaf_frequency_budget_sublinear line 28
theorem OAI.Ostmann.single_frequency_budget_subexponential line 37

theorem OAI.Ostmann.single_history_budget_parameters line 62

Source documentation

A single divisor bound works for every history and every permissible frequency range. The numerical estimate is independent of its residue modulus.

theorem single_history_budget_parameters (n : ℕ) (K C ε : ℝ)
    (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ m : ℝ in atTop, ∃ D : ℝ, 0 ≤ D ∧
      (∀ q : ℕ, q ≠ 0 → (q : ℝ) ≤ Real.exp (2 * C * m) → (q.divisors.card : ℝ) ≤ D) ∧
      (∀ N V : ℕ, ∀ Δ : ℝ, (N : ℝ) ≤ Real.exp (C * m) →
        (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
        Real.exp (-(2 ^ n : ℕ) * Δ + K) *
          ((4 * D ^ 3 * (1 + Real.log N)) ^ (2 ^ n - 1) * (2 * (V : ℝ)) ^ (2 ^ n)) ≤
            Real.exp (ε * m)) := by
…

theorem OAI.Ostmann.single_arithmetic_support_rate line 103

Source documentation

The one-history arithmetic sum, including its square-weight factor, is subexponential. This bound is uniform in the choice of residue modulus.

theorem single_arithmetic_support_rate {Q : ℕ} [NeZero Q]
    (n : ℕ) (K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ m : ℝ in atTop, ∀ N V : ℕ, ∀ Δ : ℝ, ∀ S : Finset ℤ,
      (N : ℝ) ≤ Real.exp (C * m) →
      (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
      (∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N) →
      ∀ data : FrequencyTree S n → (ZMod Q)ˣ → List (ZMod Q)ˣ → Option (ArithmeticSplitData Q),
      (∀ t P past d, data t P past = some d →
        d.hasFrequencies (singleTreeNodeFrequencies S n t past.length)) →
      Real.exp (-(2 ^ n : ℕ) * Δ + K) * singleArithmeticSupportSum S V n data ≤ Real.exp (ε * m) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.singleArithmeticSupportSum