OAI/Geometry/ComplexBundle/Orthonormal.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Continuous orthonormal frames and orthogonal complements.

  1. structure OAI.Kaplansky.ContinuousIndependentStageFrame line 19
  2. structure OAI.Kaplansky.ContinuousOrthonormalStageFrame line 24
  3. theorem OAI.Kaplansky.ContinuousIndependentStageFrame.continuous_gram line 32
  4. def OAI.Kaplansky.ContinuousIndependentStageFrame.normalize line 41
  5. theorem OAI.Kaplansky.ContinuousIndependentStageFrame.normalize_span line 55
  6. abbrev OAI.Kaplansky.ContinuousOrthonormalStageFrame.ImageTotal line 69
  7. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_synthesis line 72
  8. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_analysis line 84
  9. def OAI.Kaplansky.ContinuousOrthonormalStageFrame.imageTotalHomeomorph line 97

    Source documentation

    A homeomorphism with the subspace topology inherited from the actual ambient bundle, not a separately declared topology on an abstract image.

    def imageTotalHomeomorph : ProjectiveProduct K × EuclideanSpace ℂ (Fin d) ≃ₜ f.ImageTotal where
…
  10. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.imageTotalHomeomorph_base line 110
  11. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.imageTotalHomeomorph_fiber_linear line 114
  12. def OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection line 119
  13. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection_idempotent line 122
  14. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection_mem line 127
  15. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection_eq_self line 130
  16. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_projection line 138
  17. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.image_finrank line 143
  18. theorem OAI.Kaplansky.frameSynthesis_inner line 157
  19. def OAI.Kaplansky.frameSynthesisIsometry line 166
  20. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection_error_inner line 175
  21. def OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementProjection line 197
  22. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementProjection_mem line 200
  23. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.projection_eq_zero_of_orthogonal line 214
  24. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complementProjection_range line 224
  25. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.continuous_complementProjection line 234
  26. theorem OAI.Kaplansky.ContinuousOrthonormalStageFrame.complement_finrank line 249