OAI/Analysis/Mahler/SourceRealExterior.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.extDeriv_realPart line 12

   Source documentation

   Taking the real part commutes with the actual exterior derivative.

   theorem extDeriv_realPart {n : ℕ} {ω : E → E [⋀^Fin n]→L[ℝ] ℂ} {x : E}
       (hω : DifferentiableAt ℝ ω x) :
       extDeriv (fun y => Complex.reCLM.compContinuousAlternatingMap (ω y)) x =
         Complex.reCLM.compContinuousAlternatingMap (extDeriv ω x) := by
   …

2. theorem OAI.Mahler.extDeriv_sourceRealBoundaryForm line 34