OAI/GroupTheory/PolycyclicRecognition/Analysis/LinearProfilesOnBall.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.linearMap_eq_of_eqOn_closedBall line 15
2. def OAI.PolycyclicRecognition.linearBallProfile line 30

   Source documentation

   An ambient linear label observed through a surjective height map.

   def linearBallProfile (q : V →L[ℝ] W) (A : W →L[ℝ] W) (R : ℝ) :
       C(Metric.closedBall (0 : V) R, W) :=
   …

3. theorem OAI.PolycyclicRecognition.linearBallProfile_injective line 34
4. def OAI.PolycyclicRecognition.closedBallLinearSelf line 45

   Source documentation

   A linear contraction restricts continuously to the same ball.

   def closedBallLinearSelf (ψ : V →L[ℝ] V) (hψ : ∀ x, ‖ψ x‖ ≤ ‖x‖) (R : ℝ) :
       C(Metric.closedBall (0 : V) R, Metric.closedBall (0 : V) R) := by
   …

5. theorem OAI.PolycyclicRecognition.linearBallProfile_rescale line 53