OAI/NumberTheory/Ostmann/Arithmetic/MovingOccurrenceUnits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotReversal.Frequencies line 11
2. def OAI.Ostmann.MovingSlotData.Frequencies line 14
3. theorem OAI.Ostmann.MovingSlotData.Frequencies.root line 18
4. theorem OAI.Ostmann.MovingSlotData.occurrence_frequencies line 24
5. theorem OAI.Ostmann.MovingSlotData.occurrence_units line 54

   Source documentation

   The current compensation primes can repeat within their equality pattern. Only their disjointness from the earlier coefficient types is used here.

   theorem MovingSlotData.occurrence_units {σ : Type*} {q : ℕ} [Fact q.Prime]
       (tier : σ → ℕ) (value : σ → ℕ) {n : ℕ} (T : MovingSlotData σ n)
       (hlevels : T.Levels tier) (hfreq : T.Frequencies (fun s => (s : ZMod q) ≠ 0))
       (o : MovingSlotOccurrence σ) (ho : o ∈ T.occurrences)
       (hcop : ∀ i, o.level ≤ tier i → (value i).Coprime q) :
       (∀ s ∈ o.path,
         MovingSlotReversal.naturalReduction q value s.polynomial.v ≠ 0 ∧
         MovingSlotReversal.naturalReduction q value s.polynomial.w ≠ 0 ∧
         MovingSlotReversal.naturalReduction q value s.polynomial.u ≠ 0) ∧
       MovingSlotReversal.naturalReduction q value o.current.polynomial.v ≠ 0 ∧
         MovingSlotReversal.naturalReduction q value o.current.polynomial.w ≠ 0 := by
   …

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

6. theorem OAI.Ostmann.MovingSlotData.occurrence_units_of_prime_types line 81

   Source documentation

   Disjoint prime types discharge all denominator and nonzero-row conditions at every occurrence of the selected representative.

   theorem MovingSlotData.occurrence_units_of_prime_types {σ : Type*}
       (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       {n : ℕ} (T : MovingSlotData σ n) (hlevels : T.Levels tier)
       (o : MovingSlotOccurrence σ) (ho : o ∈ T.occurrences) (rep : σ)
       (hrep : tier rep < o.level)
       (hfreq : T.Frequencies (fun s => (s : ZMod (value rep)) ≠ 0)) :
       (∀ s ∈ o.path,
         MovingSlotReversal.naturalReduction (value rep) value s.polynomial.v ≠ 0 ∧
         MovingSlotReversal.naturalReduction (value rep) value s.polynomial.w ≠ 0 ∧
         MovingSlotReversal.naturalReduction (value rep) value s.polynomial.u ≠ 0) ∧
       MovingSlotReversal.naturalReduction (value rep) value o.current.polynomial.v ≠ 0 ∧
   …

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

7. theorem OAI.Ostmann.buildMovingSlotData_frequencyUnits line 100