OAI/Analysis/Mahler/RawAlternationDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.rawAlternatedCoefficientDerivative line 14
2. lemma OAI.Mahler.rawAlternatedCoefficientDerivative_apply line 18
3. theorem OAI.Mahler.HasRawFDerivAt.alternatization line 24
4. theorem OAI.Mahler.extDeriv_of_raw_alternatization line 42

   Source documentation

   Differentiating an actual continuous form presented as a full alternatization is full alternatization of its raw coefficient derivative. The normalization is exactly the exterior derivative, with no factor.

   theorem extDeriv_of_raw_alternatization {n : ℕ}
       {a : E → MultilinearMap ℝ (fun _ : Fin n => E) ℂ}
       {D : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : Fin n => E) ℂ}
       {ω : E → E [⋀^Fin n]→L[ℝ] ℂ} {x : E}
       (hω : DifferentiableAt ℝ ω x)
       (heq : ∀ᶠ y in 𝓝 x, (ω y).toAlternatingMap = (a y).alternatization)
       (ha : HasRawFDerivAt a D x) :
       (extDeriv ω x).toAlternatingMap = D.uncurryLeft.alternatization := by
   …

   Mentions: OAI.Mahler.HasRawFDerivAt