NilpotentLattice.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RuledApproximation.nilpotent_frame line 14
Source documentation
A square-zero planar operator has an orthonormal shear frame, with no bound on the shear coefficient.
```
lemma nilpotent_frame (A : Plane →L[ℝ] Plane) (hA : A.comp A = 0) :
    ∃ R : Plane ≃ₗᵢ[ℝ] Plane, ∃ d : ℝ, ∀ z : Plane,
      R.symm (A (R z)) = vec2 (d * z 1) 0 := by
…
```
Mentions: OAI.RuledApproximation.Plane, OAI.RuledApproximation.vec2
def OAI.RuledApproximation.shearLinear line 79
def OAI.RuledApproximation.shearCLM line 84
theorem OAI.RuledApproximation.nilpotent_lattice_model line 88
Source documentation
A sliding-row lattice for every real shear; the retained radius is finite but no smallness of the derivative is imposed.
```
theorem nilpotent_lattice_model (d : ℝ) :
    LatticeModel (d • shearCLM) 1 ((1+|d|)/2) := by
…
```
Mentions: OAI.RuledApproximation.LatticeModel, OAI.RuledApproximation.shearCLM
def OAI.RuledApproximation.orthogonalFrame line 137
lemma OAI.RuledApproximation.orthogonal_closedBall_square line 140
def OAI.RuledApproximation.squareProjected line 175