OAI/Probability/SKGap/Gaussian/GaussMoment.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Clock.gaussMoment line 122
  2. lemma OAI.SKGapCutoff.Clock.integrable_gaussMoment line 125
  3. lemma OAI.SKGapCutoff.Clock.hasDerivAt_gaussMoment line 133
  4. lemma OAI.SKGapCutoff.Clock.integrable_abs_add_one_pow_gauss line 141
  5. def OAI.SKGapCutoff.Clock.momentEnvelope line 156
  6. lemma OAI.SKGapCutoff.Clock.integrable_momentEnvelope line 159
  7. lemma OAI.SKGapCutoff.Clock.gaussMoment_deriv_bound line 169
  8. def OAI.SKGapCutoff.Clock.diffMoment line 204
  9. lemma OAI.SKGapCutoff.Clock.diffMoment_bound line 207
  10. lemma OAI.SKGapCutoff.Clock.integrable_diffMoment line 223
  11. lemma OAI.SKGapCutoff.Clock.gaussMoment_derivative_L1 line 228
  12. def OAI.SKGapCutoff.Clock.momentL1 line 262
  13. lemma OAI.SKGapCutoff.Clock.norm_toL1_real line 266
  14. lemma OAI.SKGapCutoff.Clock.momentL1_derivative line 272
  15. lemma OAI.SKGapCutoff.Clock.momentL1_mem_of_gaussian line 304
  16. def OAI.SKGapCutoff.Clock.gaussianTaylor line 328
  17. lemma OAI.SKGapCutoff.Clock.gaussianTaylor_eq line 331
  18. lemma OAI.SKGapCutoff.Clock.gaussianTaylor_bound line 341
  19. lemma OAI.SKGapCutoff.Clock.integrable_gaussianTaylor line 360
  20. lemma OAI.SKGapCutoff.Clock.gaussianTaylor_tendsto line 364
  21. lemma OAI.SKGapCutoff.Clock.gaussianTaylor_L1 line 371
  22. lemma OAI.SKGapCutoff.Clock.toL1_finsetSum line 393
  23. lemma OAI.SKGapCutoff.Clock.toL1_tendsto_of_integral_abs_sub line 409
  24. lemma OAI.SKGapCutoff.Clock.gaussian_increment_mem line 419
  25. lemma OAI.SKGapCutoff.Clock.gaussian_wider_precision_mem line 446
  26. lemma OAI.SKGapCutoff.Clock.gaussian_mem_closed_span line 473
  27. theorem OAI.SKGapCutoff.Clock.finite_gaussian_approximation line 480