OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalEnergyRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The sharp pattern budget applied to the actual coefficient energy

  1. theorem OAI.Ostmann.movingFrequencyCoefficient_original_pattern_rate line 15

    Source documentation

    This is the actual external-prior coefficient energy. The local premise is precisely the original prime-pattern bound, with its retained split probabilities; it is supplied by the prime arithmetic comparison.

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

    Mentions: OAI.Ostmann.spectatorBulkCount