OAI/NumberTheory/Ostmann/Arithmetic/MovingLineProductComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_slot_line_product_comparison line 13

   Source documentation

   This replaces the actual simultaneous line probabilities, under the original product law, by their symbolic rank and feasibility flags. The support may contain any further arithmetic and smooth restrictions.

   theorem moving_slot_line_product_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)) (external : J → Bool)
       (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