OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplatePrimeCore.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplatePrimeCore_eq_full line 19

   Source documentation

   The template amplitude used in the transfer and the core bounded by the arithmetic estimate are identical at the actual prime giants. Every cofactor, spectator transform, and leaf weight is evaluated at the original value.

   theorem movingTemplatePrimeCore_eq_full {σ I : Type} [Fintype σ]
       (pSpec : I → ℕ) [∀ i, Fact (pSpec i).Prime]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (f : ℤ → ℂ)
       (g : ∀ i, ZMod (pSpec i) → ℂ) (Dq : ∀ i, (ZMod (pSpec i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n r m : ℕ) (s : ℤ) (y : MovingRegularSlot n r m → σ)
       (q : Bool → ℕ) [∀ b, Fact (q b).Prime]
       (hprime : ∀ i, (value (y i)).Prime)
       (greg ggiant : ∀ p : ℕ, ZMod p → ℂ) (favorable : ℕ → Bool) :
       let _ : ∀ i, Fact ((value ∘ y) i).Prime := fun i => ⟨hprime i⟩
   …

   Mentions: OAI.Ostmann.MovingRegularSlot