OAI/Geometry/LatticeCovering/Isotropy.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.FiniteDimensions.absorb_finitely_many_dimensions line 18
  2. theorem OAI.SingleLatticeCovering.Assembly.all_dimensions_main_reduction line 70
  3. abbrev OAI.SingleLatticeCovering.Isotropization.E line 97
  4. def OAI.SingleLatticeCovering.Isotropization.uniformLaw line 99
  5. lemma OAI.SingleLatticeCovering.Isotropization.volume_pos line 102
  6. lemma OAI.SingleLatticeCovering.Isotropization.uniform_probability line 105
  7. lemma OAI.SingleLatticeCovering.Isotropization.continuous_memLp_uniform line 109
  8. lemma OAI.SingleLatticeCovering.Isotropization.continuous_eq_on_interior line 119
  9. lemma OAI.SingleLatticeCovering.Isotropization.inner_not_constant_on_interior line 130
  10. lemma OAI.SingleLatticeCovering.Isotropization.covariance_positive line 152
  11. lemma OAI.SingleLatticeCovering.Isotropization.positive_form_normalization line 170
  12. def OAI.SingleLatticeCovering.Isotropization.adjointEquiv line 218
  13. lemma OAI.SingleLatticeCovering.Isotropization.adjointEquiv_adjoint line 239
  14. def OAI.SingleLatticeCovering.Isotropization.centeredEquiv line 257
  15. lemma OAI.SingleLatticeCovering.Isotropization.map_centeredEquiv line 260
  16. lemma OAI.SingleLatticeCovering.Isotropization.memLp_translate line 265
  17. lemma OAI.SingleLatticeCovering.Isotropization.memLp_centered line 271
  18. lemma OAI.SingleLatticeCovering.Isotropization.centeredEquiv_mean line 275
  19. lemma OAI.SingleLatticeCovering.Isotropization.centeredEquiv_covariance line 288
  20. theorem OAI.SingleLatticeCovering.Isotropization.uniform_affine_isotropization line 299
  21. def OAI.SingleLatticeCovering.Isotropization.affineMeasurableEquiv line 332
  22. lemma OAI.SingleLatticeCovering.Isotropization.affine_map_volume line 337
  23. lemma OAI.SingleLatticeCovering.Isotropization.affine_volume_factor_pos line 346
  24. lemma OAI.SingleLatticeCovering.Isotropization.map_uniformLaw line 353
  25. theorem OAI.SingleLatticeCovering.Isotropization.isotropic_affine_body line 382
  26. def OAI.SingleLatticeCovering.Isotropization.LogConcave line 396
  27. def OAI.SingleLatticeCovering.Isotropization.uniformPdf line 400
  28. lemma OAI.SingleLatticeCovering.Isotropization.uniformPdf_measurable line 403
  29. lemma OAI.SingleLatticeCovering.Isotropization.uniformPdf_nonneg line 406
  30. lemma OAI.SingleLatticeCovering.Isotropization.uniformPdf_logConcave line 409
  31. lemma OAI.SingleLatticeCovering.Isotropization.uniformLaw_eq_withDensity line 425
  32. def OAI.SingleLatticeCovering.Isotropization.IsIsotropic line 441
  33. lemma OAI.SingleLatticeCovering.Isotropization.covariance_isotropy line 444
  34. lemma OAI.SingleLatticeCovering.Isotropization.affine_body_properties line 468
  35. theorem OAI.SingleLatticeCovering.Isotropization.isotropic_logConcave_affine_body line 483
  36. lemma OAI.SingleLatticeCovering.Sections.map_snd_restrict line 521
  37. lemma OAI.SingleLatticeCovering.Sections.measurable_fiber_measure line 539
  38. lemma OAI.SingleLatticeCovering.Sections.map_snd_uniform line 546
  39. lemma OAI.SingleLatticeCovering.Sections.canonical_density_ae line 553
  40. lemma OAI.SingleLatticeCovering.Sections.continuous_gaussian line 562
  41. lemma OAI.SingleLatticeCovering.Sections.canonical_gaussian_lower_of_ae line 569
  42. lemma OAI.SingleLatticeCovering.Sections.canonical_gaussian_lower_of_density line 588