OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternLogKernelCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed-depth cost of the terminal logarithmic cutoffs

  1. theorem OAI.Ostmann.movingPatternLogKernelBudget_spectatorScale_window line 13

    Source documentation

    Retaining all terminal log weights preserves the quadratic budget, uniformly in their centers and in the moving Fourier window.

    theorem movingPatternLogKernelBudget_spectatorScale_window
    (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ) (A H B D Dlog : ℝ)
    (hA : 0 ≤ A) (hH : 0 ≤ H) (hDlog : 0 ≤ Dlog) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ L : ℝ, 1 ≤ L →
      let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount