OAI/Analysis/Mahler/ClosedWedgePowers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Mahler.continuousReindex_finCongr_extDeriv line 11
  2. def OAI.Mahler.basisContinuousWedgePower line 18
  3. lemma OAI.Mahler.basisContinuousWedgePower_toAlternatingMap line 24
  4. lemma OAI.Mahler.contDiffAt_basisContinuousWedgePower line 39
  5. lemma OAI.Mahler.differentiableAt_basisContinuousWedgePower line 49
  6. lemma OAI.Mahler.wedge_power_zero_right line 60
  7. lemma OAI.Mahler.wedge_power_zero_left line 66
  8. theorem OAI.Mahler.extDeriv_basisContinuousWedgePower line 72

    Source documentation

    Every power of an actual closed differentiable two-form is closed.

    theorem extDeriv_basisContinuousWedgePower (basis : Module.Basis J ℝ E)
    {A : E → E [⋀^Fin 2]→L[ℝ] ℂ} {x : E}
    (hA : DifferentiableAt ℝ A x) (hclosed : extDeriv A x = 0) (k : ℕ) :
    extDeriv (fun y => basisContinuousWedgePower basis (A y) k) x = 0 := by
…

    Mentions: OAI.Mahler.basisContinuousWedgePower

  9. lemma OAI.Mahler.contDiffAt_extDeriv_power_order line 96