OAI/Geometry/ComplexBundle/CoordinatesMetric.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-coordinate smooth bundles and their metrics.

  1. def OAI.Kaplansky.finiteCoordinateEquiv line 17
  2. def OAI.Kaplansky.finiteCoordinateCore line 23
  3. abbrev OAI.Kaplansky.FiniteCoordinateBundle line 24
  4. instance OAI.Kaplansky.finiteCoordinateBundle_norm line 26
  5. instance OAI.Kaplansky.finiteCoordinateBundle_normedSpace line 28
  6. instance OAI.Kaplansky.finiteCoordinateBundle_smooth line 31
  7. def OAI.Kaplansky.finiteCoordinateTotalHomeomorph line 38

    Source documentation

    The finite-coordinate presentation is the same actual bundle, through an explicit base-preserving linear homeomorphism of total spaces.

    def finiteCoordinateTotalHomeomorph :
    TotalSpace (EuclideanSpace ℂ S) (SmoothLineSumBundle K label) ≃ₜ
      TotalSpace (Fin d → ℂ) (FiniteCoordinateBundle K label d hd) :=
…

    Mentions: OAI.Kaplansky.FiniteCoordinateBundle

  8. instance OAI.Kaplansky.(instance at line 54) line 54

    Source documentation

    Pull back the Hilbert norm, keeping the already constructed fiber topology.

    instance (priority := 2000) finiteCoordinateHilbertNorm (P : ProjectiveProduct K) :
…
  9. instance OAI.Kaplansky.(instance at line 63) line 63
  10. theorem OAI.Kaplansky.finiteCoordinate_continuousHermitianMetric line 79

    Source documentation

    The actual sum metric is continuous in the finite-coordinate presentation.

    theorem finiteCoordinate_continuousHermitianMetric :
    ContinuousHermitianMetric (d := d) (E := FiniteCoordinateBundle K label d hd) := by
…

    Mentions: OAI.Kaplansky.ContinuousHermitianMetric, OAI.Kaplansky.FiniteCoordinateBundle