OAI/Geometry/EinsteinFour/ModelIdentification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Derdzinski, Compositio Math. 49 (1983), Remark 7, p.429 (citing Hitchin), identifies compact connected oriented Einstein four-manifolds of positive scalar curvature with one vanishing Weyl block. Positive sectional curvature supplies the required scalar sign.

  1. def OAI.PositiveEinsteinFour.Geometry.DerdzinskiHitchinInput line 23

    Source documentation

    The compact positive-curvature specialization of the published half-conformally-flat identification.

    def DerdzinskiHitchinInput (g : SmoothMetric M) (o : FrameOrientation g) : Prop :=
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation

  2. theorem OAI.PositiveEinsteinFour.Geometry.classified_of_one_block_vanishes line 32