AngularEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Integrate the exact angular identity and the classical Weyl equation. The integrated Weitzenboeck equations are explicit premises; the derivative energy inequality required by Jacobi comparison is derived from them. The published input is Gursky--LeBrun (1999), equation (12), p.8 of the arXiv version math/9807055: integrate that identity with scalar curvature 12 and determinant 2 * sigma * v^3 to obtain the normalization below.

theorem OAI.PositiveEinsteinFour.Angular.cubic_energy_le line 20
theorem OAI.PositiveEinsteinFour.Angular.integrated_gradient_energy_le line 26

theorem OAI.PositiveEinsteinFour.Angular.integral_normalDerivative_energy_le line 41

Source documentation

Equation (8)'s derivative estimate after base integration. The only geometric differential premises are the two classical integrated equations.

theorem integral_normalDerivative_energy_le
    (h : FollandMoments) (Z W : B → Gradient) (v b σ τ : B → ℝ)
    (hZs : ∀ c a, (Z c a)ᵀ = Z c a)
    (hZt : ∀ c a, (Z c a).trace = 0)
    (hv : ∀ᵐ c ∂μ, 0 ≤ v c ∧ v c ≤ 2 ∧ σ c ≤ 1)
    (hb : ∀ᵐ c ∂μ, 0 ≤ b c ∧ b c ≤ 2 ∧ τ c ≤ 1)
    (hvi : Integrable (fun c => v c ^ 2) μ)
    (hbi : Integrable (fun c => b c ^ 2) μ)
    (hci : Integrable (fun c => σ c * v c ^ 3 - v c ^ 2) μ)
    (hdi : Integrable (fun c => τ c * b c ^ 3 - b c ^ 2) μ)
    (hZi : Integrable (fun c => gradientSquareNorm (Z c)) μ)
    (hWi : Integrable (fun c => gradientSquareNorm (W c)) μ)
…

Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Angular.gradientSquareNorm