OAI/NumberTheory/Ostmann/Arithmetic/MovingSlotLines.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSlotLine line 11
2. theorem OAI.Ostmann.movingSlotLine_degree line 16
3. theorem OAI.Ostmann.movingSlotLine_height line 29
4. theorem OAI.Ostmann.movingSlotLine_vars line 52
5. theorem OAI.Ostmann.moving_slot_joint_symbolic_comparison line 72

   Source documentation

   All occurrence tests for all representative internal primes are replaced at once, under the original independent slot priors. The multiplier remains complex-valued. Independence follows from absence of the tested coordinate in the actual slot lists, including every ancestor compensation list.

   theorem moving_slot_joint_symbolic_comparison {A J O : Type*}
       [Fintype A] [Nonempty A] [Fintype J] [Fintype O] {n : ℕ}
       (value : A → ℤ) (hinj : Function.Injective value)
       (prime : A → ℕ) (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
       (path : J → O → List (MovingSlotReversal (Fin (n + 1))))
       (current : J → O → MovingSlotReversal (Fin (n + 1)))
       (base : J → O) (coordinate : J → Fin (n + 1))
       (k d : ℕ) (F T : ℝ) (hF : 1 ≤ F) (hT : 1 ≤ T)
       (hlen : ∀ j o, (path j o).length ≤ k)
       (hd : ∀ j o, (∀ s ∈ path j o, s.lengthLE d ∧ s.frequencyLE F) ∧
         (current j o).lengthLE d ∧ (current j o).frequencyLE F)
       (habsent : ∀ j o,
   …

   Mentions: OAI.Ostmann.MovingSlotReversal