OAI/Analysis/Mahler/MatrixHessian.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.pairing_sum_right line 11
2. lemma OAI.Mahler.pairing_sum_left line 15
3. lemma OAI.Mahler.pairing_mul_right line 19
4. lemma OAI.Mahler.pairing_mul_left line 22
5. lemma OAI.Mahler.logKernel_sum_right line 26
6. lemma OAI.Mahler.logKernel_sum_left line 30
7. lemma OAI.Mahler.logKernel_mul_right line 34
8. lemma OAI.Mahler.logKernel_mul_left line 38
9. def OAI.Mahler.kernelMatrix line 43
10. lemma OAI.Mahler.kernelMatrix_hermitian line 47
11. lemma OAI.Mahler.kernelMatrix_quadratic line 52
12. lemma OAI.Mahler.kernelMatrix_posSemidef line 59
13. def OAI.Mahler.complexHessian line 69

    Source documentation

    Mixed Hessian in a finite family of directions; the row is the conjugate index.

    noncomputable def complexHessian (u : E → ℂ) (x : E) (e : κ → E) : Matrix κ κ ℂ :=
    …

14. lemma OAI.Mahler.complexHessian_logTau_eq line 73
15. theorem OAI.Mahler.complexHessian_logTau_posSemidef line 81

    Source documentation

    PSD of the actual complex Hessian, with no assumed Hessian formula.

    theorem complexHessian_logTau_posSemidef {f : ι → E → ℂ} {x : E} (e : κ → E)
        (hf : ∀ j, AnalyticAt ℂ (f j) x) (ht : 0 < tau f x) :
        (complexHessian (logTau f) x e).PosSemidef := by
    …

    Mentions: OAI.Mahler.tau, OAI.Mahler.complexHessian, OAI.Mahler.logTau

16. theorem OAI.Mahler.complexHessian_logTau_det_nonneg line 88

    Source documentation

    The determinant is real and nonnegative, in the complex real-axis order.

    theorem complexHessian_logTau_det_nonneg [DecidableEq κ]
        {f : ι → E → ℂ} {x : E} (e : κ → E)
        (hf : ∀ j, AnalyticAt ℂ (f j) x) (ht : 0 < tau f x) :
        0 ≤ (complexHessian (logTau f) x e).det :=
    …

    Mentions: OAI.Mahler.tau, OAI.Mahler.complexHessian, OAI.Mahler.logTau

17. def OAI.Mahler.jacobian line 94
18. lemma OAI.Mahler.complexHessian_energy_eq_gram line 98
19. theorem OAI.Mahler.complexHessian_energy_posSemidef line 105
20. theorem OAI.Mahler.complexHessian_energy_det_nonneg line 111
21. def OAI.Mahler.sourceHessian line 118

    Source documentation

    Complex Hessian indexing: row k is z_k, column l is bar z_l.

    noncomputable def sourceHessian (u : E → ℂ) (x : E) (e : κ → E) : Matrix κ κ ℂ :=
    …

22. theorem OAI.Mahler.sourceHessian_logTau_det_nonneg line 122

    Source documentation

    The complex Hessian in this indexing has real nonnegative determinant.

    theorem sourceHessian_logTau_det_nonneg [DecidableEq κ]
        {f : ι → E → ℂ} {x : E} (e : κ → E)
        (hf : ∀ j, AnalyticAt ℂ (f j) x) (ht : 0 < tau f x) :
        0 ≤ (sourceHessian (logTau f) x e).det := by
    …

    Mentions: OAI.Mahler.tau, OAI.Mahler.sourceHessian, OAI.Mahler.logTau

23. theorem OAI.Mahler.sourceHessian_energy_det_nonneg line 129