OAI/Geometry/EinsteinFour/JacobiTraceAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The sharp averaged ordered-product estimate at Weyl energy three.

  1. instance OAI.PositiveEinsteinFour.Jacobi.matrixContinuousENorm line 13

    Also declared: OAI/Geometry/EinsteinFour/AveragedRadial.lean:19 (same declaration text), OAI/Geometry/EinsteinFour/JacobiAverage.lean:18 (same declaration text), OAI/Geometry/EinsteinFour/MatrixGeodesicAverage.lean:20 (same declaration text).

  2. theorem OAI.PositiveEinsteinFour.Jacobi.integral_trace_curvature_product_le line 17