OAI/Analysis/Mahler/ExteriorLeibnizTwo.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.continuousWedgeFin line 13
2. lemma OAI.Mahler.continuousWedgeFin_toAlternatingMap line 18
3. lemma OAI.Mahler.differentiableAt_continuousWedgeFin line 24
4. lemma OAI.Mahler.contDiffAt_continuousWedgeFin line 31
5. lemma OAI.Mahler.fderiv_continuousWedgeFin line 39
6. theorem OAI.Mahler.extDeriv_continuousWedge_two line 56

   Source documentation

   Exterior Leibniz rule for an actual two-form times an arbitrary-degree form. The sign is positive because the left degree is two.

   theorem extDeriv_continuousWedge_two (basis : Module.Basis J ℝ E) {n : ℕ}
       {A : E → E [⋀^Fin 2]→L[ℝ] ℂ} {B : E → E [⋀^Fin n]→L[ℝ] ℂ} {x : E}
       (hA : DifferentiableAt ℝ A x) (hB : DifferentiableAt ℝ B x) :
       (extDeriv (fun y => continuousWedgeFin basis (A y) (B y)) x).toAlternatingMap =
         (wedge (extDeriv A x).toAlternatingMap (B x).toAlternatingMap).domDomCongr
           (derivativeLeftEquiv n) +
         (wedge (A x).toAlternatingMap (extDeriv B x).toAlternatingMap).domDomCongr
           (derivativeRightEquiv n) := by
   …

   Mentions: OAI.Mahler.continuousWedgeFin, OAI.Mahler.wedge, OAI.Mahler.derivativeLeftEquiv, OAI.Mahler.derivativeRightEquiv