OAI/NumberTheory/Ostmann/Arithmetic/MovingLineIntegration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSlotLineProbability line 10
2. theorem OAI.Ostmann.movingSlotLineProbability_eq_flags line 21
3. theorem OAI.Ostmann.internalLineFlagWeight_le_scalar line 57
4. theorem OAI.Ostmann.line_product_multiplier_bound line 67

   Source documentation

   The remaining weight may be large. Its bound is imposed only after the one-over-prime line scalars have been included, exactly as in (8.20).

   theorem line_product_multiplier_bound {A J O : Type*} [Fintype J]
       (prime : A → ℕ) (external : J → Bool) (representative : J → A)
       (weight : ℂ) (B : ℝ)
       (h : ‖weight‖ * ∏ j, internalLineScalar (external j) (prime (representative j)) ≤ B)
       (flags : J × (Bool ⊕ O) → Bool) :
       ‖weight * ∏ j, (internalLineFlagWeight (external j) (prime (representative j))
         (fun s => flags (j, s)) : ℂ)‖ ≤ B := by
   …

   Mentions: OAI.Ostmann.internalLineScalar, OAI.Ostmann.internalLineFlagWeight

5. theorem OAI.Ostmann.moving_line_product_on_support line 87

   Source documentation

   On the original full support the actual line counts can be inserted into the same signed expression. No line identity is requested on rejected samples.

   theorem moving_line_product_on_support {A J O : Type*} [Fintype J] {n : ℕ}
       (value : A → ℤ) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
       (path : J → O → List (MovingSlotReversal (Fin n)))
       (current : J → O → MovingSlotReversal (Fin n)) (base : J → O)
       (external : J → Bool) (representative : J → A) (x : Fin n → A) (weight : ℂ)
       (hpath : weight ≠ 0 → ∀ j o s, s ∈ path j o →
         let φ := integerLineReduction value x (prime (representative j))
   …

   Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.integerLineReduction