OAI/Analysis/Mahler/Hessian.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.dz line 19

   Source documentation

   Wirtinger derivative, defined from the real Frechet derivative.

   noncomputable def dz (u : E → ℂ) (x v : E) : ℂ :=
   …

2. def OAI.Mahler.dbar line 22

   Source documentation

   Conjugate Wirtinger derivative with the same normalization.

   noncomputable def dbar (u : E → ℂ) (x v : E) : ℂ :=
   …

3. lemma OAI.Mahler.dz_holomorphic line 25
4. lemma OAI.Mahler.dbar_holomorphic line 36
5. lemma OAI.Mahler.dz_conj line 47
6. lemma OAI.Mahler.dbar_conj line 56
7. lemma OAI.Mahler.dz_mul line 65
8. lemma OAI.Mahler.dbar_mul line 75
9. lemma OAI.Mahler.dz_sum line 85
10. lemma OAI.Mahler.dbar_sum line 95
11. lemma OAI.Mahler.dz_clog line 105
12. lemma OAI.Mahler.dbar_div line 115
13. def OAI.Mahler.tau line 131

    Source documentation

    The squared Euclidean norm of a finite holomorphic map.

    noncomputable def tau (f : ι → E → ℂ) (x : E) : ℝ := ∑ j, normSq (f j x)

14. def OAI.Mahler.energy line 132
15. def OAI.Mahler.logTau line 133
16. lemma OAI.Mahler.tau_nonneg line 136
17. lemma OAI.Mahler.energy_eq_tau line 139
18. lemma OAI.Mahler.logTau_eq line 141
19. lemma OAI.Mahler.diff_conj line 146
20. lemma OAI.Mahler.differentiable_energy line 150
21. lemma OAI.Mahler.dz_energy line 155
22. lemma OAI.Mahler.dbar_energy line 167
23. lemma OAI.Mahler.dz_logTau line 179
24. lemma OAI.Mahler.dbar_congr_nhds line 187
25. def OAI.Mahler.numerator line 191
26. lemma OAI.Mahler.diff_first line 195
27. lemma OAI.Mahler.diff_numerator line 199
28. lemma OAI.Mahler.dbar_numerator line 205
29. theorem OAI.Mahler.mixed_energy line 220

    Source documentation

    Actual mixed Wirtinger derivative of the squared norm.

    theorem mixed_energy {f : ι → E → ℂ} {x v w : E}
        (hf : ∀ j, AnalyticAt ℂ (f j) x) :
        dbar (fun y => dz (energy f) y v) x w =
          ∑ j, conj (fderiv ℂ (f j) x w) * fderiv ℂ (f j) x v := by
    …

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

30. theorem OAI.Mahler.mixed_logTau line 232

    Source documentation

    Actual mixed derivative of the real logarithm, on the positive tau domain.

    theorem mixed_logTau {f : ι → E → ℂ} {x v w : E}
        (hf : ∀ j, AnalyticAt ℂ (f j) x) (ht : 0 < tau f x) :
        dbar (fun y => dz (logTau f) y v) x w =
          ((tau f x : ℂ) * (∑ j, conj (fderiv ℂ (f j) x w) * fderiv ℂ (f j) x v)
            - (∑ j, conj (f j x) * fderiv ℂ (f j) x v) *
              (∑ j, conj (fderiv ℂ (f j) x w) * f j x)) / (tau f x : ℂ)^2 := by
    …

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