AngularCofactor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.third_derivative_swap_last line 17
def OAI.AffineBernstein.radiusMatrix line 39
Source comment
Radius matrix in projected constant tangent frames. At a unit `e` and an orthonormal tangent frame this is exactly `∇²_S h + h Id`; its first derivatives are the round covariant derivatives in a normal frame.
```
def radiusMatrix {ι : Type*} (H : E → ℝ) (frame : ι → E) (e : E) : Matrix ι ι ℝ :=
…
```
theorem OAI.AffineBernstein.radiusMatrix_eq line 43

theorem OAI.AffineBernstein.radiusMatrix_cofactor_divergence line 52

Source comment

The angular cofactor divergence identity, derived from the actual Hessian and Euler radial identity, not assumed as a stationarity hypothesis.

theorem radiusMatrix_cofactor_divergence {ι : Type*} [Fintype ι] [DecidableEq ι]
    {H : E → ℝ} {e : E} (hh : ContDiffAt ℝ ∞ H e)
    (hrad : ∀ v, fderiv ℝ (fderiv ℝ H) e v e = 0)
    (frame : ι → E) (hf : ∀ i, inner ℝ e (frame i) = 0) (i : ι) :
    (∑ j, fderiv ℝ (fun y => (radiusMatrix H frame y).adjugate j i) e (frame j)) = 0 := by
…

Mentions: OAI.AffineBernstein.radiusMatrix