OAI/Geometry/ProjectionBody/Counterexample.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The geometric projection formulas identify the two actual projection bodies. Their proved Euclidean volumes are substituted into the normalized ratio before the final exact arithmetic is performed.

  1. theorem OAI.ProjectionCounterexample.simplex_twenty_brightness line 20
  2. theorem OAI.ProjectionCounterexample.product_brightness line 27
  3. theorem OAI.ProjectionCounterexample.simplex_twenty_projectionBody line 39
  4. theorem OAI.ProjectionCounterexample.product_projectionBody line 45
  5. theorem OAI.ProjectionCounterexample.simplex_twenty_projection_support line 52
  6. theorem OAI.ProjectionCounterexample.product_projection_support line 60
  7. theorem OAI.ProjectionCounterexample.simplex_twenty_ratio line 68
  8. theorem OAI.ProjectionCounterexample.product_ratio_value line 75
  9. theorem OAI.ProjectionCounterexample.product_to_simplex_ratio line 82
  10. theorem OAI.ProjectionCounterexample.product_exceeds_simplex line 87
  11. theorem OAI.ProjectionCounterexample.universal_simplex_upper_bound_false line 96

    Distinct definitions of this name: ComparatorChallenges/ProjectionCounterexample.lean:37 (same statement text; different proof or body). Qualify references as OAI.ProjectionCounterexample.universal_simplex_upper_bound_false@path.