OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternKernelNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.realValueKernelPair_norm_le line 12

   Source documentation

   The bound used in prime replacement is explicit, rather than an unspecified boundedness constant of the constructed integrand.

   theorem realValueKernelPair_norm_le {σ : Type*}
       (value : σ → ℝ) (i : σ) (childBound pivotBound : ℕ → ℕ)
       {n : ℕ} (T : Bool → MovingSlotData σ n)
       (hcomp : ∀ b, (T b).CompensationAbsent i)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (hV : ∀ b, (T b).Frequencies (fun s => |(s : ℝ)| ≤ V))
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0) (L R : ℝ) :
       ‖realValueKernelPair value childBound pivotBound T ψ X lo hi hlo hhi φ G L R‖ ≤
         (movingFourierVariationBudget ψ V lo hi n *
           (2 * B + D * (Real.exp 2 - 1)) ^ (2 ^ n - 1)) ^ 2 := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.realValueKernelPair, OAI.Ostmann.movingFourierVariationBudget

2. theorem OAI.Ostmann.movingPattern_kernel_norm_le line 30