OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternKernelGain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quartet gain absorbs the actual sharp-kernel main term

  1. theorem OAI.Ostmann.bulkKernelPair_smooth_le_budget line 11
  2. theorem OAI.Ostmann.exists_movingPatternKernelGain line 23

    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 (ψ : 𝓢(ℝ, ℂ)) (n r₀ : ℕ)
    (A lo hi B D F gain : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) :
    ∃ C : ℝ, 0 < C ∧ ∀ m : ℕ, 1 ≤ 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