OAI/NumberTheory/Ostmann/Characters/SignedFrequencySum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.natAbs_fiber_card_le_two line 12
2. theorem OAI.Ostmann.sum_signed_magnitudes_le line 21
3. theorem OAI.Ostmann.signed_reducedFrequency_lcm_sum_le line 44

   Source documentation

   The factor four is exactly the two possible signs in each history.

   theorem signed_reducedFrequency_lcm_sum_le (S T : Finset ℤ) (N g h : ℕ)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
       (hT : ∀ t ∈ T, t ≠ 0 ∧ t.natAbs ≤ N) (hg : g ≠ 0) (hh : h ≠ 0) :
       (∑ s ∈ S, ∑ t ∈ T,
         (((reducedFrequency g s.natAbs).lcm (reducedFrequency h t.natAbs) : ℕ) : ℝ)⁻¹) ≤
         4 * (g.divisors.card : ℝ) * h.divisors.card * (1 + Real.log N) ^ 3 := by
   …

   Mentions: OAI.Ostmann.reducedFrequency