OAI/NumberTheory/JointDickman/Amplification/GraphEndpointDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.graphEndpointResidue line 11
2. theorem OAI.JointDickman.graph_endpoint_congruence line 15
3. theorem OAI.JointDickman.graph_endpoint_three_root_mean line 34

   Source documentation

   Exact finite-period mean; the coefficient congruences cost 1/(ab). The three retained roots do not interact with this congruence.

   theorem graph_endpoint_three_root_mean {a b c : ℕ} [NeZero a] [NeZero b]
       (hab : a.Coprime b) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       [NeZero (∏ p ∈ P, p)] [∀ p : P, NeZero p.val]
       (hcop : (a*b).Coprime (∏ p ∈ P, p)) (j : ℤ)
       (ha : ∀ p ∈ P, ¬p ∣ a) (hb : ∀ p ∈ P, ¬p ∣ b) (hc : ∀ p ∈ P, ¬p ∣ c)
       (hj : ∀ p ∈ P, (j : ZMod p) ≠ 0) (he : (a : ℤ) = b+j*c) :
       (∑ x : ZMod (a*b*∏ p ∈ P, p),
         (if b ∣ x.val ∧ (a : ℤ) ∣ (x.val : ℤ)+j then (1 : ℝ) else 0) *
         ∏ p : P, residueWeight (1/2) (0 : ZMod p.val) (x.val : ZMod p.val) *
           residueWeight (1/2) (-(j : ZMod p.val)) (x.val : ZMod p.val) *
           residueWeight (1/2) ((b : ZMod p.val)*(c : ZMod p.val)⁻¹) (x.val : ZMod p.val)) /
           ((a : ℝ)*b*∏ p ∈ P, (p : ℝ)) =
   …

   Mentions: OAI.JointDickman.residueWeight