OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeSupportedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_transfer_on_support line 13

   Source documentation

   Specialization to the actual surviving giant, regular tuple and frequency. The compensation draw and the giant harmonic normalization are unchanged.

   theorem movingTemplatePrimeAmplitude_transfer_on_support {σ : Type} [Fintype σ]
       (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime)
       (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (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))
       (hsets : ∀ a, (sets (value a)).Nonempty)
   …

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