OAI/Analysis/Mahler/Positivity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.finite_cauchy_schwarz line 13
2. def OAI.Mahler.pairing line 21
3. def OAI.Mahler.sizeSq line 22
4. def OAI.Mahler.logKernel line 23
5. lemma OAI.Mahler.pairing_conj line 26
6. lemma OAI.Mahler.pairing_self line 28
7. lemma OAI.Mahler.logKernel_conj line 30
8. lemma OAI.Mahler.logKernel_diagonal line 34
9. lemma OAI.Mahler.logKernel_nonneg line 42
10. lemma OAI.Mahler.mixed_logTau_kernel line 50
11. theorem OAI.Mahler.levi_logTau_nonneg line 58

    Source documentation

    Nonnegativity of the actual Levi form, proved using Cauchy-Schwarz.

    theorem levi_logTau_nonneg {f : ι → E → ℂ} {x v : E}
        (hf : ∀ j, AnalyticAt ℂ (f j) x) (ht : 0 < tau f x) :
        0 ≤ dbar (fun y => dz (logTau f) y v) x v := by
    …

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

12. theorem OAI.Mahler.levi_energy_nonneg line 65

    Source documentation

    The actual Levi form of tau is a sum of squared moduli.

    theorem levi_energy_nonneg {f : ι → E → ℂ} {x v : E}
        (hf : ∀ j, AnalyticAt ℂ (f j) x) :
        0 ≤ dbar (fun y => dz (energy f) y v) x v := by
    …

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