OAI/NumberTheory/Ostmann/Arithmetic/SignedSplitSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frequencySignUnit line 11
2. theorem OAI.Ostmann.intCast_frequencySign line 13
3. theorem OAI.Ostmann.signed_coefficient_equation_iff line 24
4. theorem OAI.Ostmann.common_reduced_modulus line 31
5. theorem OAI.Ostmann.signed_joint_split_probability_le line 39

   Source documentation

   Both signs are absorbed into fixed units, and impossible gcd patterns contribute zero. Thus no soluble-pattern hypothesis is needed.

   theorem signed_joint_split_probability_le {s t Q : ℕ} [NeZero s] [NeZero t] [NeZero Q]
       (hs : s ∣ Q) (ht : t ∣ Q) (v w v' w' : ℤ)
       (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 * (((reducedFrequency (v.natAbs.gcd w.natAbs) s).lcm
             (reducedFrequency (v'.natAbs.gcd w'.natAbs) t)).divisors.card : ℝ) ^ 2 /
           (reducedFrequency (v.natAbs.gcd w.natAbs) s).lcm
   …

   Mentions: OAI.Ostmann.reducedFrequency