ContinuousRadialComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the actual first-mode Dirichlet comparison to the radial limit.

def OAI.PositiveEinsteinFour.Jacobi.sampledCurvature line 16

theorem OAI.PositiveEinsteinFour.Jacobi.continuous_radial_comparison line 22

Source documentation

The finite comparison passes to the actual sine-weighted curvature integral. The two determinant convergence premises are supplied by the Jacobi approximation, while positivity is supplied by preconjugacy.

theorem continuous_radial_comparison {t D : ℝ} (ht : 0 < t) (htπ : t < Real.pi)
    (A : ℝ → NormalMatrix) (htrace : ∀ s, (A s).trace = 0)
    {L : ℝ} (hL : 0 ≤ L)
    (hc : Continuous (fun s => Averages.sineWeight s • A s))
    (hLip : ∀ s r, ‖Averages.sineWeight s • A s - Averages.sineWeight r • A r‖ ≤
      L * |s - r|)
    (hpos : ∀ᶠ N in atTop, (curvatureDirichlet t (sampledCurvature A N)).PosDef)
    (hdet : Tendsto (fun N : ℕ => (t / (N + 1)) ^ 3 *
      (curvatureDirichlet t (sampledCurvature A N)).det) atTop (nhds D))
    (href : Tendsto (fun N : ℕ => (t / (N + 1)) ^ 3 * (referenceMatrix t N).det ^ 3)
      atTop (nhds (Real.sin t ^ 3))) :
    D ≤ Real.sin t ^ 3 * ((1 : NormalMatrix) -
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Averages.sineWeight, OAI.PositiveEinsteinFour.Jacobi.curvatureDirichlet, OAI.PositiveEinsteinFour.Jacobi.sampledCurvature, OAI.PositiveEinsteinFour.Jacobi.referenceMatrix