OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternWindowGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_movingPatternKernelGain_window line 12

   Source documentation

   The tolerance is selected after the fixed Fourier profile and frequency cost, and before the bulk length. All sharp cutoffs are included in W.

   theorem exists_movingPatternKernelGain_window (ψ : 𝓢(ℝ, ℂ)) (n r₀ : ℕ)
       (A H B D F gain : ℝ) (hA : 0 ≤ A) (hH : 0 ≤ H) :
       ∃ C : ℝ, 0 < C ∧ ∀ m : ℕ, 1 ≤ m → ∀ lo hi : ℝ, lo ≤ hi →
         hi - lo ≤ Real.exp (H * m) → ∀ amp δ : ℝ,
         0 ≤ amp → amp ≤ Real.exp (F * m) → 0 ≤ δ →
         δ ≤ signedBulkGainTarget n (C + F) gain →
         let W := (movingFourierVariationBudget ψ (Real.exp (A * m)) lo hi n *
   …

   Mentions: OAI.Ostmann.signedBulkGainTarget, OAI.Ostmann.movingFourierVariationBudget