SmoothCoefficients.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.contDiffAt_hessian_entry line 12
Source documentation
The frozen coordinate Hessian has smooth entries at every interior smooth point.
```
theorem contDiffAt_hessian_entry {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (i j : Fin n) :
    ContDiffAt ℝ ∞ (fun y => hessian u y i j) x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian
theorem OAI.AffineBernstein.contDiffAt_det_hessian line 19
Source documentation
Determinants of the actual Hessian are smooth, by row multilinearity.
```
theorem contDiffAt_det_hessian {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) : ContDiffAt ℝ ∞ (fun y => (hessian u y).det) x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian
theorem OAI.AffineBernstein.contDiffAt_adjugate_hessian_entry line 26
Source documentation
Polynomial cofactor entries are smooth even before invertibility is used.
```
theorem contDiffAt_adjugate_hessian_entry {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (i j : Fin n) :
    ContDiffAt ℝ ∞ (fun y => (hessian u y).adjugate i j) x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.contDiffAt_cofactorHessian_entry line 51

Source documentation

Smoothness of U on its actual open domain, with no extension hypothesis.

theorem contDiffAt_cofactorHessian_entry {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) {x : Space n} (hx : x ∈ Ω) (i j : Fin n) :
    ContDiffAt ℝ ∞ (fun y => cofactorHessian u y i j) x := by
…

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

theorem OAI.AffineBernstein.contDiffAt_affineWeight line 60
Source documentation
The real determinant weight has its original exponent throughout the proof.
```
theorem contDiffAt_affineWeight {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (hpos : (hessian u x).PosDef) :
    ContDiffAt ℝ ∞ (affineWeight u) x :=
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineWeight