OAI/Analysis/Mahler/SourceRawJets.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.rawCovectorJet line 13

   Source documentation

   Forget continuity only after taking the actual bundled derivative.

   def rawCovectorJet (A : E →L[ℝ] E →L[ℝ] ℂ) : E →ₗ[ℝ] E [⋀^Fin 1]→ₗ[ℝ] ℂ where
   …

2. def OAI.Mahler.rawFirstJet line 18
3. lemma OAI.Mahler.rawFirstJet_apply line 21
4. def OAI.Mahler.rawSecondJet line 24
5. lemma OAI.Mahler.rawSecondJet_apply line 30
6. theorem OAI.Mahler.rawSecondJet_closed line 35

   Source documentation

   Actual symmetry of the second Frechet derivative kills its full alternatization, including the covector-evaluation slot.

   theorem rawSecondJet_closed {a : E → E →L[ℝ] ℂ} {x : E}
       (ha : ContDiffAt ℝ 2 a x) :
       (rawPrefix (rawSecondJet (E := E) (fderiv ℝ (fderiv ℝ a) x))).alternatization = 0 := by
   …

   Mentions: OAI.Mahler.rawPrefix, OAI.Mahler.rawSecondJet

7. theorem OAI.Mahler.rawFirstJet_alternatization line 48

   Source documentation

   The raw first jet alternates to the exterior derivative.

   theorem rawFirstJet_alternatization {a : E → E →L[ℝ] ℂ} {x : E}
       (ha : DifferentiableAt ℝ a x) :
       (rawFirstJet (fderiv ℝ a x)).alternatization = (extDeriv (oneForm a) x).toAlternatingMap := by
   …

   Mentions: OAI.Mahler.rawFirstJet, OAI.Mahler.oneForm