OAI/NumberTheory/JointDickman/Arithmetic/PrimeBandExtractionCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Summability of all prime-square and width errors in the MRT bands

  1. lemma OAI.JointDickman.sum_range_succ_eq_Icc line 9
  2. lemma OAI.JointDickman.sum_range_succ_inv_sq_le line 23
  3. lemma OAI.JointDickman.primeBand_square_mass_le line 30
  4. lemma OAI.JointDickman.mrt_band_lower_ge_square line 53
  5. lemma OAI.JointDickman.canonical_square_mass_le line 77
  6. lemma OAI.JointDickman.canonical_square_mass_le_one line 95
  7. theorem OAI.JointDickman.canonical_extraction_sum_le line 109