FrameVolume.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Application of the proved radial determinant estimate to the actual frame-curvature fields. The geometric premises retain the ordinary Jacobi equation and polar integration formula; no radial deficit is assumed.

theorem OAI.PositiveEinsteinFour.Geometry.volume_ratio_upper_of_frame_flow line 26

Source documentation

Once the two time-zero energies have been obtained by spherical integration, the classical parallel-frame/Jacobi/polar construction gives the manuscript's upper-volume deficit.

theorem 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