OrientationQuotient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transport the metric quotient construction through an arbitrary identification of the orientation cover with the round sphere.

theorem OAI.PositiveEinsteinFour.classified_of_round_double_cover line 21

Source documentation

The round-cover branch of the unoriented argument. All hypotheses refer to the covering projection and its deck involution.

theorem classified_of_round_double_cover
    (g : SmoothMetric M) (a : ℝ) (ha : 0 < a)
    (e : N ≃ RoundSphere4) (τ : N → N)
    (hτ : Function.Involutive τ) (hfree : ∀ x, τ x ≠ x)
    (hτdistance : ∀ x y, roundDistance (e (τ x)) (e (τ y)) =
      roundDistance (e x) (e y))
    (p : N → M) (hp : Function.Surjective p)
    (hfibers : ∀ x y, p x = p y ↔ x = y ∨ x = τ y)
    (hdistance : ∀ x y, scaledEDistance g a (p x) (p y) =
      ENNReal.ofReal (min (roundDistance (e x) (e y))
        (roundDistance (e x) (e (τ y))))) : Classified g := by
…

Mentions: OAI.PositiveEinsteinFour.Classified