OAI/NumberTheory/Ostmann/Arithmetic/MovingArithmeticPrimeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPrimeRootCuts line 11
2. theorem OAI.Ostmann.movingPrimeRootCuts_card line 18
3. theorem OAI.Ostmann.PublishedProgressionInput.moving_arithmetic_prime_comparison line 30

   Source documentation

   The arithmetic gate in this statement is the original recursive gate. Its idealization is derived on an explicitly bounded number of root cells.

   theorem PublishedProgressionInput.moving_arithmetic_prime_comparison
       (P : PublishedProgressionInput) {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XR a M Q : ℕ)
       (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
       (hQ : 2 ≤ Q) (hq : 1 ≤ M) (hqQ : M ≤ Q) (ha : a.Coprime M)
       (u v : ℝ) (hu : 1 ≤ u) (huv : u ≤ v) (hshort : v ≤ u + 1)
       {k : ℕ} (F : Fin k → ClippedPolynomialFactor) :
       ∃ (s : ℕ → ℝ) (N : ℕ) (d : ℕ → ℂ),
         Monotone s ∧ s 0 = u ∧ s N = v ∧
         N ≤ (movingTopRootCuts value hvalue childBound pivotBound T hf XR).card +
           (∑ i, (F i).polynomial.derivative.natDegree) + 1 ∧ (∀ j, ‖d j‖ ≤ 1) ∧
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.movingTopRootCuts