Central charge calculations for Sugawara constructions

This file contains the crucial auxiliary calculations leading to the values of the central charge in various Sugawara constructions. The calculations make use of "discrete integration" on ℤ.

Main definitions

• zPrimitive: A "discrete integral function" to a given function f : ℤ → R. The defining properties of F = zPrimitive f are F(0) = 0 and F(n+1) - F(n) = f(n).
• zMonomialF: The dth discrete monomial function is defined by d-fold discrete integration starting from the function 1. (The continuum analogue is the monomial 1/d! • x^d.)

Main statements

• zMonomialF_eq The dth discrete monomial function is given by n ↦ 1/d! • ∏ j (0 ≤ j < d), (n - j)
• bosonic_sugawara_cc_calc: For any n ∈ ℤ, we have zPrimitive (fun l ↦ (l : R) * (n - l)) n = (n^3 - n) / 6.
• bosonic_sugawara_cc_calc_nonneg: For any n ∈ ℕ, we have ∑ l (0 ≤ l < n), (l : ℚ) * (n - l) = (n^3 - n) / 6.

TODO

• TODO: Add variants of the calculation for fermionic Sugawara constructions etc.

Tags

central charge, Sugawara construction

def VirasoroProject.zPrimitive {R : Type u_1} [AddCommGroup R] (f : ℤ → R) (n : ℤ) : R

A discrete integral of a function on ℤ.

Equations

• VirasoroProject.zPrimitive f n = if 0 ≤ n then ∑ j ∈ Finset.range n.toNat, f ↑j else -∑ j ∈ Finset.range n.natAbs, f (-↑j - 1)

@[simp]

theorem VirasoroProject.zPrimitive_zero {R : Type u_1} [AddCommGroup R] (f : ℤ → R) : zPrimitive f 0 = 0

@[simp]

theorem VirasoroProject.zPrimitive_apply_of_nonneg {R : Type u_1} [AddCommGroup R] (f : ℤ → R) {n : ℤ} (hn : 0 ≤ n) : zPrimitive f n = ∑ j ∈ Finset.range n.toNat, f ↑j

@[simp]

theorem VirasoroProject.zPrimitive_apply_of_nonpos {R : Type u_1} [AddCommGroup R] (f : ℤ → R) {n : ℤ} (hn : n ≤ 0) : zPrimitive f n = -∑ j ∈ Finset.range n.natAbs, f (-↑j - 1)

@[simp]

theorem VirasoroProject.zPrimitive_succ {R : Type u_1} [AddCommGroup R] (f : ℤ → R) (n : ℤ) : zPrimitive f (n + 1) = zPrimitive f n + f n

theorem VirasoroProject.eq_zPrimitive_of_eq_zero_of_forall_eq_add {R : Type u_1} [AddCommGroup R] {f F : ℤ → R} (h0 : F 0 = 0) (h1 : ∀ (n : ℤ), F (n + 1) = F n + f n) : F = zPrimitive f

theorem VirasoroProject.zPrimitive_add {R : Type u_1} [AddCommGroup R] (f g : ℤ → R) : zPrimitive (f + g) = zPrimitive f + zPrimitive g

theorem VirasoroProject.zPrimitive_smul {R : Type u_1} {S : Type u_2} [AddCommGroup R] [DistribSMul S R] (c : S) (f : ℤ → R) : zPrimitive (c • f) = c • zPrimitive f

theorem VirasoroProject.zPrimitive_sub {R : Type u_1} [AddCommGroup R] (f g : ℤ → R) : zPrimitive (f - g) = zPrimitive f - zPrimitive g

theorem VirasoroProject.zPrimitive_mul_left {R : Type u_1} [Ring R] (c : R) (f : ℤ → R) : (zPrimitive fun (n : ℤ) => c * f n) = fun (n : ℤ) => c * zPrimitive f n

theorem VirasoroProject.zPrimitive_mul_right {R : Type u_1} [Ring R] (c : R) (f : ℤ → R) : (zPrimitive fun (n : ℤ) => f n * c) = fun (n : ℤ) => zPrimitive f n * c

def VirasoroProject.zMonomialF (R : Type u_1) [AddCommGroup R] [One R] (d : ℕ) : ℤ → R

A discrete monomial function of degree d, obtained recursively by starting from the unit function 1 and taking the discrete primitive d times. (Note: The resulting normalization is such that this monomial approximately x ↦ 1/d! * x^d.)

Equations

• VirasoroProject.zMonomialF R 0 = fun (x : ℤ) => 1
• VirasoroProject.zMonomialF R d_2.succ = VirasoroProject.zPrimitive (VirasoroProject.zMonomialF R d_2)

theorem VirasoroProject.zMonomialF_eq (R : Type u_1) [Field R] [CharZero R] (d : ℕ) : zMonomialF R d = fun (n : ℤ) => (∏ j ∈ Finset.range d, (↑n - ↑j)) / ↑d.factorial

theorem VirasoroProject.zMonomialF_zero_eq (R : Type u_1) [Field R] (n : ℤ) : zMonomialF R 0 n = 1

theorem VirasoroProject.zMonomialF_one_eq (R : Type u_1) [Field R] [CharZero R] (n : ℤ) : zMonomialF R 1 n = ↑n

theorem VirasoroProject.zMonomialF_two_eq (R : Type u_1) [Field R] [CharZero R] (n : ℤ) : zMonomialF R 2 n = ↑n * (↑n - 1) / 2

theorem VirasoroProject.zMonomialF_three_eq (R : Type u_1) [Field R] [CharZero R] (n : ℤ) : zMonomialF R 3 n = ↑n * (↑n - 1) * (↑n - 2) / 6

theorem VirasoroProject.zMonomialF_four_eq (R : Type u_1) [Field R] [CharZero R] (n : ℤ) : zMonomialF R 4 n = ↑n * (↑n - 1) * (↑n - 2) * (↑n - 3) / 24

theorem VirasoroProject.zMonomialF_five_eq (R : Type u_1) [Field R] [CharZero R] (n : ℤ) : zMonomialF R 5 n = ↑n * (↑n - 1) * (↑n - 2) * (↑n - 3) * (↑n - 4) / 120

theorem VirasoroProject.zMonomialF_apply_eq_zero_of_of_nonneg_lt (R : Type u_1) [Field R] [CharZero R] (d : ℕ) {n : ℕ} (n_lt : n < d) : zMonomialF R d ↑n = 0

theorem VirasoroProject.bosonic_sugawara_cc_calc (R : Type u_1) [Field R] [CharZero R] (n : ℤ) : zPrimitive (fun (l : ℤ) => ↑l * (↑n - ↑l)) n = (↑n ^ 3 - ↑n) / 6

theorem VirasoroProject.bosonic_sugawara_cc_calc_nonneg (n : ℕ) : ∑ l ∈ Finset.range n, ↑l * (↑n - ↑l) = (↑n ^ 3 - ↑n) / 6