JacobiKernelAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Averaged powers of the actual noncommuting finite curvature kernel.

theorem OAI.PositiveEinsteinFour.Jacobi.curvatureKernel_power_block_continuous line 15
theorem OAI.PositiveEinsteinFour.Jacobi.integral_trace_kernel_sandwich_le line 27

theorem OAI.PositiveEinsteinFour.Jacobi.integral_trace_curvatureKernel_power_le line 67

Source documentation

At the exceptional energy three, all finite moments of order at least two are bounded by five sixths of the scalar curvature-three moments.

theorem integral_trace_curvatureKernel_power_le {N : ℕ}
    (G : Matrix (Fin N) (Fin N) ℝ) (hG : ∀ i j, 0 ≤ G i j)
    (R : Fin N → Ω → NormalMatrix) (hR : ∀ i, Continuous (R i))
    (hpos : ∀ i x, (R i x).PosSemidef ∧ (R i x).trace = 3)
    (hE : ∀ i, (∫ x, ‖R i x‖ ^ 2 ∂μ) = 15 / 2) (k : ℕ) :
    (∫ x, (curvatureKernel G (fun i => R i x) ^ (k + 2)).trace ∂μ) ≤
      (5 / 6 : ℝ) * 3 ^ (k + 2) * (G ^ (k + 2)).trace := by
…

Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.curvatureKernel