OAI/NumberTheory/JointDickman/Arithmetic/PrimeDigitDecomposition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.primeDigits line 10
2. def OAI.JointDickman.joinPrimeDigits line 13
3. theorem OAI.JointDickman.primeDigits_join line 16
4. theorem OAI.JointDickman.join_primeDigits line 30
5. def OAI.JointDickman.primeDigitEquiv line 39
6. theorem OAI.JointDickman.primeSquare_digit_mean line 47

   Source documentation

   The complete residue law, including any dependence on both digits.

   theorem primeSquare_digit_mean {p : ℕ} [NeZero p]
       (F : ZMod p → ZMod p → ℝ) :
       (∑ x : ZMod (p^2), F (primeDigits p x).1 (primeDigits p x).2)/(p : ℝ)^2 =
         (∑ r : ZMod p, ∑ t : ZMod p, F r t)/(p : ℝ)^2 := by
   …

   Mentions: OAI.JointDickman.primeDigits

7. theorem OAI.JointDickman.primeSquare_first_digit_test line 57

   Source documentation

   First-digit events do not alter the conditional distribution of the second digit. This is a finite sum identity, requiring no conditional measure.

   theorem primeSquare_first_digit_test {p : ℕ} [NeZero p]
       (f : ZMod p → ℝ) (g : ZMod p → ZMod p → ℝ) :
       (∑ x : ZMod (p^2), f (primeDigits p x).1 *
         g (primeDigits p x).1 (primeDigits p x).2)/(p : ℝ)^2 =
         ∑ r : ZMod p, (f r/(p : ℝ))*((∑ t : ZMod p, g r t)/(p : ℝ)) := by
   …

   Mentions: OAI.JointDickman.primeDigits