OAI/NumberTheory/DirichletL/PrimeRows/Measurable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbeHighRowFamily.measurable_const_cpow line 14
  2. lemma OAI.SevenEighths.ProbeHighRowFamily.rowClosedMarked_measurable line 18
  3. lemma OAI.SevenEighths.ProbeHighRowFamily.continuedMarkedLocal_measurable line 27
  4. lemma OAI.SevenEighths.ProbeHighRowFamily.ramifiedCorrection_measurable line 43
  5. lemma OAI.SevenEighths.ProbeHighRowFamily.idealUnramifiedCorrection_measurable line 54
  6. lemma OAI.SevenEighths.ProbeHighRowFamily.continuedCorrection_measurable line 64
  7. lemma OAI.SevenEighths.ProbeHighRowFamily.continuedCompensatedLocal_measurable line 80
  8. lemma OAI.SevenEighths.ProbeHighRowFamily.LFunction_measurable line 91
  9. lemma OAI.SevenEighths.ProbeHighRowFamily.regularizedL_measurable line 100
  10. lemma OAI.SevenEighths.ProbeHighRowFamily.reciprocal_measurable line 107
  11. lemma OAI.SevenEighths.ProbeHighRowFamily.continuedL_measurable line 113
  12. lemma OAI.SevenEighths.ProbeHighRowFamily.physicalCompensatedRow_measurable line 119
  13. lemma OAI.SevenEighths.ProbeHighRowFamily.calibratedTupleValue_measurable line 138
  14. lemma OAI.SevenEighths.ProbeHighRowFamily.calibratedTupleValue_onLines_aestronglyMeasurable line 154