OAI/Probability/SKGap/Localization/ScalarParametersJoined.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.momentBall line 14
  2. def OAI.SKGap.momentCut line 17
  3. lemma OAI.SKGap.momentCut_nonneg line 23
  4. lemma OAI.SKGap.momentCut_tendsto line 26
  5. lemma OAI.SKGap.momentBall_iff line 33
  6. lemma OAI.SKGap.isClosed_momentBall line 53
  7. lemma OAI.SKGap.momentBall_integrable line 62
  8. lemma OAI.SKGap.momentBall_integral_le line 68
  9. lemma OAI.SKGap.mem_momentBall line 74
  10. lemma OAI.SKGap.momentBall_tail line 81
  11. lemma OAI.SKGap.isTight_momentBall line 97
  12. lemma OAI.SKGap.isCompact_momentBall line 119
  13. lemma OAI.SKGap.integrable_of_linear_bound line 123
  14. def OAI.SKGap.momentClip line 132
  15. lemma OAI.SKGap.momentClip_error line 138
  16. lemma OAI.SKGap.moment_integral_approx line 151
  17. lemma OAI.SKGap.continuousOn_integral_of_linear_bound line 183
  18. lemma OAI.SKGap.gaussian_affine_hasLaw line 204
  19. def OAI.SKGap.gaussianAverage line 215
  20. lemma OAI.SKGap.gaussianAverage_eq_integral line 217
  21. lemma OAI.SKGap.integrable_gaussian_comp_of_bound line 222
  22. lemma OAI.SKGap.continuous_gaussianAverage line 227
  23. theorem OAI.SKGap.continuous_tanh line 239
  24. abbrev OAI.SKGap.ScalarPoint line 245
  25. def OAI.SKGap.scalarM line 247
  26. def OAI.SKGap.scalarQMoment line 249
  27. def OAI.SKGap.scalarD line 251
  28. def OAI.SKGap.scalarS line 253
  29. def OAI.SKGap.scalarA line 255
  30. def OAI.SKGap.scalarPsi line 258
  31. def OAI.SKGap.scalarMomentDomain line 262
  32. lemma OAI.SKGap.continuous_scalarM line 264
  33. lemma OAI.SKGap.continuous_scalarQMoment line 269
  34. lemma OAI.SKGap.continuous_scalarD line 274
  35. lemma OAI.SKGap.continuous_scalarS line 277
  36. lemma OAI.SKGap.scalarQMoment_bounds line 281
  37. lemma OAI.SKGap.scalarM_bounds line 288
  38. lemma OAI.SKGap.continuousOn_scalarA line 293
  39. lemma OAI.SKGap.scalarA_eq line 304
  40. lemma OAI.SKGap.continuousOn_scalarPsi line 317
  41. def OAI.SKGap.scalarLogMoment line 327
  42. lemma OAI.SKGap.continuous_scalarLogMoment line 330
  43. lemma OAI.SKGap.scalarLogMoment_eq line 346