OAI/Probability/ProjectionMoments/Graph.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProjectionMoments.volume_preserving_curry line 11
  2. lemma OAI.ProjectionMoments.volume_preserving_transpose line 27
  3. lemma OAI.ProjectionMoments.gaussian_graph_kernel_bound line 39
  4. lemma OAI.ProjectionMoments.measurable_vectorSmoothing line 69
  5. theorem OAI.ProjectionMoments.vectorSmoothing_graph_moment line 75
  6. lemma OAI.ProjectionMoments.measurable_ballKernel line 107
  7. lemma OAI.ProjectionMoments.ballKernel_integral line 111
  8. lemma OAI.ProjectionMoments.rowMap_apply line 131
  9. lemma OAI.ProjectionMoments.measurable_ballAverage line 136
  10. lemma OAI.ProjectionMoments.ballAverage_eq line 144
  11. lemma OAI.ProjectionMoments.measurable_lowerDensity line 170
  12. lemma OAI.ProjectionMoments.ballAverage_graph_moment line 174
  13. theorem OAI.ProjectionMoments.lowerDensity_graph_moment line 186
  14. theorem OAI.ProjectionMoments.lowerDensity_is_density line 205
  15. lemma OAI.ProjectionMoments.ballAverage_eq_zero_of_far line 226
  16. theorem OAI.ProjectionMoments.lowerDensity_eq_zero_of_far line 249
  17. def OAI.ProjectionMoments.rescale line 268
  18. def OAI.ProjectionMoments.dilate line 269
  19. lemma OAI.ProjectionMoments.measurable_rescale line 272
  20. lemma OAI.ProjectionMoments.measurable_dilate line 275
  21. lemma OAI.ProjectionMoments.dilate_rescale line 279
  22. lemma OAI.ProjectionMoments.rescale_preimage_closedBall line 284
  23. def OAI.ProjectionMoments.normalizedRescale line 293
  24. lemma OAI.ProjectionMoments.normalizedRescale_finite line 297
  25. lemma OAI.ProjectionMoments.normalizedRescale_local line 304
  26. lemma OAI.ProjectionMoments.normalizedRescale_support line 317
  27. lemma OAI.ProjectionMoments.normalizedRescale_recover line 334
  28. lemma OAI.ProjectionMoments.ballAverage_smul line 345
  29. lemma OAI.ProjectionMoments.ballAverage_dilate line 350
  30. lemma OAI.ProjectionMoments.normalizedRescale_mass line 379
  31. lemma OAI.ProjectionMoments.ballAverage_normalizedRescale line 393
  32. theorem OAI.ProjectionMoments.ballAverage_graph_moment_scaled line 407
  33. theorem OAI.ProjectionMoments.lowerDensity_graph_moment_scaled line 433
  34. lemma OAI.ProjectionMoments.gaussian_vector_replica_bound line 459
  35. lemma OAI.ProjectionMoments.vectorSmoothing_pow line 495
  36. theorem OAI.ProjectionMoments.vectorSmoothing_integrated_moment line 511
  37. theorem OAI.ProjectionMoments.ballAverage_integrated_moment line 536
  38. theorem OAI.ProjectionMoments.lowerDensity_integrated_moment line 549