GraphResidueMajorant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing coefficient primes from the three quotient weights

theorem OAI.JointDickman.graph_residue_product line 11
theorem OAI.JointDickman.base_residue_three_subset_le line 37

theorem OAI.JointDickman.graph_quotient_residue_majorant line 64

Source documentation

An exact congruence calculation turns the retained quotient factors into the three distinct roots used in the edge-mass calculation.

theorem graph_quotient_residue_majorant (B : ℕ) (G : Finset ℕ)
    (hG : G ⊆ auxiliaryPrimes B) (a b c m l₁ l₂ n : ℕ) (j : ℤ)
    (ha : ∀ p ∈ G, ¬ p ∣ a) (hb : ∀ p ∈ G, ¬ p ∣ b) (hc : ∀ p ∈ G, ¬ p ∣ c)
    (hn : n = b*l₁) (hj : (n : ℤ)+j = a*l₂) (hm : c*n = a*b*m+b) :
    baseArithmeticResidueWeight B m * baseArithmeticResidueWeight B l₁ *
      baseArithmeticResidueWeight B l₂ ≤
      (auxiliaryRatio B ^ (1/2 : ℝ))^3 * ∏ p ∈ G,
        residueWeight (1/2) (0 : ZMod p) (n : ZMod p) *
        residueWeight (1/2) (-(j : ZMod p)) (n : ZMod p) *
        residueWeight (1/2) ((b : ZMod p)*(c : ZMod p)⁻¹) (n : ZMod p) := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.baseArithmeticResidueWeight, OAI.JointDickman.auxiliaryRatio, OAI.JointDickman.residueWeight