ArithmeticPatternPriorRate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A depth-independent cost for all original equality patterns

theorem OAI.Ostmann.movingPattern_prior_cost_rate line 15

Source documentation

The original internal-prior cost has an absolute coefficient of 2^n m once the depth is chosen. The fixed pattern count is absorbed only as L tends to infinity; no constant exponential in the depth is charged per slot.

theorem movingPattern_prior_cost_rate (k : ℕ) (hk : 0 < k)
    (C ε : ℝ) (hC : 1 ≤ C) (hε : 0 < ε) (hdepth : 8 * C ≤ (k : ℝ) ^ 3) :
    ∀ᶠ L : ℝ in atTop, ∀ n : ℕ, n ≤ k →
      (2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
          (max 2 (Real.exp (C * L))) ^ (4 * n * 2 ^ n) ≤
        Real.exp ((2 ^ n : ℕ) * spectatorBulkCount k L + ε * spectatorBulkCount k L) := by
…

Mentions: OAI.Ostmann.spectatorBulkCount

theorem OAI.Ostmann.arithmetic_prime_pattern_budget_rate line 62

Source documentation

The retained numerical norm, including all original equality-pattern weights, has the absolute bulk constant log 12 + 1.

theorem arithmetic_prime_pattern_budget_rate (ψ : SchwartzMap ℝ ℂ) (n k : ℕ)
    (hk : 0 < k) (hn : n ≤ k) (B Cfreq Cprior ε : ℝ)
    (hCfreq : 0 ≤ Cfreq) (hCprior : 1 ≤ Cprior) (hε : 0 < ε)
    (hdepth : 8 * Cprior ≤ (k : ℝ) ^ 3) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…

Mentions: OAI.Ostmann.spectatorBulkCount