OAI/NumberTheory/EgyptianFractions/EightProductRationalSupply.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.rational_divisor_sum_eight_of_collision line 14

   Source documentation

   A conductor collision bound for an indexed family of positive divisors gives an eight-term rational supply of the modulus. Repeated samples are allowed; no primality assumption is made on the modulus.

   theorem rational_divisor_sum_eight_of_collision
       {q P : ℕ} [NeZero q] {ι : Type*} [Fintype ι] [Nonempty ι]
       (a : ι → ℕ) (ha : ∀ i, 0 < a i) (had : ∀ i, a i ∣ P)
       (hcollision : ∀ d : ℕ, 2 ≤ d → d ∣ q →
         (CompositeSpectral.remainderCollisionCount a d : ℝ) ≤
           (Fintype.card ι : ℝ) ^ 2 / (d : ℝ) ^ ((7 : ℝ) / 8)) :
       HasRationalDivisorSum (P ^ 2) (q : ℚ) 8 := by
   …

   Mentions: OAI.Problem337.CompositeSpectral.remainderCollisionCount, OAI.Problem337.HasRationalDivisorSum

2. theorem OAI.Problem337.rational_divisor_sum_eight_of_divisor_collision line 34

   Source documentation

   The exact divisor-list specialization of the indexed collision criterion. The collision count retains each natural divisor once, even if residues coincide. Nonzero P supplies the index 1, including the boundary P = 1.

   theorem rational_divisor_sum_eight_of_divisor_collision
       {q P : ℕ} [NeZero q] (hP : P ≠ 0)
       (hcollision : ∀ d : ℕ, 2 ≤ d → d ∣ q →
         (CompositeSpectral.remainderCollisionCount
           (fun i : P.divisors => (i : ℕ)) d : ℝ) ≤
           (P.divisors.card : ℝ) ^ 2 / (d : ℝ) ^ ((7 : ℝ) / 8)) :
       HasRationalDivisorSum (P ^ 2) (q : ℚ) 8 := by
   …

   Mentions: OAI.Problem337.CompositeSpectral.remainderCollisionCount, OAI.Problem337.HasRationalDivisorSum