OAI/Geometry/LatticeCovering/Desmoothing.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Desmoothing.convex_escape line 12
  2. lemma OAI.SingleLatticeCovering.Desmoothing.logConcave_superlevel line 62
  3. lemma OAI.SingleLatticeCovering.Desmoothing.density_le_peak line 78
  4. lemma OAI.SingleLatticeCovering.Desmoothing.density_le_tail line 84
  5. lemma OAI.SingleLatticeCovering.Desmoothing.integrable_density_mul line 93
  6. lemma OAI.SingleLatticeCovering.Desmoothing.integral_density_sub_left line 101
  7. lemma OAI.SingleLatticeCovering.Desmoothing.integrable_density_sub_left line 105
  8. lemma OAI.SingleLatticeCovering.Desmoothing.convolution_upper_of_far_superlevel line 113
  9. theorem OAI.SingleLatticeCovering.Desmoothing.logConcave_desmoothing line 136
  10. def OAI.SingleLatticeCovering.CanonicalDensity.canonical line 157
  11. lemma OAI.SingleLatticeCovering.CanonicalDensity.canonical_nonneg line 160
  12. lemma OAI.SingleLatticeCovering.CanonicalDensity.canonical_measurable line 163
  13. lemma OAI.SingleLatticeCovering.CanonicalDensity.canonical_usc line 167
  14. lemma OAI.SingleLatticeCovering.CanonicalDensity.canonical_map line 184
  15. lemma OAI.SingleLatticeCovering.CanonicalDensity.canonical_mass line 197
  16. lemma OAI.SingleLatticeCovering.LinearCoordinates.map_uniform_coordinates line 224
  17. lemma OAI.SingleLatticeCovering.CanonicalDensity.linear_body_properties line 265
  18. lemma OAI.SingleLatticeCovering.CanonicalDensity.image_volume_ne_zero line 275
  19. lemma OAI.SingleLatticeCovering.CanonicalDensity.projected_uniform_density line 284
  20. lemma OAI.SingleLatticeCovering.CanonicalDensity.projected_convolution line 301
  21. theorem OAI.SingleLatticeCovering.LinearCoordinates.exists_coordinates line 334
  22. def OAI.SingleLatticeCovering.GaussianProjection.localStep line 384
  23. def OAI.SingleLatticeCovering.GaussianProjection.tailError line 385
  24. lemma OAI.SingleLatticeCovering.GaussianProjection.localStep_pos line 388
  25. lemma OAI.SingleLatticeCovering.GaussianProjection.localStep_le_one line 389
  26. theorem OAI.SingleLatticeCovering.GaussianProjection.actual_canonical_lower line 396
  27. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_scaling line 465
  28. lemma OAI.SingleLatticeCovering.GaussianDensity.density_scaling line 474
  29. def OAI.SingleLatticeCovering.CanonicalDensity.verticalScale line 488
  30. lemma OAI.SingleLatticeCovering.CanonicalDensity.verticalScale_fiber line 492
  31. lemma OAI.SingleLatticeCovering.CanonicalDensity.verticalScale_volume line 501
  32. lemma OAI.SingleLatticeCovering.CanonicalDensity.canonical_verticalScale line 519
  33. lemma OAI.SingleLatticeCovering.CanonicalDensity.standardize_lower line 528
  34. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_inv_bound line 558
  35. lemma OAI.SingleLatticeCovering.GaussianDensity.volume_closedBall_bound line 569
  36. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_dimension_mono line 589
  37. lemma OAI.SingleLatticeCovering.GaussianDensity.densityFloor_dimension_mono line 594
  38. lemma OAI.SingleLatticeCovering.GaussianProjection.root_error_identity line 604
  39. lemma OAI.SingleLatticeCovering.GaussianProjection.normalization_second line 616