ExteriorHessian.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.mixed_second_real line 14

Source documentation

Actual mixed derivatives expanded in the real second Fréchet derivative.

lemma mixed_second_real [IsScalarTower ℝ ℂ E] {u : E → ℂ} {x v w : E} (hu : ContDiffAt ℝ 2 u x) :
    dbar (fun y => dz u y v) x w =
      (fderiv ℝ (fderiv ℝ u) x w v - I * fderiv ℝ (fderiv ℝ u) x w (I • v) +
        I * fderiv ℝ (fderiv ℝ u) x (I • w) v +
        fderiv ℝ (fderiv ℝ u) x (I • w) (I • v)) / 4 := by
…

Mentions: OAI.Mahler.dbar, OAI.Mahler.dz

theorem OAI.Mahler.extDeriv_dc_mixed line 31
Source documentation
The exterior derivative of the d^c one-form is exactly the antisymmetrized mixed Hessian, with coefficient i/2.
```
theorem extDeriv_dc_mixed {u : E → ℂ} {x : E} (hu : ContDiffAt ℝ 2 u x) (v w : E) :
    extDeriv (oneForm (dcLinear u)) x ![v, w] =
      (I / 2) * (dbar (fun y => dz u y v) x w - dbar (fun y => dz u y w) x v) := by
…
```
Mentions: OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.dbar, OAI.Mahler.dz

theorem OAI.Mahler.extDeriv_dc_logTau_of_open line 54

Source documentation

The exterior two-form identity, with no added regularity.

theorem extDeriv_dc_logTau_of_open [FiniteDimensional ℂ E]
    {ι : Type*} [Fintype ι] {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) :
    extDeriv (oneForm (dcLinear (logTau f))) x ![v, w] =
      (I / 2) *
        (logKernel (fun j => f j x) (fun j => fderiv ℂ (f j) x w)
          (fun j => fderiv ℂ (f j) x v) -
         logKernel (fun j => f j x) (fun j => fderiv ℂ (f j) x v)
          (fun j => fderiv ℂ (f j) x w)) := by
…

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