OAI/NumberTheory/TwoPoint/ShortIntervals/MRTResolution.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic bin resolution used in the multiscale partition. Its balance with the first prime threshold is exact.

  1. def OAI.TwoPointCorrelations.mrtBaseResolution line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:13 (same declaration text).

  2. def OAI.TwoPointCorrelations.mrtResolution line 16

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:16 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrtBaseResolution_pos line 19

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:19 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrtResolution_one line 22

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:22 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrtResolution_pos line 25

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:25 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.mrt_base_resolution_le line 30

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:30 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.mrt_resolution_le line 39

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:39 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.mrt_resolution_log_le line 44

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:44 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.mrt_base_resolution_balance line 53

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:53 (same declaration text).

  10. lemma OAI.TwoPointCorrelations.mrt_base_resolution_first_cost line 76

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:76 (same declaration text).

  11. lemma OAI.TwoPointCorrelations.mrt_resolution_inverse_sum line 87

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTResolution.lean:87 (same declaration text).