GraphResidueFactors.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The three distinct residue roots in a graph representation

theorem OAI.JointDickman.sum_three_residueWeights line 12
theorem OAI.JointDickman.graph_three_root_mean line 35

theorem OAI.JointDickman.crt_product_mean line 45

Source documentation

Product residue tests factor exactly, including nonnormalized tests.

theorem crt_product_mean {ι : Type*} [Fintype ι] [DecidableEq ι]
    (m : ι → ℕ) [∀ i, NeZero (m i)]
    (hcop : Pairwise (fun i j => (m i).Coprime (m j)))
    (f : ∀ i, ZMod (m i) → ℝ) :
    (∑ n ∈ range (∏ i, m i), ∏ i, f i (n : ZMod (m i))) /
      (∏ i, (m i : ℝ)) = ∏ i, (∑ x : ZMod (m i), f i x) / (m i : ℝ) := by
…

theorem OAI.JointDickman.graph_roots_distinct line 54

Source documentation

At good primes the three graph roots are 0, -j, and b/c.

theorem graph_roots_distinct {p : ℕ} [Fact p.Prime]
    (a b c j : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
    (hj : j ≠ 0) (he : a = b+j*c) :
    (0 : ZMod p) ≠ -j ∧ (0 : ZMod p) ≠ b/c ∧ -j ≠ b/c := by
…