JacobiVolume.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The upper volume estimate from the Jacobi ODE, curvature-field identities, energy bounds, and the polar volume formula.

theorem OAI.PositiveEinsteinFour.Jacobi.volume_ratio_upper_of_jacobi line 28

Source documentation

Equation (7) from the actual Jacobi ODE and the two geodesic field identities.

theorem volume_ratio_upper_of_jacobi
    (d : (u : ℝ) → Ω → RegularJacobi (Real.pi * u))
    {F G : ℝ → C(Ω, NormalMatrix)} {V s : ℝ}
    (hs : 0 ≤ s)
    (hderiv : ∀ r, HasDerivAt F (G r) r)
    (hstationary : ∀ r, (∫ x, ‖F r x‖ ^ 2 ∂μ) = (3 / 2) * s)
    (henergy : ∀ r, (∫ x, ‖G r x‖ ^ 2 ∂μ) ≤ (3 / 2) * ((3 / 2) * s))
    (hcurvature : ∀ u x r, (d u x).R r = 1 + F r x)
    (hpos : ∀ u x r, ((d u x).R r).PosSemidef)
    (htrace : ∀ u x r, ((d u x).R r).trace = 3)
    (hLip : ∀ u, 0 < u → u < 1 → ∀ x, ∃ L : ℝ, 0 ≤ L ∧ ∀ a b,
      ‖Averages.sineWeight a • radialCurvature (d u x).R (Real.pi * u) a -
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.RegularJacobi, OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Averages.sineWeight, OAI.PositiveEinsteinFour.Jacobi.radialCurvature