OAI/Probability/GaussianReplacement/Density.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.cubeKernel line 15
  2. lemma OAI.CurrentProjection.measurable_cubeKernel line 18
  3. lemma OAI.CurrentProjection.lintegral_cubeKernel line 21
  4. lemma OAI.CurrentProjection.rowKernel_cube line 28
  5. lemma OAI.CurrentProjection.cubeAverage_eq_kernel line 48
  6. instance OAI.CurrentProjection.sphereLift_isFiniteMeasure line 67
  7. theorem OAI.CurrentProjection.mixed_cube_moment line 72
  8. lemma OAI.CurrentProjection.measurable_append line 91
  9. lemma OAI.CurrentProjection.map_append_pi line 99
  10. lemma OAI.CurrentProjection.ae_pi_append line 121
  11. lemma OAI.CurrentProjection.lintegral_pi_append line 129
  12. lemma OAI.CurrentProjection.cubeAverage_scale_lower line 141
  13. lemma OAI.CurrentProjection.cubeAverage_scale_upper line 151
  14. lemma OAI.CurrentProjection.tendsto_cube_of_recip_nat line 161
  15. lemma OAI.CurrentProjection.measurable_cubeAverage line 214
  16. def OAI.CurrentProjection.extendedCubeDensity line 224
  17. lemma OAI.CurrentProjection.measurable_extendedCubeDensity line 228
  18. lemma OAI.CurrentProjection.cubeAverage_lt_top line 232
  19. lemma OAI.CurrentProjection.exactDensity_eq_of_tendsto line 237
  20. lemma OAI.CurrentProjection.measurable_exactDensity line 250
  21. def OAI.CurrentProjection.labelLaw line 275
  22. instance OAI.CurrentProjection.labelLaw_isFiniteMeasure line 278
  23. lemma OAI.CurrentProjection.cubeAverage_eq_ball_ratio line 281
  24. lemma OAI.CurrentProjection.tendsto_cube_scale line 297
  25. lemma OAI.CurrentProjection.ae_cube_tendsto_positive line 306
  26. lemma OAI.CurrentProjection.mixed_liminf_moment_le line 331
  27. instance OAI.CurrentProjection.gaussianRows_isProbabilityMeasure line 351

    Also declared: ComparatorChallenges/GaussianReplacement.lean:69 (same declaration text).

  28. lemma OAI.CurrentProjection.measurable_own_label line 355

    Also declared: ComparatorChallenges/GaussianReplacement.lean:73 (same declaration text).

  29. lemma OAI.CurrentProjection.measurable_fixed_label line 362
  30. lemma OAI.CurrentProjection.measurable_own_cube line 366
  31. lemma OAI.CurrentProjection.measurable_own_extended line 373
  32. lemma OAI.CurrentProjection.measurable_own_exact line 380
  33. lemma OAI.CurrentProjection.measurable_fixed_extended line 387
  34. lemma OAI.CurrentProjection.measurable_fixed_exact line 394
  35. lemma OAI.CurrentProjection.extended_mixed_moment line 401
  36. lemma OAI.CurrentProjection.extended_ae_finite line 423
  37. lemma OAI.CurrentProjection.ae_target_cube_limit line 451
  38. lemma OAI.CurrentProjection.exact_mixed_moment_of_ae line 462
  39. theorem OAI.CurrentProjection.mixedMomentMain line 484

    Distinct definitions of this name: ComparatorChallenges/GaussianReplacement.lean:433 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.mixedMomentMain@path.