MatrixGeodesicAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Specialization of mean-square geodesic averaging to actual normal curvature matrices, using their Frobenius norm.

instance OAI.PositiveEinsteinFour.Jacobi.matrixContinuousENorm line 20
Also declared: OAI/Geometry/EinsteinFour/AveragedRadial.lean:19 (same declaration text), OAI/Geometry/EinsteinFour/JacobiAverage.lean:18 (same declaration text), OAI/Geometry/EinsteinFour/JacobiTraceAverage.lean:13 (same declaration text).
def OAI.PositiveEinsteinFour.Jacobi.matrixVector line 25
Source documentation
Entry coordinates preserve the Frobenius norm exactly.
```
def matrixVector : NormalMatrix →ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 3 × Fin 3) where
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix

theorem OAI.PositiveEinsteinFour.Jacobi.matrix_geodesic_mean_square_lower line 47

Source documentation

The matrix form of the averaging theorem used by the radial comparison. The derivative is a derivative of the continuous curvature field, so its energy is measured over all initial geodesics.

theorem matrix_geodesic_mean_square_lower {F G : ℝ → C(Ω, NormalMatrix)} {q t : ℝ}
    (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) :
    q * (1 - (t / Real.pi) ^ 2 / 2) ≤
      ∫ x, ‖∫ u, F (t * u) x ∂Averages.sineMeasure‖ ^ 2 ∂μ := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Averages.sineMeasure