OAI/Analysis/Mahler/LevelForms.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.contDiffAt_energy_of_open line 14
2. lemma OAI.Mahler.dc_logTau_eq_div line 25
3. theorem OAI.Mahler.extDeriv_logTau_on_level line 39

   Source documentation

   On tangent vectors to an energy level, the actual exterior log form is energy^{-1} times the energy form. This is local calculus, not Stokes.

   theorem extDeriv_logTau_on_level {f : ι → E → ℂ} {U : Set E} {x : E}
       (hU : IsOpen U) (hx : x ∈ U) (hf : ∀ j, DifferentiableOn ℂ (f j) U)
       (ht : 0 < tau f x) (v w : E)
       (hv : fderiv ℝ (energy f) x v = 0) (hw : fderiv ℝ (energy f) x w = 0) :
       extDeriv (oneForm (dcLinear (logTau f))) x ![v, w] =
         (energy f x)⁻¹ * extDeriv (oneForm (dcLinear (energy f))) x ![v, w] := by
   …

   Mentions: OAI.Mahler.tau, OAI.Mahler.energy, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau