OAI/NumberTheory/Ostmann/Arithmetic/LcmFrequencySum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal-lcm sum in the frequency budget

The gcd coordinates embed each frequency pair into three independent positive harmonic sums. No asymptotic divisor estimate is used here.

  1. def OAI.Ostmann.gcdFrequencyCoordinates line 18
  2. theorem OAI.Ostmann.gcdFrequencyCoordinates_recover line 21
  3. theorem OAI.Ostmann.gcdFrequencyCoordinates_injective line 27
  4. theorem OAI.Ostmann.gcdFrequencyCoordinates_lcm line 35
  5. theorem OAI.Ostmann.gcdFrequencyCoordinates_mem line 49
  6. theorem OAI.Ostmann.reciprocal_lcm_sum_le_harmonic_cube line 66

    Source documentation

    Exact finite bound before estimating the harmonic sum.

    theorem reciprocal_lcm_sum_le_harmonic_cube (N : ℕ) :
    (∑ a ∈ Finset.Icc 1 N, ∑ b ∈ Finset.Icc 1 N, ((a.lcm b : ℕ) : ℝ)⁻¹) ≤
      (∑ n ∈ Finset.Icc 1 N, (n : ℝ)⁻¹) ^ 3 := by
…
  7. theorem OAI.Ostmann.reciprocal_lcm_sum_le_log_cube line 106

    Source documentation

    The quantitative frequency-pair estimate used by the norm comparison.

    theorem reciprocal_lcm_sum_le_log_cube (N : ℕ) :
    (∑ a ∈ Finset.Icc 1 N, ∑ b ∈ Finset.Icc 1 N, ((a.lcm b : ℕ) : ℝ)⁻¹) ≤
      (1 + Real.log N) ^ 3 := by
…