OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeNext.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplateDoubledPrior line 10
2. theorem OAI.Ostmann.movingTemplateDoubledPrior_side line 15
3. theorem OAI.Ostmann.amplitude_pair_sum line 22
4. theorem OAI.Ostmann.amplitude_full_sum line 62
5. theorem OAI.Ostmann.movingAmplitudeOffDiagonal_eq_next line 105

   Source documentation

   The off-diagonal is the next amplitude under the independent doubled regular law. Both surviving giants retain their common original prior.

   theorem movingAmplitudeOffDiagonal_eq_next {σ : 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 : Finset ℕ) (hPg : ∀ q ∈ Pg, q.Prime) (ρ : Pg → ℝ)
       (ν : MovingRegularSlot n r m → σ → ℝ)
       (hlarge : ∀ q : Pg, V (n + 1) < (q : ℕ))
       (I : Finset ℕ) (hI : ∀ p ∈ I, 0 < p)
       (hφ : ∀ p : ℕ, 0 < p → φ (Real.log p - G (n + 1)) ≠ 0 → p ∈ I)
       (hchild : V n ≤ childBound (n + 1))
       (hgap : ∀ XR : Pg, ∀ right : MovingRegularSlot n r m → σ, (∏ i, ν i (right i)) ≠ 0 →
   …

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