Counting directed nuclear pairs

Each increasing pair occurs in the directed boundary sum once in each orientation.

def LiebThirring.directedNuclearPairEquiv (M : ℕ) : (k : Fin M) × { l : Fin M // l ≠ k } ≃ NuclearPair M ⊕ NuclearPair M

A directed pair is an increasing pair together with its orientation.

Equations

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

theorem LiebThirring.sum_directedNuclearPairs_oriented {M : ℕ} {A : Type u_1} [AddCommMonoid A] (f : (k l : Fin M) → k ≠ l → A) : ∑ k : Fin M, ∑ l : { l : Fin M // l ≠ k }, f k ↑l ⋯ = ∑ p : NuclearPair M, (f (↑p).1 (↑p).2 ⋯ + f (↑p).2 (↑p).1 ⋯)

Group each directed pair with its reverse orientation.

theorem LiebThirring.sum_directedNuclearPairs {M : ℕ} {A : Type u_1} [AddCommMonoid A] (f : (k l : Fin M) → k ≠ l → A) (hf : ∀ (k l : Fin M) (hkl : k ≠ l), f k l hkl = f l k ⋯) : ∑ k : Fin M, ∑ l : { l : Fin M // l ≠ k }, f k ↑l ⋯ = ∑ p : NuclearPair M, f (↑p).1 (↑p).2 ⋯ + ∑ p : NuclearPair M, f (↑p).1 (↑p).2 ⋯

A symmetric directed sum is twice its sum over increasing pairs.