HessianDivergence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.adjugate_hessian_divergence line 13
Source documentation
Smoothness through order three suffices for the cofactor cancellation.
```
theorem adjugate_hessian_divergence {n : ℕ} (u : Space n → ℝ) (x : Space n)
    (hu : ContDiffAt ℝ 3 u x) (i : Fin n) :
    (∑ j, fderiv ℝ (fun y => (hessian u y).adjugate i j) x
      (coordinateVector n j)) = 0 := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.coordinateVector
theorem OAI.AffineBernstein.cofactorHessian_eq_adjugate line 26
Source documentation
For an invertible Hessian, the manuscript's definition is exactly the adjugate.
```
theorem cofactorHessian_eq_adjugate {n : ℕ} (u : Space n → ℝ) (x : Space n)
    (hdet : (hessian u x).det ≠ 0) : cofactorHessian u x = (hessian u x).adjugate := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.cofactorHessian
theorem OAI.AffineBernstein.cofactorHessian_isSymm line 32
Source documentation
The Hessian cofactor is symmetric under the standing positivity hypothesis.
```
theorem cofactorHessian_isSymm {n : ℕ} (u : Space n → ℝ) (x : Space n)
    (hpos : (hessian u x).PosDef) : (cofactorHessian u x).IsSymm := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.cofactorHessian

theorem OAI.AffineBernstein.cofactorHessian_divergence line 38

Source documentation

Both divergences of the actual coefficient matrix vanish on the original domain.

theorem cofactorHessian_divergence {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    (u : Space n → ℝ) (hu : ContDiffOn ℝ 3 u Ω)
    (hpos : ∀ x ∈ Ω, (hessian u x).PosDef) (x : Space n) (hx : x ∈ Ω) (i : Fin n) :
    (∑ j, fderiv ℝ (fun y => cofactorHessian u y i j) x (coordinateVector n j)) = 0 ∧
    (∑ j, fderiv ℝ (fun y => cofactorHessian u y j i) x (coordinateVector n j)) = 0 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.cofactorHessian, OAI.AffineBernstein.coordinateVector