theorem ΛDecompMem (p q : ℕ) : p ∈ Finset.range (p + q + 1)

def ΛDecomp : (j : ℕ) × { x : ℕ // x ∈ Finset.range (j + 1) } ≃ ℕ × ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem bigeometric_series {K : Type u_1} [RCLike K] (x y : K) (xbound : ‖x‖ < 2⁻¹) (ybound : ‖y‖ < 2⁻¹) : HasSum (fun (pq : ℕ × ℕ) => ↑(Jₚ pq) * x ^ pq.1 * y ^ pq.2) (1 - (x + y))⁻¹