OAI/Analysis/Mahler/ContinuousWedgeDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.differentiableAt_formCoefficient line 13
2. lemma OAI.Mahler.fderiv_formCoefficient line 20
3. lemma OAI.Mahler.differentiableAt_basisContinuousWedge line 29
4. theorem OAI.Mahler.fderiv_basisContinuousWedge line 39

   Source documentation

   The Frechet product rule for the continuous, actual shuffle wedge.

   theorem fderiv_basisContinuousWedge (basis : Module.Basis J ℝ E)
       {A : E → E [⋀^ι]→L[ℝ] ℂ} {B : E → E [⋀^κ]→L[ℝ] ℂ} {x : E}
       (hA : DifferentiableAt ℝ A x) (hB : DifferentiableAt ℝ B x) (u : E) :
       fderiv ℝ (fun y => basisContinuousWedge basis (A y) (B y)) x u =
         basisContinuousWedge basis (fderiv ℝ A x u) (B x) +
         basisContinuousWedge basis (A x) (fderiv ℝ B x u) := by
   …

   Mentions: OAI.Mahler.basisContinuousWedge