Coordinates.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Coordinates and realization of Hermitian scaling sections.

def OAI.Kaplansky.bundleMapCoordinates line 24
Source documentation
Coordinates of genuine fiber maps in the constructed orthonormal frames.
```
def bundleMapCoordinates (T : ∀ y, Fin n → E y →ₗ[ℂ] F y) (a y : Y) :
    Fin n → Matrix (Fin r) (Fin d) ℂ :=
…
```
theorem OAI.Kaplansky.bundleMapCoordinates_eq line 30
theorem OAI.Kaplansky.continuousOn_bundleMapCoordinates line 40
theorem OAI.Kaplansky.bundleMapCoordinates_expanding line 58
theorem OAI.Kaplansky.bundleUnitaryTransition_star line 69
theorem OAI.Kaplansky.bundleMapCoordinates_compatible line 79
theorem OAI.Kaplansky.mem_hermitianChartSet line 101
def OAI.Kaplansky.realizeHomSection line 108
Source documentation
Interpret a section of the constructed core as linear maps between its original bundles, using the core's selected chart in each fiber.
```
def realizeHomSection
    (hE : ContinuousHermitianMetric (d := d) (E := E))
…
```
Mentions: OAI.Kaplansky.ContinuousHermitianMetric
theorem OAI.Kaplansky.realizeHomSection_at line 119
theorem OAI.Kaplansky.realizeHomSection_coordinates line 128
theorem OAI.Kaplansky.continuousOn_realizeHomSection_coordinates line 139
theorem OAI.Kaplansky.exists_hermitian_scaled_section line 172
Source documentation
Normalization of intrinsic expanding maps descends in the constructed Hom-tuple bundle. The ordinary input bundles may be nontrivial.
```
theorem exists_hermitian_scaled_section
    (hE : ContinuousHermitianMetric (d := d) (E := E))
…
```
Mentions: OAI.Kaplansky.ContinuousHermitianMetric