PiolaAlgebra.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.continuousDetRows line 13
Source documentation
The determinant, as a continuous map multilinear in its rows.
```
def continuousDetRows : ContinuousMultilinearMap ℝ (fun _ : ι => ι → ℝ) ℝ :=
…
```
theorem OAI.AffineBernstein.continuousDetRows_apply line 18

theorem OAI.AffineBernstein.det_updateRow_pair_swap line 22

Source documentation

Exchanging two independently replaced rows reverses the determinant.

theorem det_updateRow_pair_swap (A : Matrix ι ι ℝ) {i l : ι} (hil : i ≠ l)
    (v w : ι → ℝ) :
    ((A.updateRow i v).updateRow l w).det =
      -((A.updateRow i w).updateRow l v).det := by
…

theorem OAI.AffineBernstein.det_updateRow_sum line 44

Source documentation

Expand one determinant row in the coordinate vectors.

theorem det_updateRow_sum (A : Matrix ι ι ℝ) (l : ι) (v : ι → ℝ) :
    (A.updateRow l v).det = ∑ m, v m * (A.updateRow l (Pi.single m 1)).det := by
…

theorem OAI.AffineBernstein.sum_two_rows_eq_zero line 58

Source documentation

Symmetric coefficients contract to zero with an alternating pair of rows.

theorem sum_two_rows_eq_zero (A : Matrix ι ι ℝ) {i l : ι} (hil : i ≠ l)
    (T : ι → ι → ℝ) (hT : ∀ j m, T j m = T m j) :
    (∑ j, ∑ m, T j m *
      ((A.updateRow i (Pi.single j 1)).updateRow l (Pi.single m 1)).det) = 0 := by
…

theorem OAI.AffineBernstein.piola_cancel line 80

Source documentation

The algebraic cancellation underlying the Piola identity.

theorem piola_cancel (A : Matrix ι ι ℝ) (i : ι) (T : ι → ι → ι → ℝ)
    (hT : ∀ l j m, T l j m = T l m j) :
    (∑ j, ∑ l, ((A.updateRow i (Pi.single j 1)).updateRow l
      (if l = i then 0 else T l j)).det) = 0 := by
…