OAI/NumberTheory/Ostmann/Arithmetic/MovingSpectatorCells.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSpectatorProduct_modEq line 13
2. theorem OAI.Ostmann.movingSpectatorProduct_norm line 28
3. theorem OAI.Ostmann.PublishedProgressionInput.moving_spectator_prime_comparison line 46

   Source documentation

   This is the literal moving spectator recursion under the original arithmetic indicator. Its residue constancy is proved above; it is not an extra input to the prime comparison.

   theorem PublishedProgressionInput.moving_spectator_prime_comparison
       (P : PublishedProgressionInput) {σ I : Type*} (q : I → ℕ)
       [∀ i, Fact (q i).Prime] (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
       (childBound pivotBound : ℕ → ℕ)
       (g : ∀ i, ZMod (q i) → ℂ) (D : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (B : I → ℝ) (hB : ∀ i ∈ S, 0 ≤ B i) (hg : ∀ i ∈ S, ∀ z, ‖g i z‖ ≤ B i)
       {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XR a M Q : ℕ)
       (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
       (hMq : ∀ i ∈ S, (q i : ℤ) * movingSpectatorDenominator value T ∣ (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) :
   …

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