CenterAxis.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.CenterAxis.point_zero line 13
Source documentation
The finite certificate and the analytic construction use the same central point.
```
@[simp] theorem point_zero : point 0 = (0 : E3) := by
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.CenterAxis.point_one line 17
Source documentation
The first positive component is the first analytic axis.
```
@[simp] theorem point_one : point 1 = axisVector 0 := by
…
```
theorem OAI.Problem356.CenterAxis.point_two line 22
Source documentation
The first negative component is opposite to the first analytic axis.
```
@[simp] theorem point_two : point 2 = -axisVector 0 := by
…
```
theorem OAI.Problem356.CenterAxis.point_three line 28
Source documentation
The second positive component is the second analytic axis.
```
@[simp] theorem point_three : point 3 = axisVector 1 := by
…
```
theorem OAI.Problem356.CenterAxis.point_four line 34
Source documentation
The second negative component is opposite to the second analytic axis.
```
@[simp] theorem point_four : point 4 = -axisVector 1 := by
…
```
theorem OAI.Problem356.CenterAxis.norm_point_of_ne_zero line 40
Source documentation
Each noncentral certificate point is a unit vector.
```
theorem norm_point_of_ne_zero (i : Fin 5) (hi : i ≠ 0) : ‖point i‖ = 1 := by
…
```

theorem OAI.Problem356.CenterAxis.canonical_center_triples line 44

Source documentation

The two canonical contact triples coincide literally with the analytic center triples.

theorem canonical_center_triples :
    (point 0, (point 1, point 2)) = ((0 : E3), (axisVector 0, -axisVector 0)) ∧
    (point 0, (point 3, point 4)) = ((0 : E3), (axisVector 1, -axisVector 1)) := by
…

Mentions: OAI.Problem356.E3