OAI/Geometry/LatticeCovering/Sections.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Sections.affine_section_of_ball_projection line 24
  2. def OAI.SingleLatticeCovering.Sections.gaussian line 131
  3. lemma OAI.SingleLatticeCovering.Sections.gaussian_pos line 134
  4. lemma OAI.SingleLatticeCovering.Sections.gaussian_near line 140
  5. theorem OAI.SingleLatticeCovering.Sections.finite_section_labels line 168
  6. def OAI.SingleLatticeCovering.Sections.sectionShear line 235
  7. lemma OAI.SingleLatticeCovering.Sections.sectionShear_apply line 249
  8. lemma OAI.SingleLatticeCovering.Sections.fiber_sectionShear line 252
  9. lemma OAI.SingleLatticeCovering.Sections.fiber_sectionShear_measure line 265
  10. lemma OAI.SingleLatticeCovering.Sections.sectionShear_measure line 271
  11. lemma OAI.SingleLatticeCovering.Sections.convex_interior_of_measure_pos line 284
  12. theorem OAI.SingleLatticeCovering.Sections.centered_affine_image line 295
  13. lemma OAI.SingleLatticeCovering.Sections.eventually_fiber_subset line 327
  14. lemma OAI.SingleLatticeCovering.Sections.upperSemicontinuous_fiber_measure line 342
  15. lemma OAI.SingleLatticeCovering.Sections.lower_bound_everywhere_of_ae line 352
  16. theorem OAI.SingleLatticeCovering.Sections.canonical_marginal_lower line 370
  17. theorem OAI.SingleLatticeCovering.Sections.gaussian_marginal_to_sections line 396
  18. lemma OAI.SingleLatticeCovering.Sections.gaussian_toLp line 456
  19. lemma OAI.SingleLatticeCovering.Sections.appendEquiv_measurePreserving line 479
  20. def OAI.SingleLatticeCovering.Sections.flatten line 495
  21. lemma OAI.SingleLatticeCovering.Sections.flatten_apply line 499
  22. lemma OAI.SingleLatticeCovering.Sections.flatten_measurePreserving line 502
  23. lemma OAI.SingleLatticeCovering.Sections.flatten_volume line 508
  24. def OAI.SingleLatticeCovering.Sections.coordinateFiber line 530
  25. lemma OAI.SingleLatticeCovering.Sections.flatten_fiber line 533
  26. theorem OAI.SingleLatticeCovering.Sections.coordinate_marginal_to_labels line 547