OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeSupportedStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_step_on_support line 13

   Source documentation

   The next term is the actual doubled-prior amplitude. The transfer inequality is derived rather than imposed as a recurrence hypothesis.

   theorem movingTemplatePrimeAmplitude_step_on_support {σ : Type} [Fintype σ]
       (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime)
       (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (Pg I : Finset ℕ) (hPg : ∀ p ∈ Pg, p.Prime) (hPI : Pg ⊆ I)
       (hI : ∀ p ∈ I, 0 < p) (hφ : ∀ x, 0 ≤ φ x)
       (hpos : 0 < smoothGiantMass Pg φ (G (n + 1)))
       (hμ : ∀ a, 0 ≤ μ n a) (hμmass : ∑ a, μ n a = 1)
       (ν : MovingRegularSlot n r m → σ → ℝ)
       (sets : ∀ q : ℕ, Finset (ZMod q))
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.MovingRegularSlot