OAI/NumberTheory/JointDickman/Arithmetic/PrimeDigitCRT.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.primeDigitFamilyEquiv line 11
2. theorem OAI.JointDickman.prime_square_crt_digits line 24

   Source documentation

   Uniform CRT residues retain independent uniform higher digits after all first digits are exposed. The test may depend on both entire families.

   theorem prime_square_crt_digits (P : Finset ℕ) [∀ p : P, NeZero p.val]
       (hP : ∀ p ∈ P, p.Prime)
       (F : (∀ p : P, ZMod p.val) → (∀ p : P, ZMod p.val) → ℝ) :
       (∑ n ∈ range (∏ p ∈ P, p^2),
         F (fun p => (primeDigits p.val (n : ZMod (p.val^2))).1)
           (fun p => (primeDigits p.val (n : ZMod (p.val^2))).2)) /
         (∏ p ∈ P, (p : ℝ)^2) =
       (∑ r, ∑ t, F r t) / (∏ p ∈ P, (p : ℝ)^2) := by
   …

   Mentions: OAI.JointDickman.primeDigits