OAI/NumberTheory/Ostmann/Arithmetic/MovingConstructedLiveProductStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_step_constructed_live line 16

   Source documentation

   The cap, monotonicity and frequency-scale hypotheses are discharged by one and the same terminal product and compensation-cell construction.

   theorem movingTemplatePrimeAmplitude_step_constructed_live {σ J : Type} [Fintype σ]
       (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime)
       (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ)
       (q : J → ℕ) [∀ i, Fact (q i).Prime]
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (hF : ∀ {n} (T : MovingSlotData σ n), F T 0 = 0)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset J)
       (ψ : SchwartzMap ℝ ℂ) (X lo hi W : ℝ) (hX : 0 < X)
       (hwindow : X * hi ≤ Real.exp W)
       (φ : ℝ → ℝ) (G c : ℕ → ℝ) (hout : ∀ t, 1 ≤ |t| → φ t = 0)
       (hμlower : ∀ j x, μ j x ≠ 0 → Real.exp (c j - 1) ≤ (value x : ℝ))
   …

   Mentions: OAI.Ostmann.MovingSlotData