OAI/Geometry/ProjectionBodies/SupportMeasures.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PettyProjection.gauge_pos_sphere line 13
  2. def OAI.PettyProjection.gaugeDensity line 22
  3. def OAI.PettyProjection.gaugeProjectionMeasure line 25
  4. lemma OAI.PettyProjection.gaugeDensity_measurable line 29
  5. lemma OAI.PettyProjection.gaugeDensity_toReal line 34
  6. lemma OAI.PettyProjection.gaugeMeasure_integral line 38
  7. lemma OAI.PettyProjection.gaugeMeasure_finite line 50
  8. lemma OAI.PettyProjection.gaugeMeasure_mass line 65
  9. lemma OAI.PettyProjection.gaugeMeasure_probability line 73
  10. lemma OAI.PettyProjection.gaugeMeasure_bounded line 81
  11. lemma OAI.PettyProjection.boundedMeasure_integrable_continuous line 97
  12. lemma OAI.PettyProjection.gaugeMeasure_shadow line 106
  13. lemma OAI.PettyProjection.gaugeMeasure_firstVariation line 112
  14. def OAI.PettyProjection.supportFunctional line 129
  15. def OAI.PettyProjection.normalizedVolume line 132
  16. lemma OAI.PettyProjection.normalizedVolume_formula line 135
  17. lemma OAI.PettyProjection.gaugeMeasure_functional line 140
  18. lemma OAI.PettyProjection.gaugeMeasure_self line 165
  19. lemma OAI.PettyProjection.shadowVolume_pos line 187
  20. lemma OAI.PettyProjection.Spherical.convex_deriv_limit line 209
  21. lemma OAI.PettyProjection.Spherical.convex_fderiv_apply_limit line 240
  22. lemma OAI.PettyProjection.Spherical.convex_gradient_limit line 257
  23. lemma OAI.PettyProjection.Spherical.normSmooth_tendsto line 270
  24. lemma OAI.PettyProjection.Spherical.normSmooth_gradient_tendsto line 278