theorem VirasoroProject.heiOper_pairNO_eq_pairNO'.{u_1,
    u_2}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  {heiOper : ℤ → V →ₗ[𝕜] V}
  (heiComm :
    ∀ (k l : ℤ),
      (heiOper k).commutator (heiOper l) =
        if k + l = 0 then ↑k • 1 else 0)
  (k l : ℤ) :
  VirasoroProject.pairNO heiOper k l =
    VirasoroProject.pairNO' heiOper k l

theorem VirasoroProject.pairNO_apply_eq_zero.{u_1,
    u_2}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  (A : ℤ → V →ₗ[𝕜] V) {v : V} {N : ℤ}
  (A_trunc : ∀ n ≥ N, (A n) v = 0)
  {k l : ℤ} (h : N ≤ max k l) :
  (VirasoroProject.pairNO A k l) v = 0

theorem VirasoroProject.hasFiniteSupport_smul_pairNO_apply.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  {heiOper : ℤ → V →ₗ[𝕜] V}
  (heiTrunc :
    ∀ (v : V),
      ∀ᶠ (l : ℤ) in Filter.atTop,
        (heiOper l) v = 0)
  {𝕂 : Type u_3} [Zero 𝕂]
  [SMulZeroClass 𝕂 V] (c : ℤ → 𝕂)
  (n m : ℤ) (v : V) :
  Function.HasFiniteSupport fun k =>
    c k •
      (VirasoroProject.pairNO heiOper
          (n - k) (m + k))
        v

theorem VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply.{u_1,
    u_2}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  {heiOper : ℤ → V →ₗ[𝕜] V}
  (heiTrunc :
    ∀ (v : V),
      ∀ᶠ (l : ℤ) in Filter.atTop,
        (heiOper l) v = 0)
  (n : ℤ) (A : V →ₗ[𝕜] V) (v : V) :
  ((VirasoroProject.sugawaraGen heiTrunc
            n).commutator
        A)
      v =
    2⁻¹ •
      ∑ᶠ (k : ℤ),
        ((VirasoroProject.pairNO heiOper
                (n - k) k).commutator
            A)
          v

theorem VirasoroProject.commutator_sugawaraGen_heiOper.{u_1,
    u_2}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  {heiOper : ℤ → V →ₗ[𝕜] V}
  (heiTrunc :
    ∀ (v : V),
      ∀ᶠ (l : ℤ) in Filter.atTop,
        (heiOper l) v = 0)
  (heiComm :
    ∀ (k l : ℤ),
      (heiOper k).commutator (heiOper l) =
        if k + l = 0 then ↑k • 1 else 0)
  [CharZero 𝕜] (n m : ℤ) :
  (VirasoroProject.sugawaraGen heiTrunc
          n).commutator
      (heiOper m) =
    -↑m • heiOper (n + m)

theorem VirasoroProject.commutator_sugawaraGen_heiPairNO'.{u_1,
    u_2}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  {heiOper : ℤ → V →ₗ[𝕜] V}
  (heiTrunc :
    ∀ (v : V),
      ∀ᶠ (l : ℤ) in Filter.atTop,
        (heiOper l) v = 0)
  (heiComm :
    ∀ (k l : ℤ),
      (heiOper k).commutator (heiOper l) =
        if k + l = 0 then ↑k • 1 else 0)
  [CharZero 𝕜] (n m k : ℤ) :
  (VirasoroProject.sugawaraGen heiTrunc
          n).commutator
      (VirasoroProject.pairNO' heiOper
        (m - k) k) =
    -↑k •
          VirasoroProject.pairNO' heiOper
            (m - k) (n + k) +
        -(↑m - ↑k) •
          VirasoroProject.pairNO' heiOper
            (n + m - k) k +
      (if n + m = 0 then
          ↑k * (↑n + ↑k) *
            ((if k + n ≤ 0 then 1
              else 0) -
              if k ≤ 0 then 1 else 0)
        else 0) •
        1

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

theorem VirasoroProject.commutator_sugawaraGen.{u_1,
    u_2}
  {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2}
  [AddCommGroup V] [Module 𝕜 V]
  {heiOper : ℤ → V →ₗ[𝕜] V}
  (heiTrunc :
    ∀ (v : V),
      ∀ᶠ (l : ℤ) in Filter.atTop,
        (heiOper l) v = 0)
  (heiComm :
    ∀ (k l : ℤ),
      (heiOper k).commutator (heiOper l) =
        if k + l = 0 then ↑k • 1 else 0)
  [CharZero 𝕜] (n m : ℤ) :
  (VirasoroProject.sugawaraGen heiTrunc
          n).commutator
      (VirasoroProject.sugawaraGen
        heiTrunc m) =
    (↑n - ↑m) •
        VirasoroProject.sugawaraGen
          heiTrunc (n + m) +
      if n + m = 0 then
        ((↑n ^ 3 - ↑n) / 12) • 1
      else 0