OAI/NumberTheory/Ostmann/Construction/ScheduledSampledEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.uniform_scheduled_clipped_square_rate line 16

   Source documentation

   The original prime law is retained. Both the integer equations and the coefficient units come from the full weight; only published analytic estimates and the explicit prime-cell size conditions remain for the final application.

   theorem uniform_scheduled_clipped_square_rate (n : ℕ)
       (ψ : 𝓢(ℝ, ℂ)) (C₀ K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε)
       (hψ : SchwartzMap.seminorm ℝ 0 0 (𝓕 ψ : 𝓢(ℝ, ℂ)) ≤ Real.exp K) :
       ∀ᶠ m : ℝ in atTop,
         ∀ {I : Type*} [Fintype I],
         ∀ (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
           (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
           (i : I) (hi : role i = .word)
           (_hu : ∀ k < n, ∀ a b, role a = .pivot k → role b = .pivot k → a = b),
         ∀ N V : ℕ, ∀ Δ X lo upper : ℝ,
         ∀ P : Finset ℕ, ∀ S : Finset ℤ,
         (N : ℝ) ≤ Real.exp (C * m) →
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange

2. theorem OAI.Ostmann.scheduled_clipped_square_rate line 85