Definitions.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Geometric definitions for the product counterexample. The projection measure is the canonically normalized Euclidean Hausdorff measure of dimension d - 1, not ambient d-dimensional measure.

def OAI.ProjectionCounterexample.project line 21
Source documentation
Orthogonal projection onto the hyperplane normal to u.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:23 (same declaration text).
```
def project {d : ℕ} (u : E d) : E d →L[ℝ] E d :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.projectionVolume line 25
Source documentation
Actual (d−1)-dimensional Euclidean volume of the orthogonal projection.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:26 (same declaration text).
```
def projectionVolume {d : ℕ} (P : Set (E d)) (u : E d) : ℝ :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.projectionBody line 30
Source documentation
The projection body, defined entirely by its directional projection volumes. The bounds are the normalized Hausdorff measures of orthogonal projections.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:29 (same declaration text).
```
def projectionBody {d : ℕ} (P : Set (E d)) : Set (E d) :=
…
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.bodyVolume line 34
Source documentation
Lebesgue volume in the ambient Euclidean space.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:32 (same declaration text).
```
def bodyVolume {d : ℕ} (P : Set (E d)) : ℝ := (volume P).toReal
```
Mentions: OAI.ProjectionCounterexample.E
def OAI.ProjectionCounterexample.ratio line 37
Source documentation
The normalized projection-body volume.
Also declared: ComparatorChallenges/ProjectionCounterexample.lean:34 (same declaration text).
```
def ratio {d : ℕ} (P : Set (E d)) : ℝ :=
…
```
Mentions: OAI.ProjectionCounterexample.E