OAI/Analysis/Mahler/OpenHessian.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.diff_numerator_of_open line 13
2. lemma OAI.Mahler.dbar_numerator_of_open line 19
3. theorem OAI.Mahler.mixed_energy_of_open line 34

   Source documentation

   Actual mixed Wirtinger derivative of the squared norm.

   theorem mixed_energy_of_open {f : ι → E → ℂ} {U : Set E} {x v w : E}
       (hU : IsOpen U) (hx : x ∈ U) (hf : ∀ j, DifferentiableOn ℂ (f j) U) :
       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

4. theorem OAI.Mahler.mixed_logTau_of_open line 47

   Source documentation

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

   theorem mixed_logTau_of_open {f : ι → E → ℂ} {U : Set E} {x v w : E}
       (hU : IsOpen U) (hx : x ∈ U) (hf : ∀ j, DifferentiableOn ℂ (f j) U) (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

5. lemma OAI.Mahler.complexHessian_logTau_eq_of_open line 74
6. theorem OAI.Mahler.complexHessian_logTau_posSemidef_of_open line 82
7. lemma OAI.Mahler.complexHessian_energy_eq_gram_of_open line 90
8. theorem OAI.Mahler.complexHessian_energy_posSemidef_of_open line 97
9. theorem OAI.Mahler.sourceHessian_logTau_det_nonneg_of_open line 104
10. theorem OAI.Mahler.sourceHessian_energy_det_nonneg_of_open line 112
11. theorem OAI.Mahler.MassHypotheses.massDensity_nonneg line 121

    Source documentation

    The mass density is nonnegative under the mass hypotheses.

    theorem MassHypotheses.massDensity_nonneg {n N m : ℕ} {U : Set (ComplexEuclidean n)}
        {f : Fin N → ComplexEuclidean n → ℂ} {G : Fin N → MvPolynomial (Fin n) ℂ}
        (h : MassHypotheses n N m U f G) {z : ComplexEuclidean n} (hz : z ∈ U) :
        0 ≤ massDensity f z := by
    …

    Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.massDensity