SmoothParameter.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.second_deriv_smul_id line 16
Source comment
A twice differentiated eigenvector equation, still valid at a singular matrix and in dimension one.
```
theorem second_deriv_smul_id {g : ℝ → F} (hg : ContDiff ℝ ∞ g) :
    deriv (deriv (fun t : ℝ => t • g t)) 0 = 2 • deriv g 0 := by
…
```
lemma OAI.AffineBernstein.contDiff_adjugate_shift line 34
lemma OAI.AffineBernstein.contDiff_det_shift line 41
theorem OAI.AffineBernstein.newtonTensor_radial line 51
Source comment
A radial null vector of the Hessian is an eigenvector of its Newton polynomial. No nonsingularity, division by a determinant, or limiting inverse is used.
```
theorem newtonTensor_radial {A : Matrix ι ι ℝ} {v : ι → ℝ}
    (hv : A *ᵥ v = 0) : ∃ c : ℝ, newtonTensor A *ᵥ v = c • v := by
…
```
Mentions: OAI.AffineBernstein.newtonTensor