JacobiKernelPowers.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Positive scalar path weights bound the noncommuting curvature kernel.

def OAI.PositiveEinsteinFour.Jacobi.curvatureKernel line 12
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_curvatureKernel line 16
theorem OAI.PositiveEinsteinFour.Jacobi.blockAt_one line 22
theorem OAI.PositiveEinsteinFour.Jacobi.scalar_pow_entry_nonneg line 28
theorem OAI.PositiveEinsteinFour.Jacobi.curvatureKernel_power_bound line 38
Source documentation
The initial matrix is kept outside the scalar path bound. In particular, the zero-step bound does not lose the norm of the identity matrix.
```
theorem curvatureKernel_power_bound {N : ℕ} (G : Matrix (Fin N) (Fin N) ℝ)
    (hG : ∀ i j, 0 ≤ G i j) (R : Fin N → NormalMatrix)
    (hR : ∀ i, ‖R i‖ ≤ 3) (k : ℕ) (A : NormalMatrix) (i j : Fin N) :
    ‖A * blockAt (curvatureKernel G R ^ k) i j‖ ≤
      (3 ^ k * (G ^ k) i j) * ‖A‖ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.blockAt, OAI.PositiveEinsteinFour.Jacobi.curvatureKernel