OAI/Probability/LatticeSurface/Convexity/BoundedLattice.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedLattice.height line 144
  2. def OAI.BoundedLattice.body line 147
  3. def OAI.BoundedLattice.law line 150
  4. def OAI.BoundedLattice.statistic line 153
  5. def OAI.BoundedData.activeGraph line 164
  6. lemma OAI.BoundedData.activeGraph_anchored line 169
  7. lemma OAI.BoundedLattice.continuous_height line 191
  8. lemma OAI.BoundedLattice.closed_body line 197
  9. lemma OAI.BoundedLattice.body_zero line 202
  10. lemma OAI.BoundedLattice.law_zero line 214
  11. lemma OAI.BoundedLattice.statistic_zero line 217
  12. lemma OAI.BoundedLattice.coordinates_height line 220
  13. lemma OAI.BoundedLattice.body_coordinates line 232
  14. lemma OAI.BoundedLattice.map_law line 250
  15. lemma OAI.BoundedLattice.inverse_map_law line 273
  16. lemma OAI.BoundedLattice.one_sample_bounded_data line 282
  17. lemma OAI.BoundedLattice.continuous_statistic line 333
  18. lemma OAI.BoundedLattice.statistic_difference_bound line 337
  19. lemma OAI.BoundedLattice.bounded_moment_transfer line 352
  20. theorem OAI.BoundedLattice.bounded_pinned_exponential_moments line 382
  21. def OAI.BoundedLattice.finiteDomainBody line 412
  22. def OAI.BoundedLattice.finiteDomainLaw line 415
  23. lemma OAI.BoundedLattice.finiteDomainBody_eq line 426
  24. lemma OAI.BoundedLattice.finiteDomainLaw_eq line 446
  25. theorem OAI.BoundedLattice.macroscopic_exponential_moments line 451
  26. lemma OAI.BoundedLattice.measurable_mixed_statistic line 480
  27. theorem OAI.BoundedLattice.macroscopic_exponential_moments_mixtures line 490