JacobiTraceProducts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Ordered curvature products in the lower radial determinant estimate. No curvature matrices at different times are commuted.

theorem OAI.PositiveEinsteinFour.Jacobi.abs_trace_mul_le_frobenius line 15
theorem OAI.PositiveEinsteinFour.Jacobi.frobenius_le_three_of_posSemidef_trace line 31
theorem OAI.PositiveEinsteinFour.Jacobi.frobenius_mul_list_le line 42
theorem OAI.PositiveEinsteinFour.Jacobi.abs_trace_curvature_product_le line 62
Source documentation
This is the ordered-product bound in manuscript Lemma 4.7. The first and last factors retain their square-integrable norms.
```
theorem abs_trace_curvature_product_le (A B : NormalMatrix) (L : List NormalMatrix)
    (hL : ∀ C ∈ L, C.PosSemidef ∧ C.trace = 3) :
    |(A * L.prod * B).trace| ≤ 3 ^ L.length * ‖A‖ * ‖B‖ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix