OAI/Geometry/ComplexBundle/Frames.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.frameMul line 18

   Source documentation

   Change a finite frame by a matrix acting on its coefficient columns.

   def frameMul (v : Fin d → E) (A : Matrix (Fin d) (Fin d) ℂ) : Fin d → E :=
   …

2. theorem OAI.Kaplansky.gram_frameMul line 21
3. theorem OAI.Kaplansky.inverse_sqrt_gram_identity line 35

   Source documentation

   The inverse positive square root orthonormalizes a positive Gram matrix.

   theorem inverse_sqrt_gram_identity {G : Matrix (Fin d) (Fin d) ℂ} (hG : G.PosDef) :
       (CFC.sqrt G)⁻¹ᴴ * G * (CFC.sqrt G)⁻¹ = 1 := by
   …

4. def OAI.Kaplansky.metricFrame line 47
5. theorem OAI.Kaplansky.metricFrame_orthonormal line 50
6. theorem OAI.Kaplansky.continuous_metricFrame_coefficients line 57

   Source documentation

   Coefficient continuity is valid on open charts by restricting the base.

   theorem continuous_metricFrame_coefficients {Y : Type*} [TopologicalSpace Y]
       (G : Y → Matrix (Fin d) (Fin d) ℂ) (hG : Continuous G)
       (hp : ∀ y, (G y).PosDef) :
       Continuous (fun y => (CFC.sqrt (G y))⁻¹) :=
   …

7. theorem OAI.Kaplansky.frameMul_mul line 64
8. theorem OAI.Kaplansky.frameMul_one line 75
9. theorem OAI.Kaplansky.span_frameMul_le line 80
10. theorem OAI.Kaplansky.span_metricFrame line 87
11. def OAI.Kaplansky.metricBasis line 101

    Source documentation

    An ordinary linear basis supplies the complete orthonormal basis; no orthonormal-frame existence hypothesis is used.

    def metricBasis (b : Module.Basis (Fin d) ℂ E) : OrthonormalBasis (Fin d) ℂ E :=
    …

12. theorem OAI.Kaplansky.metricBasis_apply line 105
13. def OAI.Kaplansky.frameSynthesis line 118
14. def OAI.Kaplansky.frameAnalysis line 123
15. theorem OAI.Kaplansky.frameAnalysis_synthesis line 128
16. theorem OAI.Kaplansky.frameSynthesis_mem_span line 133
17. theorem OAI.Kaplansky.frameSynthesis_analysis line 138
18. def OAI.Kaplansky.frameSpanEquiv line 151
19. theorem OAI.Kaplansky.frameSpan_finrank line 160
20. def OAI.Kaplansky.ContinuousHermitianMetric line 179

    Source documentation

    Continuity of a Hermitian metric, expressed by its values on local continuous sections of an ordinary complex vector bundle.

    def ContinuousHermitianMetric : Prop :=
    …

21. def OAI.Kaplansky.bundleChartFrame line 186

    Source documentation

    The ordinary frame obtained from a linear trivialization.

    def bundleChartFrame (e : Trivialization (Fin d → ℂ) (π (Fin d → ℂ) E))
        [e.IsLinear ℂ] (y : Y) (i : Fin d) : E y :=
    …

22. def OAI.Kaplansky.bundleChartBasis line 190
23. theorem OAI.Kaplansky.bundleChartBasis_apply line 194
24. theorem OAI.Kaplansky.bundleChartFrame_independent line 199
25. theorem OAI.Kaplansky.continuousOn_bundleChartFrame line 207
26. theorem OAI.Kaplansky.continuousOn_bundleGram line 217
27. def OAI.Kaplansky.bundleOrthonormalFrame line 229

    Source documentation

    The actual orthonormal frame on the chart, extended by zero outside.

    def bundleOrthonormalFrame
        (e : Trivialization (Fin d → ℂ) (π (Fin d → ℂ) E)) [e.IsLinear ℂ] (y : Y) : Fin d → E y :=
    …

28. theorem OAI.Kaplansky.bundleOrthonormalFrame_eq line 233
29. theorem OAI.Kaplansky.bundleOrthonormalFrame_orthonormal line 244
30. def OAI.Kaplansky.bundleOrthonormalBasis line 249
31. theorem OAI.Kaplansky.bundleOrthonormalBasis_apply line 254
32. theorem OAI.Kaplansky.continuousOn_bundleOrthonormalFrame line 263
33. def OAI.Kaplansky.bundleUnitaryTransition line 298

    Source documentation

    Transition from the orthonormalization of chart a to that of chart b.

    def bundleUnitaryTransition
        (a b : Trivialization (Fin d → ℂ) (π (Fin d → ℂ) E)) [a.IsLinear ℂ] [b.IsLinear ℂ]
        (y : Y) : Matrix (Fin d) (Fin d) ℂ :=
    …

34. theorem OAI.Kaplansky.bundleUnitaryTransition_eq line 303
35. theorem OAI.Kaplansky.bundleUnitaryTransition_unitary line 313
36. theorem OAI.Kaplansky.bundleUnitaryTransition_self line 322
37. theorem OAI.Kaplansky.bundleUnitaryTransition_comp line 328
38. theorem OAI.Kaplansky.continuousOn_bundleUnitaryTransition line 340