AveragedRadial.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Averaging the proved Jacobi determinant deficit over initial geodesics. The density is explicitly truncated at the first conjugate point.

instance OAI.PositiveEinsteinFour.Jacobi.matrixContinuousENorm line 19
Also declared: OAI/Geometry/EinsteinFour/JacobiAverage.lean:18 (same declaration text), OAI/Geometry/EinsteinFour/JacobiTraceAverage.lean:13 (same declaration text), OAI/Geometry/EinsteinFour/MatrixGeodesicAverage.lean:20 (same declaration text).
def OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.truncatedDensity line 24
Source documentation
The radial Jacobian, set to zero once a conjugate point has occurred.
```
def RegularJacobi.truncatedDensity {t : ℝ} (d : RegularJacobi t) : ℝ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.RegularJacobi
theorem OAI.PositiveEinsteinFour.Jacobi.RegularJacobi.truncatedDensity_le line 28

theorem OAI.PositiveEinsteinFour.Jacobi.averaged_truncatedDensity_le line 57

Source documentation

The actual averaged radial determinant estimate. Its mean-square and energy hypotheses apply to the field, rather than to individual geodesics. All matrix comparison, finite approximation and averaging steps are proved.

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

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