OAI/Analysis/Mahler/SourceRawCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.rawLinearJet line 11
2. lemma OAI.Mahler.rawCovector_hasRawFDerivAt line 16
3. lemma OAI.Mahler.rawFirstJet_hasRawFDerivAt line 26
4. theorem OAI.Mahler.rawBoundary_hasRawFDerivAt line 38

   Source documentation

   The coefficientwise derivative of the full raw form, including every derivative of every first-jet factor.

   theorem rawBoundary_hasRawFDerivAt {a : E → E →L[ℝ] ℂ} {x : E}
       (ha : ContDiffAt ℝ 2 a x) (k : ℕ) :
       HasRawFDerivAt
         (fun y => rawBoundary (a y).toLinearMap (rawFirstJet (fderiv ℝ a y)) k)
         (rawProductVariation (rawCovector (a x).toLinearMap)
           (rawCovectorVariation (rawLinearJet (fderiv ℝ a x)))
           (rawPower (rawFirstJet (fderiv ℝ a x)) k)
           (rawPowerVariation (rawFirstJet (fderiv ℝ a x))
             (rawSecondJet (fderiv ℝ (fderiv ℝ a) x)) k)) x := by
   …

   Mentions: OAI.Mahler.HasRawFDerivAt, OAI.Mahler.rawBoundary, OAI.Mahler.rawFirstJet, OAI.Mahler.rawProductVariation, OAI.Mahler.rawCovector, OAI.Mahler.rawCovectorVariation, OAI.Mahler.rawLinearJet, OAI.Mahler.rawPower, OAI.Mahler.rawPowerVariation, OAI.Mahler.rawSecondJet