OAI/NumberTheory/Ostmann/Arithmetic/SquareRootProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The divisor loss in the square-congruence probability

  1. theorem OAI.Ostmann.two_pow_primeFactors_card_le_divisors_card line 13
  2. theorem OAI.Ostmann.le_divisors_card_mul_totient line 26
  3. theorem OAI.Ostmann.square_root_density_factor_le line 37

    Source documentation

    The loss from unit sampling and the possible power of two is bounded by two divisor factors, leaving the essential reciprocal-modulus decay.

    theorem square_root_density_factor_le (q : ℕ) [NeZero q] :
    (2 : ℝ) ^ (q.primeFactors.card + 1) / q.totient ≤
      2 * (q.divisors.card : ℝ) ^ 2 / q := by
…
  4. theorem OAI.Ostmann.unit_square_probability_le line 58

    Source documentation

    A Haar unit satisfies a prescribed square congruence with probability at most 2*tau(q)^2/q. This applies also to inconsistent congruences.

    theorem unit_square_probability_le (q : ℕ) [NeZero q] (a : (ZMod q)ˣ) :
    (Nat.card {x : (ZMod q)ˣ // x ^ 2 = a} : ℝ) / Fintype.card (ZMod q)ˣ ≤
      2 * (q.divisors.card : ℝ) ^ 2 / q := by
…