30.11. Abel.AbelPairingPositivity🔗

Jacobians.Abel.AbelPairingPositivity — source

constCF

The constant c as a SmoothCFunctions.

def constCF (c : ℂ) : SmoothCFunctions X

constCF_apply

@[simp] theorem constCF_apply (c : ℂ) (x : X) : (constCF (X := X) c) x = c

pairForm_cSmul_const

⟨η, c·g⟩ = c·⟨η, g⟩ for a constant ℂ-scale of the (0,1)-slot.

theorem pairForm_cSmul_const (η : HolomorphicOneForms X) (c : ℂ) (g : SmoothCOneForms X) :
    pairForm η (cSmulForm (constCF c) g) = c * pairForm η g

conjForm_add

theorem conjForm_add (η₁ η₂ : HolomorphicOneForms X) :
    conjForm (η₁ + η₂) = conjForm η₁ + conjForm η₂

conjForm_zero

theorem conjForm_zero : conjForm (0 : HolomorphicOneForms X) = 0

conjForm_smul

Conjugation of a ℂ-scaled form: conj(c·η) = c̄·conj(η) (as a cSmulForm).

theorem conjForm_smul (c : ℂ) (η : HolomorphicOneForms X) :
    conjForm (c • η) = cSmulForm (constCF ((starRingEnd ℂ) c)) (conjForm η)

conjForm_sum

theorem conjForm_sum {ι : Type*} (s : Finset ι) (f : ι → HolomorphicOneForms X) :
    conjForm (∑ k ∈ s, f k) = ∑ k ∈ s, conjForm (f k)

pairForm_eta_zero

theorem pairForm_eta_zero (g : SmoothCOneForms X) :
    pairForm (0 : HolomorphicOneForms X) g = 0

pairForm_eta_sum

theorem pairForm_eta_sum {ι : Type*} (s : Finset ι) (f : ι → HolomorphicOneForms X)
    (g : SmoothCOneForms X) :
    pairForm (∑ k ∈ s, f k) g = ∑ k ∈ s, pairForm (f k) g

pairForm_conjForm_ne_zero

Positivity of the conjugate pairing (Forster 19.6-style): for η ≠ 0, pairForm η (conjForm η) ≠ 0 — each chart piece is ∫ ρⱼ·|h|² ≥ 0 and some piece is strictly positive at a point where the coefficient and the PoU weight are both nonzero.

theorem pairForm_conjForm_ne_zero {η : HolomorphicOneForms X} (hη : η ≠ 0) :
    pairForm η (conjForm η) ≠ 0