OAI/Probability/SKGap/Localization/IntegrableMulBounded.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGapCutoff.Clock.integrable_mul_bounded line 126
  2. lemma OAI.SKGapCutoff.Clock.pairing_abs_le line 132
  3. lemma OAI.SKGapCutoff.Clock.pairing_sub_abs_le line 141
  4. lemma OAI.SKGapCutoff.Clock.pairing_of_L1_limit line 148
  5. theorem OAI.SKGapCutoff.Clock.pairing_of_finite_approximation line 157
  6. lemma OAI.SKGapCutoff.Clock.measurable_stepMass line 204
  7. lemma OAI.SKGapCutoff.Clock.stepMass_abs_le line 208
  8. lemma OAI.SKGapCutoff.Clock.stepMass_mul line 216
  9. lemma OAI.SKGapCutoff.Clock.summable_mul_bounded line 222
  10. lemma OAI.SKGapCutoff.Clock.integral_histogram_summable line 228
  11. def OAI.SKGapCutoff.Clock.testHistogram line 242
  12. lemma OAI.SKGapCutoff.Clock.measurable_testHistogram line 245
  13. lemma OAI.SKGapCutoff.Clock.testHistogram_bound line 250
  14. lemma OAI.SKGapCutoff.Clock.integral_histogram_test line 254