OAI/NumberTheory/Ostmann/Arithmetic/MovingResidueFactorization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingResidueFlag line 12
2. def OAI.Ostmann.movingArchimedeanFlag line 15
3. def OAI.Ostmann.movingSpectatorResidue line 18
4. theorem OAI.Ostmann.movingArithmeticIndicator_residue_real line 23
5. theorem OAI.Ostmann.moving_arithmetic_spectator_residue_factor line 42

   Source documentation

   On a fixed top residue pair the original spectator coefficient is a fixed signed-residue value. The only remaining variable gate is real.

   theorem moving_arithmetic_spectator_residue_factor {σ 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) {n : ℕ} (T : MovingSlotData σ n)
       (hf : T.Frequencies (· ≠ 0)) (XL XR a b M : ℕ)
       (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
       (hMq : ∀ i ∈ S, (q i : ℤ) * movingSpectatorDenominator value T ∣ (M : ℤ))
       (hL : (XL : ℤ) ≡ (a : ℤ) [ZMOD M]) (hR : (XR : ℤ) ≡ (b : ℤ) [ZMOD M]) :
       let nodes := T.formulaNodes value hvalue childBound pivotBound hf (.prime false) (.prime true)
   …

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