MovingPatternKernelCost.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed-depth cost of the actual sharp pattern kernel

theorem OAI.Ostmann.movingFourierVariationBudget_nonneg line 12

theorem OAI.Ostmann.movingPatternKernelBudget_exp line 23

Source documentation

Both the polynomial root count and the smooth variation use the bounds of the constructed pattern tree. The constant is independent of bulk size.

theorem movingPatternKernelBudget_exp (ψ : 𝓢(ℝ, ℂ)) (n r₀ : ℕ)
    (A lo hi B D : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) :
    ∃ C : ℝ, 0 < C ∧ ∀ m : ℕ,
      bulkKernelPairComparisonBudget ψ (Real.exp (A * m)) lo hi n
        (2 ^ n * (r₀ + m + 4 * n + 4)) (2 ^ n * (r₀ + m + 4 * n)) 0 B D ≤
      Real.exp (C * ((m : ℝ) + 1)) := by
…

Mentions: OAI.Ostmann.bulkKernelPairComparisonBudget

theorem OAI.Ostmann.movingPatternKernelBudget_spectatorScale line 77
Source documentation
The manuscript chooses a bulk length linear in L at fixed depth. Consequently the complete sharp comparison budget fits the quadratic cost used by the weighted prime-error estimate.
```
theorem movingPatternKernelBudget_spectatorScale (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A lo hi B D : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ L : ℝ, 1 ≤ L →
      let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount
theorem OAI.Ostmann.movingPatternKernelBudget_exp_window line 101
theorem OAI.Ostmann.movingPatternKernelBudget_spectatorScale_window line 153