SpecializedCover.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RuledApproximation.IsParallelogram.isCompact line 12
lemma OAI.RuledApproximation.Cylinder.enlarge_open line 26
lemma OAI.RuledApproximation.HasFiniteCover.open_enlarge line 39
Source documentation
Compact parallelogram covers admit bounded open perpendicular bases with any additional positive error. No portion of the closed ruled family is discarded.
```
lemma HasFiniteCover.open_enlarge {S : Set Space} {A eps : ℝ}
    (hc : HasFiniteCover Cylinder.parallelogram S A) (heps : 0 < eps) :
    HasFiniteCover Cylinder.openBounded S (A+eps) := by
…
```
Mentions: OAI.RuledApproximation.Space, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.Cylinder.parallelogram, OAI.RuledApproximation.Cylinder.openBounded
theorem OAI.RuledApproximation.productCell line 63
Source documentation
The product-cell endpoint follows from the stronger arbitrary-compact producer and exact open-base enlargement.
```
theorem productCell : ProductCellStatement := by
…
```
Mentions: OAI.RuledApproximation.ProductCellStatement
lemma OAI.RuledApproximation.plane_charpoly line 70
lemma OAI.RuledApproximation.plane_hyperbolic_eigenvalues line 77
lemma OAI.RuledApproximation.eigenvalue_le_norm line 86
lemma OAI.RuledApproximation.eigenvalue_smul line 94
theorem OAI.RuledApproximation.orthogonalGrid line 107
Source documentation
The orthogonal-grid endpoint needs no new cover construction: its norm bound implies precisely the two-eigenvalue condition of the general theorem.
```
theorem orthogonalGrid : OrthogonalGridStatement := by
…
```
Mentions: OAI.RuledApproximation.OrthogonalGridStatement
lemma OAI.RuledApproximation.OpenRectangleC2.smoothNear line 121
theorem OAI.RuledApproximation.logarithmic line 132
Source documentation
The logarithmic-cell endpoint follows with its exact velocity scaling and orthonormal-coordinate weight, while its boundary hypothesis remains local.
```
theorem logarithmic : LogarithmicStatement := by
…
```
Mentions: OAI.RuledApproximation.LogarithmicStatement