CurvatureGreen.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The derivative-slot curvature integration. Divergence freedom removes the differentiated coefficient, and skew-symmetry leaves exactly one half of the covariant commutator.

abbrev OAI.PositiveEinsteinFour.Averages.CurvatureIndex line 15
def OAI.PositiveEinsteinFour.Averages.outerSwap line 17
theorem OAI.PositiveEinsteinFour.Averages.divergence_sum_zero line 23
theorem OAI.PositiveEinsteinFour.Averages.skew_commutator_sum line 42

theorem OAI.PositiveEinsteinFour.Averages.weighted_curvature_green line 76

Source documentation

Integrating a divergence-free curvature coefficient leaves the precise half-commutator term. All first-derivative weight terms are retained.

theorem weighted_curvature_green
    (φ : Fin 4 → ℝ → Ω ≃ᵐ Ω)
    (hφ : ∀ k, Continuous (fun p : ℝ × Ω => φ k p.1 p.2))
    (hμ : ∀ k t, MeasurePreserving (φ k t) μ μ)
    (m : C(Ω, ℝ)) (dm : Fin 4 → C(Ω, ℝ))
    (A dA : CurvatureIndex → C(Ω, ℝ))
    (Z : Fin 4 → C(Ω, E)) (X : Fin 4 → Fin 4 → C(Ω, E))
    (D : Fin 4 → Fin 4 → Fin 4 → C(Ω, E))
    (hdiv : ∀ i j l x, (∑ k, dA ((i, k), (j, l)) x) = 0)
    (hskew : ∀ i k j l x, A ((k, i), (j, l)) x = -A ((i, k), (j, l)) x)
    (hm : ∀ k t x, HasDerivAt (fun s => m (φ k s x)) (dm k (φ k t x)) t)
    (hA : ∀ p t x, HasDerivAt (fun s => A p (φ p.1.2 s x)) (dA p (φ p.1.2 t x)) t)
…

Mentions: OAI.PositiveEinsteinFour.Averages.CurvatureIndex