PiolaDifferential.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.jacobianRows line 15
Source documentation
Rows of the derivative of a list of scalar functions, in fixed directions.
```
def jacobianRows (F : ι → E → ℝ) (e : ι → E) (x : E) : Matrix ι ι ℝ :=
…
```

theorem OAI.AffineBernstein.fderiv_adjugate_jacobianRows line 19

Source documentation

Differentiate a cofactor by differentiating each of its unfrozen rows.

theorem fderiv_adjugate_jacobianRows (F : ι → E → ℝ) (e : ι → E) (x : E)
    (hF : ∀ l, ContDiffAt ℝ 2 (F l) x) (i j : ι) (v : E) :
    fderiv ℝ (fun y => (jacobianRows F e y).adjugate j i) x v =
      ∑ l, (((jacobianRows F e x).updateRow i (Pi.single j 1)).updateRow l
        (if l = i then 0 else fun m => fderiv ℝ (fderiv ℝ (F l)) x v (e m))).det := by
…

Mentions: OAI.AffineBernstein.jacobianRows

theorem OAI.AffineBernstein.piola_identity line 61

Source documentation

Piola's identity in fixed directions; it uses only equality of mixed partials.

theorem piola_identity (F : ι → E → ℝ) (e : ι → E) (x : E)
    (hF : ∀ l, ContDiffAt ℝ 2 (F l) x) (i : ι) :
    (∑ j, fderiv ℝ (fun y => (jacobianRows F e y).adjugate j i) x (e j)) = 0 := by
…

Mentions: OAI.AffineBernstein.jacobianRows