OAI/NumberTheory/Ostmann/Arithmetic/BulkSmoothFactors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkSmoothFactors line 11
2. theorem OAI.Ostmann.bulkSmoothFactors_value line 20
3. theorem OAI.Ostmann.bulkSmoothFactors_budget line 35
4. theorem OAI.Ostmann.bulkSmoothFactors_nat_value line 53

   Source documentation

   Specialization back to the exact natural-prime samples.

   theorem bulkSmoothFactors_nat_value {σ : Type*} (value : σ → ℕ) (i : σ)
       {n : ℕ} (T : MovingSlotData σ n) (hT : T.CompensationAbsent i)
       (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ)
       (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (φ : ℝ → ℝ) (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) (p : ℕ) :
       smoothPolynomialWeight (bulkSmoothFactors (fun j => (value j : ℝ)) i T L R ψ X lo hi
         hlo hhi φ G B D hB hD hφ hlip) (p : ℝ) =
         movingRealSmoothWeight (Function.update value i p) T ψ X lo hi hlo hhi φ G
           (L.eval (p : ℝ)) (R.eval (p : ℝ)) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.smoothPolynomialWeight, OAI.Ostmann.bulkSmoothFactors, OAI.Ostmann.movingRealSmoothWeight