JacobiRadialODE.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Radial determinant comparison from the Jacobi ODE.

def OAI.PositiveEinsteinFour.Jacobi.radialCurvature line 14
theorem OAI.PositiveEinsteinFour.Jacobi.sampled_radialCurvature line 16

theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.radial_determinant_comparison line 33

Source documentation

The Jacobi radial inequality follows from the ODE, trace normalization, and preconjugacy.

theorem radial_determinant_comparison (ht : 0 < t) (htπ : t < Real.pi)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (d.J s))
    (htrace : ∀ s, (d.R s).trace = 3)
    {L : ℝ} (hL : 0 ≤ L)
    (hc : Continuous (fun s => Averages.sineWeight s • radialCurvature d.R t s))
    (hLip : ∀ s r,
      ‖Averages.sineWeight s • radialCurvature d.R t s -
        Averages.sineWeight r • radialCurvature d.R t r‖ ≤ L * |s - r|) :
    (d.J t).det ≤ Real.sin t ^ 3 * ((1 : NormalMatrix) -
      (t ^ 2 / (Real.pi ^ 2 - t ^ 2)) •
        (∫ s in (0 : ℝ)..1, Averages.sineWeight s • radialCurvature d.R t s)).det := by
…

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

theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.radial_compression_posSemidef line 52

Source documentation

The limiting compression is positive semidefinite, including a singular limit; this is the spectral input for the subsequent determinant deficit.

theorem radial_compression_posSemidef (ht : 0 < t) (htπ : t < Real.pi)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (d.J s))
    {L : ℝ} (hL : 0 ≤ L)
    (hc : Continuous (fun s => Averages.sineWeight s • radialCurvature d.R t s))
    (hLip : ∀ s r,
      ‖Averages.sineWeight s • radialCurvature d.R t s -
        Averages.sineWeight r • radialCurvature d.R t r‖ ≤ L * |s - r|) :
    ((1 : NormalMatrix) - (t ^ 2 / (Real.pi ^ 2 - t ^ 2)) •
      (∫ s in (0 : ℝ)..1, Averages.sineWeight s • radialCurvature d.R t s)).PosSemidef := by
…

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