OAI/NumberTheory/TwoPointCorrelations/MRTLogPrimeBins.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual logarithmic bins used in the MRT factorization. Their integer index and multiplicative width are controlled with the original floor.

  1. def OAI.TwoPointCorrelations.mrtPrimeLogBin line 13

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:13 (same declaration text).

  2. def OAI.TwoPointCorrelations.mrtPrimeLogLower line 16

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:16 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrt_prime_log_lower_one line 19

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:19 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrt_prime_log_bin_bounds line 23

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:23 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrt_prime_log_bin_range line 45

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:45 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.mrt_prime_log_width line 54

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:54 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.mrt_prime_log_lower_le_upper line 68

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:68 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.mrt_log_bin_weighted_sum line 81

    Source documentation

    The complete first-band scalar sum; the number of coarse bins does not appear in the geometric part of the bound.

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:81 (same declaration text).

    theorem mrt_log_bin_weighted_sum {β H P Q N T : ℝ}
    (hβ : 0 < β) (hH : 0 < H) (hβH : β ≤ H)
    (hP : 1 ≤ P) (hQ : 1 ≤ Q) (hN : 0 < N) (hT : 0 ≤ T) :
    (∑ k ∈ Icc ⌊H * Real.log P⌋₊ ⌊H * Real.log Q⌋₊,
      Real.exp (-β * (k : ℝ) / H) * (T * mrtPrimeLogLower H k / N + 1)) ≤
      ((2 * Real.exp 1 * H / β) * P ^ (-β)) * (T * Q / N + 1) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtPrimeLogLower

  9. lemma OAI.TwoPointCorrelations.mrt_log_bin_card line 102

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPrimeBins.lean:102 (same declaration text).