OAI/Geometry/ProjectionVolume/ApproximationBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper092.volume_smul_real line 12
  2. theorem OAI.Paper092.volume_real_mono line 17
  3. theorem OAI.Paper092.approximation_brightness_bound line 21
  4. theorem OAI.Paper092.approximation_projectionBody_sandwich line 40
  5. theorem OAI.Paper092.approximation_volume_sandwich line 49
  6. theorem OAI.Paper092.approximation_projectionBody_volume_sandwich line 57
  7. theorem OAI.Paper092.approximation_brightness_uniform line 68
  8. theorem OAI.Paper092.tendsto_of_multiplicative_sandwich line 88
  9. theorem OAI.Paper092.approximation_volume_tendsto line 100