OAI/Probability/SKGap/Localization/StepMass.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGapCutoff.Clock.scheffe_density line 120
  2. theorem OAI.SKGapCutoff.Clock.scheffe_density_filter line 157
  3. def OAI.SKGapCutoff.Clock.stepMass line 195
  4. lemma OAI.SKGapCutoff.Clock.stepMass_of_nonneg line 198
  5. lemma OAI.SKGapCutoff.Clock.stepMass_of_neg line 209
  6. lemma OAI.SKGapCutoff.Clock.stepMass_nonneg line 220
  7. lemma OAI.SKGapCutoff.Clock.integral_step_interval line 226
  8. lemma OAI.SKGapCutoff.Clock.integrable_step_interval line 231
  9. lemma OAI.SKGapCutoff.Clock.integral_step_interval_norm line 236
  10. lemma OAI.SKGapCutoff.Clock.integral_stepMass line 245
  11. lemma OAI.SKGapCutoff.Clock.integrable_stepMass line 252
  12. def OAI.SKGapCutoff.Clock.histogram line 257
  13. lemma OAI.SKGapCutoff.Clock.integrable_histogram line 260
  14. lemma OAI.SKGapCutoff.Clock.integral_histogram line 268
  15. lemma OAI.SKGapCutoff.Clock.histogram_nonneg line 283