JacobiRadialDeficit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The quantitative radial deficit before the first conjugate point.

theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.radial_determinant_deficit line 20

Source documentation

The actual Jacobi determinant loses a definite fraction of the squared sine-weighted averaged curvature.

theorem radial_determinant_deficit (ht : 0 < t) (htπ : t < Real.pi)
    (hpre : ∀ s, 0 < s → s ≤ t → IsUnit (d.J s))
    (hR : Continuous d.R) (hRpos : ∀ s, (d.R s).PosSemidef)
    (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 - lossFactor (t ^ 2 / (Real.pi ^ 2 - t ^ 2)) / 6 *
        ‖∫ s in (0 : ℝ)..1, Averages.sineWeight s • radialCurvature d.R t s‖ ^ 2) := by
…

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

theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.radial_deficit_nonneg line 54
Source documentation
After conjugacy the truncated radial density is zero. The same upper bound stays nonnegative from the curvature range alone.
```
theorem radial_deficit_nonneg (ht : 0 ≤ t) (htπ : t < Real.pi)
    (hR : Continuous d.R) (hRpos : ∀ s, (d.R s).PosSemidef)
    (htrace : ∀ s, (d.R s).trace = 3) :
    0 ≤ Real.sin t ^ 3 *
      (1 - lossFactor (t ^ 2 / (Real.pi ^ 2 - t ^ 2)) / 6 *
        ‖∫ s in (0 : ℝ)..1, Averages.sineWeight s • radialCurvature d.R t s‖ ^ 2) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.lossFactor, OAI.PositiveEinsteinFour.Averages.sineWeight, OAI.PositiveEinsteinFour.Jacobi.radialCurvature