Maps.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Continuous bundle maps, adjoints, and normalized Hermitian scaling.

theorem OAI.Kaplansky.continuousOn_bundle_sum_over line 20
theorem OAI.Kaplansky.continuousOn_bundle_smul_over line 39
theorem OAI.Kaplansky.inner_toMatrix line 69

theorem OAI.Kaplansky.intrinsic_relations_of_matrix line 81

Source documentation

Transfer the normalized matrix relations to actual adjoints on the original finite-dimensional Hermitian fibers.

theorem intrinsic_relations_of_matrix
    (b : OrthonormalBasis (Fin d) ℂ E) (c : OrthonormalBasis (Fin r) ℂ F)
    (X : Fin n → E →ₗ[ℂ] F)
    (hcol : (∑ i, (LinearMap.toMatrix b.toBasis c.toBasis (X i))ᴴ *
      LinearMap.toMatrix b.toBasis c.toBasis (X i)) = 1)
    (hrow : ((2/3 : ℂ) • (1 : Matrix (Fin r) (Fin r) ℂ) -
      ∑ i, LinearMap.toMatrix b.toBasis c.toBasis (X i) *
        (LinearMap.toMatrix b.toBasis c.toBasis (X i))ᴴ).PosSemidef) :
    (∑ i, (LinearMap.adjoint (X i)).comp (X i)) = LinearMap.id ∧
      ∀ v : F, 0 ≤ inner ℂ v (((2/3 : ℂ) • (LinearMap.id : F →ₗ[ℂ] F) -
        ∑ i, (X i).comp (LinearMap.adjoint (X i))) v) := by
…

theorem OAI.Kaplansky.bundleMap_apply_eq line 125
theorem OAI.Kaplansky.continuousOn_bundleMap_apply_section line 145
Source documentation
Continuous coordinate matrices act continuously on local sections of the original bundles.
```
theorem continuousOn_bundleMap_apply_section
    (hE : ContinuousHermitianMetric (d := d) (E := E))
…
```
Mentions: OAI.Kaplansky.ContinuousHermitianMetric
theorem OAI.Kaplansky.bundleChartFrame_sum line 172
theorem OAI.Kaplansky.continuous_bundleMap_of_coordinates line 182
Source documentation
Continuity on the actual total spaces follows from the constructed coordinate matrices. No simultaneous trivialization is assumed.
```
theorem continuous_bundleMap_of_coordinates
    (hE : ContinuousHermitianMetric (d := d) (E := E))
…
```
Mentions: OAI.Kaplansky.ContinuousHermitianMetric
theorem OAI.Kaplansky.continuous_realizeHomSection line 223
theorem OAI.Kaplansky.bundleFiberFiniteDimensional line 235
Source documentation
Finite-dimensionality is derived from the ordinary bundle chart.
```
theorem bundleFiberFiniteDimensional (y : Y) : FiniteDimensional ℂ (E y) :=
…
```
def OAI.Kaplansky.bundleAdjoint line 241
Source documentation
The actual fiberwise adjoint, with finite-dimensionality supplied by the original bundle rather than a new hypothesis.
```
def bundleAdjoint (T : ∀ y, Fin n → E y →ₗ[ℂ] F y) (y : Y) (i : Fin n) : F y →ₗ[ℂ] E y := by
…
```
theorem OAI.Kaplansky.bundleAdjoint_inner line 246
theorem OAI.Kaplansky.bundleAdjoint_coordinates line 253
theorem OAI.Kaplansky.continuous_bundleAdjoint line 264
theorem OAI.Kaplansky.exists_continuous_normalized_bundle_maps line 301