OAI/Geometry/EinsteinFour/GeodesicGeometry11.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The nonround half-flat branch has an actual nonzero self-dual harmonic two-form, by the proved signature formula and Weyl gap.

  1. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_signature line 27
  2. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_harmonic_dimension line 50
  3. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_exists_positive_harmonic line 69
  4. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_normalized_sphericalJacobi line 96
  5. theorem OAI.PositiveEinsteinFour.Geometry.volumeMeasure_le_normalized_canonicalRadialMass line 110
  6. theorem OAI.PositiveEinsteinFour.Geometry.normalized_totalVolume_le_actualJacobiIntegral line 125
  7. theorem OAI.PositiveEinsteinFour.Geometry.normalized_actualJacobiPolar line 149
  8. theorem OAI.PositiveEinsteinFour.Geometry.normalized_volume_ratio_upper_of_frame_flow line 207

    Source documentation

    The two time-zero energies and the parallel-frame/Jacobi/polar construction give the manuscript's upper-volume deficit.

    theorem normalized_volume_ratio_upper_of_frame_flow
    (g : SmoothMetric M) [CompactSpace (FrameBundle g)]
    {μ : Measure (FrameBundle g)} [IsProbabilityMeasure μ]
    (φ : FrameFlow g μ)
    (hC : Continuous (frameCurvatureField g))
    (hH : Continuous (frameCurvatureDerivative g))
    (hpoint : ∀ t e, HasDerivAt
      (fun r => frameCurvatureField g (φ.map r e))
      (frameCurvatureDerivative g (φ.map t e)) t)
    {s : ℝ}
    (hCmean : (∫ e, ‖frameCurvatureField g e‖ ^ 2 ∂μ) = (3 / 2) * s)
    (hHmean : (∫ e, ‖frameCurvatureDerivative g e‖ ^ 2 ∂μ) ≤ (9 / 4) * s)
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField, OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative

  9. theorem OAI.PositiveEinsteinFour.Geometry.normalized_volume_ratio_upper line 276
  10. theorem OAI.PositiveEinsteinFour.Geometry.normalized_hodge_counts line 329
  11. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_volume_energy_counts line 370
  12. theorem OAI.PositiveEinsteinFour.Geometry.actual_oriented_norm_pinching line 392
  13. theorem OAI.PositiveEinsteinFour.Geometry.actual_plus_energy_le_four line 404
  14. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_harmonic_dimension_le_two line 421
  15. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_positive_harmonic_dimension_cases line 433
  16. theorem OAI.PositiveEinsteinFour.Geometry.actual_plusNorm_eq_one_of_energy_one line 461
  17. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_dimension_one_energy line 473
  18. theorem OAI.PositiveEinsteinFour.Geometry.halfFlat_dimension_one_norm line 483