OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeOccurrences.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.MovingPrimeOccurrences line 11
2. def OAI.Ostmann.movingPrimeOccurrence line 16
3. def OAI.Ostmann.movingPrimeOccurrenceLine line 21
4. theorem OAI.Ostmann.movingPrimeOccurrences_card line 27
5. theorem OAI.Ostmann.movingInternalLocalSupport_occurrences line 41
6. theorem OAI.Ostmann.movingPrimeOccurrenceLine_nonzero line 61

   Source documentation

   Every row used by the simultaneous lift estimate is nonzero, by the actual prime tiers and frequencies of its original occurrence.

   theorem movingPrimeOccurrenceLine_nonzero {σ : Type*} {n : ℕ}
       (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (T : Bool → MovingSlotData σ n) (hlevels : ∀ side, (T side).Levels tier)
       (p : ℕ) (hf : ∀ side, (T side).Frequencies (fun s => (s : ZMod p) ≠ 0))
       (j : MovingPrimeOccurrences value T p) :
       let φ := MovingSlotReversal.naturalReduction p value
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPrimeOccurrences, OAI.Ostmann.MovingSlotReversal.naturalReduction

7. theorem OAI.Ostmann.movingPrimeOccurrenceLine_denominator_ne_zero line 88

   Source documentation

   Ancestor denominators are also units at the current internal prime.

   theorem movingPrimeOccurrenceLine_denominator_ne_zero {σ : Type*} {n : ℕ}
       (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (T : Bool → MovingSlotData σ n) (hlevels : ∀ side, (T side).Levels tier)
       (p : ℕ) (hf : ∀ side, (T side).Frequencies (fun s => (s : ZMod p) ≠ 0))
       (j : MovingPrimeOccurrences value T p) :
       MovingSlotReversal.naturalReduction p value
         (movingPrimeOccurrenceLine value T p j).denominator ≠ 0 := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPrimeOccurrences, OAI.Ostmann.MovingSlotReversal.naturalReduction, OAI.Ostmann.movingPrimeOccurrenceLine