OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternRegularUnits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingRegularOther line 12

   Source documentation

   The denominator left after removing one regular prime and both giants.

   noncomputable def movingRegularOther {σ : Type*} (value : σ → ℕ)
       (outside : List ℕ) (slots : List σ) (j : Fin slots.length) : ℤ :=
   …

2. theorem OAI.Ostmann.movingPattern_regular_other_unit line 16
3. theorem OAI.Ostmann.movingPattern_regular_frequency_unit line 51

   Source documentation

   Every retained frequency is a unit at a regular prime above the common cutoff.

   theorem movingPattern_regular_frequency_unit {σ : Type*}
       (value : σ → ℕ) (hprime : ∀ i, (value i).Prime) (slots : List σ)
       (V : ℕ) (hlarge : ∀ i, V < value i) (s : ℤ) (hs : s ≠ 0) (hV : s.natAbs ≤ V)
       (j : Fin slots.length) : (s : ZMod (value (slots.get j))) ≠ 0 := by
   …