PairTransgression.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.pairExterior line 13
Source documentation
The actual ordered two-form alpha wedge beta, as a continuous form.
```
noncomputable def pairExterior (a b : E →L[ℝ] ℂ) : E [⋀^Fin 2]→L[ℝ] ℂ :=
…
```
lemma OAI.Mahler.pairExterior_apply line 20
lemma OAI.Mahler.pairExterior_toAlternatingMap line 25
lemma OAI.Mahler.differentiableAt_pairExterior line 34
lemma OAI.Mahler.contDiffAt_pairExterior line 51
lemma OAI.Mahler.fderiv_pairExterior_eval line 75
lemma OAI.Mahler.covectorVolume_one line 89

theorem OAI.Mahler.extDeriv_pairExterior line 98

Source documentation

The negative-sign exterior Leibniz identity for two actual one-forms. All derivatives are exterior derivatives, and the shuffle order is identified explicitly with the standard three slots.

theorem extDeriv_pairExterior {J : Type*} [Fintype J]
    (basis : Module.Basis J ℝ E) {a b : E → E →L[ℝ] ℂ} {x : E}
    (ha : DifferentiableAt ℝ a x) (hb : DifferentiableAt ℝ b x) :
    (extDeriv (fun y => pairExterior (a y) (b y)) x).toAlternatingMap =
      (wedge (oneForm b x).toAlternatingMap (extDeriv (oneForm a) x).toAlternatingMap).domDomCongr
        (prependFinEquiv 2) -
      (wedge (oneForm a x).toAlternatingMap (extDeriv (oneForm b) x).toAlternatingMap).domDomCongr
        (prependFinEquiv 2) := by
…

Mentions: OAI.Mahler.pairExterior, OAI.Mahler.wedge, OAI.Mahler.oneForm, OAI.Mahler.prependFinEquiv