OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateLiveHarmonic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplate_harmonic_diagonal_live line 15

   Source documentation

   The original harmonic product law pays the giant atom and a single factorial product-fibre cost. The frequency range contributes no cardinality factor, because the diagonal key includes the frequency itself.

   theorem movingTemplate_harmonic_diagonal_live
       (P Pg : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPg : ∀ p ∈ Pg, p.Prime)
       (outside : List ℕ) (μ : ℕ → P → ℝ) (childBound pivotBound V : ℕ → ℕ)
       (F : MovingSlotState P → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (hφ0 : ∀ x, 0 ≤ φ x) (hφ1 : ∀ x, φ x ≤ 1) (G : ℕ → ℝ)
       (cg : ℝ)
       (n r m : ℕ) (Q : MovingRegularSlot n r m → Finset ℕ)
       (u : TreeLeafIndex n × Fin 4 → P) (p : ℕ)
       (hvg : ∀ q : Pg, smoothGiantPrior Pg φ cg q ≠ 0 → V n < (q : ℕ)) (hvr : ∀ i (q : P), primeSubsetPrior P (Q i) q ≠ 0 → V n < (q : ℕ))
       (hsep : ∀ q : Pg, smoothGiantPrior Pg φ cg q ≠ 0 →
         ∀ i (a : P), primeSubsetPrior P (Q i) a ≠ 0 → (q : ℕ) ≠ (a : ℕ))
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) :
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.smoothGiantPrior, OAI.Ostmann.primeSubsetPrior