OAI/Analysis/Mahler/SourceExteriorDerivative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.continuousWedgeCLM_apply line 13
2. theorem OAI.Mahler.fderiv_continuousWedge_apply line 17

   Source documentation

   Actual real Frechet differentiation of the whole shuffle product.

   theorem fderiv_continuousWedge_apply {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
       {a : X → E [⋀^ι]→L[ℝ] ℂ} {b : X → E [⋀^κ]→L[ℝ] ℂ} {x : X}
       (ha : DifferentiableAt ℝ a x) (hb : DifferentiableAt ℝ b x) (v : X) :
       fderiv ℝ (fun y => continuousWedge (a y) (b y)) x v =
         continuousWedge (fderiv ℝ a x v) (b x) + continuousWedge (a x) (fderiv ℝ b x v) := by
   …

   Mentions: OAI.Mahler.continuousWedge

3. def OAI.Mahler.continuousWedgePowerVariation line 38

   Source documentation

   The exact finite product-rule variation of a bundled exterior power.

   def continuousWedgePowerVariation (a da : E [⋀^Fin 2]→L[ℝ] ℂ) :
       (k : ℕ) → E [⋀^WedgePowerSlots k]→L[ℝ] ℂ
     | 0 => 0
     | k+1 => continuousWedge da (continuousWedgePower a k) +
         continuousWedge a (continuousWedgePowerVariation a da k)

   Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.continuousWedge, OAI.Mahler.continuousWedgePower

4. theorem OAI.Mahler.fderiv_continuousWedgePower_apply line 44
5. theorem OAI.Mahler.extDeriv_sourceDDC_zero line 62

   Source documentation

   Closedness of the actual dd^c field is a consequence of symmetric second derivatives, through d²=0.

   theorem extDeriv_sourceDDC_zero {u : E → ℂ} {x : E}
       (hu : ContDiffAt ℝ 3 u x) :
       extDeriv (extDeriv (oneForm (dcLinear u))) x = 0 := by
   …

   Mentions: OAI.Mahler.oneForm, OAI.Mahler.dcLinear

6. theorem OAI.Mahler.MassHypotheses.extDeriv_energyDDC_zero line 72
7. theorem OAI.Mahler.MassHypotheses.extDeriv_logDDC_zero line 77