OAI/NumberTheory/Ostmann/Arithmetic/ReducedFrequencySum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.reducedFrequency line 12
2. theorem OAI.Ostmann.reducedFrequency_mul_gcd line 14
3. theorem OAI.Ostmann.reducedFrequency_mem line 17
4. theorem OAI.Ostmann.reducedFrequency_fiber_card_le line 26

   Source documentation

   A fixed reduced modulus has at most one frequency for each divisor of the gcd of the two child frequencies.

   theorem reducedFrequency_fiber_card_le (N g a : ℕ) (hg : g ≠ 0) :
       ((Finset.Icc 1 N).filter fun s => reducedFrequency g s = a).card ≤ g.divisors.card := by
   …

   Mentions: OAI.Ostmann.reducedFrequency

5. theorem OAI.Ostmann.sum_reducedFrequency_le line 40
6. theorem OAI.Ostmann.reducedFrequency_lcm_sum_le line 64

   Source documentation

   After fixing the child frequencies, summing the two parent reduced moduli costs only the divisor multiplicities and a cubic logarithm.

   theorem reducedFrequency_lcm_sum_le (N g h : ℕ) (hg : g ≠ 0) (hh : h ≠ 0) :
       (∑ s ∈ Finset.Icc 1 N, ∑ t ∈ Finset.Icc 1 N,
         (((reducedFrequency g s).lcm (reducedFrequency h t) : ℕ) : ℝ)⁻¹) ≤
         (g.divisors.card : ℝ) * h.divisors.card * (1 + Real.log N) ^ 3 := by
   …

   Mentions: OAI.Ostmann.reducedFrequency