HigherPrimeDigits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The next digit at a coefficient prime remains uniform

theorem OAI.JointDickman.prime_square_affine_digit line 11

Source documentation

Cancellation of one known prime factor leaves the next-digit test.

theorem prime_square_affine_digit {p : ℕ} (hp : p ≠ 0) {z c t : ℤ}
    (hz : (p : ℤ) ∣ z) :
    (p : ℤ)^2 ∣ z+(p : ℤ)*c*t ↔ (p : ℤ) ∣ z/p+c*t := by
…

def OAI.JointDickman.higherDigitRoot line 20
theorem OAI.JointDickman.prime_square_digit_root line 25
Source documentation
The actual second-digit divisibility condition is one residue class; no conditioning on absence of squares is used.
```
theorem prime_square_digit_root {p : ℕ} [Fact p.Prime] {z c : ℤ}
    (hz : (p : ℤ) ∣ z) (hc : ¬ (p : ℤ) ∣ c) (t : ZMod p) :
    ((p : ℤ)^2 ∣ z+(p : ℤ)*c*(t.val : ℤ)) ↔ t = higherDigitRoot p z c := by
…
```
Mentions: OAI.JointDickman.higherDigitRoot

theorem OAI.JointDickman.prime_square_digit_probability line 37

Source documentation

Given any first digit compatible with the coefficient, the probability of the quotient prime test over its unconditioned next digit is exactly 1/p.

theorem prime_square_digit_probability {p : ℕ} [Fact p.Prime] {z c : ℤ}
    (hz : (p : ℤ) ∣ z) (hc : ¬ (p : ℤ) ∣ c) :
    (∑ t : ZMod p, if (p : ℤ)^2 ∣ z+(p : ℤ)*c*(t.val : ℤ)
      then (1 : ℝ) else 0)/(p : ℝ) = 1/(p : ℝ) := by
…

theorem OAI.JointDickman.affine_numerator_digit_probability line 45

Source documentation

Equivalent form for an affine numerator at a fixed site.

theorem affine_numerator_digit_probability {p : ℕ} [Fact p.Prime]
    (c b r i : ℤ) (hz : (p : ℤ) ∣ c*(r+i)-b) (hc : ¬ (p : ℤ) ∣ c) :
    (∑ t : ZMod p, if (p : ℤ)^2 ∣ c*(r+(p : ℤ)*(t.val : ℤ)+i)-b
      then (1 : ℝ) else 0)/(p : ℝ) = 1/(p : ℝ) := by
…

theorem OAI.JointDickman.prime_square_digit_probability_le line 56

Source documentation

An incompatible first digit gives probability zero; the uniform bound therefore holds without a first-digit compatibility hypothesis.

theorem prime_square_digit_probability_le {p : ℕ} [Fact p.Prime] (z c : ℤ)
    (hc : ¬ (p : ℤ) ∣ c) :
    (∑ t : ZMod p, if (p : ℤ)^2 ∣ z+(p : ℤ)*c*(t.val : ℤ)
      then (1 : ℝ) else 0)/(p : ℝ) ≤ 1/(p : ℝ) := by
…