OAI/NumberTheory/Ostmann/Arithmetic/JointSplitProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.reduced_modulus_pos line 11
2. theorem OAI.Ostmann.joint_split_probability_le line 18

   Source documentation

   The two histories share the random child product but may have different parent products, pivots, and frequencies. No complete-history validity event has been conditioned on in this average.

   theorem joint_split_probability_le {s t Q : ℕ} [NeZero s] [NeZero t] [NeZero Q]
       (hs : s ∣ Q) (ht : t ∣ Q) (v w v' w' : ℕ)
       (hgcd : v.gcd s = w.gcd s) (hgcd' : v'.gcd t = w'.gcd t)
       (A B P : (ZMod s)ˣ) (A' B' P' : (ZMod t)ˣ) :
       (Fintype.card (ZMod Q)ˣ : ℝ)⁻¹ * (∑ x : (ZMod Q)ˣ,
         if (v : ZMod s) * (A * (P / ZMod.unitsMap hs x) : (ZMod s)ˣ) =
             (w : ZMod s) * (B * ZMod.unitsMap hs x : (ZMod s)ˣ) ∧
           (v' : ZMod t) * (A' * (P' / ZMod.unitsMap ht x) : (ZMod t)ˣ) =
             (w' : ZMod t) * (B' * ZMod.unitsMap ht x : (ZMod t)ˣ)
         then (1 : ℝ) else 0) ≤
         2 * (((s / v.gcd s).lcm (t / v'.gcd t)).divisors.card : ℝ) ^ 2 /
           (s / v.gcd s).lcm (t / v'.gcd t) := by
   …