OAI/NumberTheory/Ostmann/Arithmetic/SimultaneousSquares.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.unitsMap_eq_iff_modEq line 11
2. theorem OAI.Ostmann.lcm_units_ext line 21
3. theorem OAI.Ostmann.simultaneous_square_probability_le line 33
4. theorem OAI.Ostmann.reduced_simultaneous_square_probability_le line 76

   Source documentation

   The support probability under the original larger Haar modulus, before conditioning on any history tests.

   theorem reduced_simultaneous_square_probability_le {a b Q : ℕ}
       [NeZero a] [NeZero b] [NeZero Q]
       (ha : a ∣ Q) (hb : b ∣ Q) (A : (ZMod a)ˣ) (B : (ZMod b)ˣ) :
       (Fintype.card (ZMod Q)ˣ : ℝ)⁻¹ *
           (∑ x : (ZMod Q)ˣ,
             if (ZMod.unitsMap ha x) ^ 2 = A ∧ (ZMod.unitsMap hb x) ^ 2 = B then (1 : ℝ) else 0) ≤
         2 * ((a.lcm b).divisors.card : ℝ) ^ 2 / (a.lcm b) := by
   …