symm_Λ₀_eq — Mathlib

English

For the symmetric WeakFEPair P.symm, Λ₀(s) satisfies the analogous decomposition with the roles of f₀ and g₀ swapped and with ε inverted: Λ₀(s) = Λ_symm(s) + (1/s) g₀ + (ε⁻¹/(k − s)) f₀.

Русский

Для симметричного WeakFEPair P.symm выполняется аналогичное разложение с поменянными ролями f₀ и g₀ и с заменой ε на ε⁻¹: Λ₀(s) = Λ_symm(s) + (1/s) g₀ + (ε⁻¹/(k − s)) f₀.

LaTeX

$$$\\Lambda_0^{\\mathrm{symm}}(s) = \\Lambda^{\\mathrm{symm}}(s) + \\frac{1}{s} g_0 + \\frac{\\varepsilon^{-1}}{k - s} f_0$$$

Lean4

theorem symm_Λ₀_eq (s : ℂ) : P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (P.k - s)) • P.f₀ :=
  by
  rw [P.symm.Λ₀_eq]
  rfl

Похожие утверждения