PhyslibAlpha.QuantumMechanics.QuantumHarmonicOscillator

PhyslibAlpha
QuantumMechanics
QuantumHarmonicOscillator

Imports

/-
Copyright (c) 2026 Bjørn Kjos-Hanssen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bjørn Kjos-Hanssen
-/
module
public import Mathlib.Data.Matrix.PEquiv
public import Mathlib.Probability.Distributions.Poisson.Basic
public import Mathlib.Analysis.Normed.Lp.lpSpace

Quantum harmonic oscillator

Annihilation operator.

def a (x : ℕ → ℂ) : ℕ → ℂ := fun n => √(n + 1) * x (n + 1)

def aLin : (ℕ → ℂ) →ₗ[ℂ] (ℕ → ℂ) := {
  toFun := a
  map_add' := by⊢ ∀ (x y : ℕ → ℂ), a (x + y) = a x + a y
    unfold a⊢ ∀ (x y : ℕ → ℂ),
  (fun n => ↑√(↑n + 1) * (x + y) (n + 1)) = (fun n => ↑√(↑n + 1) * x (n + 1)) + fun n => ↑√(↑n + 1) * y (n + 1)
    intro x yx:ℕ → ℂy:ℕ → ℂ⊢ (fun n => ↑√(↑n + 1) * (x + y) (n + 1)) = (fun n => ↑√(↑n + 1) * x (n + 1)) + fun n => ↑√(↑n + 1) * y (n + 1)
    ext nx:ℕ → ℂy:ℕ → ℂn:ℕ⊢ ↑√(↑n + 1) * (x + y) (n + 1) = ((fun n => ↑√(↑n + 1) * x (n + 1)) + fun n => ↑√(↑n + 1) * y (n + 1)) n
    simp only [Pi.add_apply]x:ℕ → ℂy:ℕ → ℂn:ℕ⊢ ↑√(↑n + 1) * (x (n + 1) + y (n + 1)) = ↑√(↑n + 1) * x (n + 1) + ↑√(↑n + 1) * y (n + 1)
    ring_nfAll goals completed! 🐙
  map_smul' := by⊢ ∀ (m : ℂ) (x : ℕ → ℂ), a (m • x) = (RingHom.id ℂ) m • a x
    intro m xm:ℂx:ℕ → ℂ⊢ a (m • x) = (RingHom.id ℂ) m • a x
    unfold am:ℂx:ℕ → ℂ⊢ (fun n => ↑√(↑n + 1) * (m • x) (n + 1)) = (RingHom.id ℂ) m • fun n => ↑√(↑n + 1) * x (n + 1)
    ext nm:ℂx:ℕ → ℂn:ℕ⊢ ↑√(↑n + 1) * (m • x) (n + 1) = ((RingHom.id ℂ) m • fun n => ↑√(↑n + 1) * x (n + 1)) n
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]m:ℂx:ℕ → ℂn:ℕ⊢ ↑√(↑n + 1) * (m * x (n + 1)) = m * (↑√(↑n + 1) * x (n + 1))
    ring_nfAll goals completed! 🐙
}

Creation operator.

def a_dag (x : ℕ → ℂ) : ℕ → ℂ := fun n => ite (n = 0) 0 (√n * x (n - 1))

def a_dagLin : (ℕ → ℂ) →ₗ[ℂ] (ℕ → ℂ) := {
  toFun := a_dag
  map_add' := by⊢ ∀ (x y : ℕ → ℂ), a_dag (x + y) = a_dag x + a_dag y
    unfold a_dag⊢ ∀ (x y : ℕ → ℂ),
  (fun n => if n = 0 then 0 else ↑√↑n * (x + y) (n - 1)) =
    (fun n => if n = 0 then 0 else ↑√↑n * x (n - 1)) + fun n => if n = 0 then 0 else ↑√↑n * y (n - 1)
    intro x yx:ℕ → ℂy:ℕ → ℂ⊢ (fun n => if n = 0 then 0 else ↑√↑n * (x + y) (n - 1)) =
  (fun n => if n = 0 then 0 else ↑√↑n * x (n - 1)) + fun n => if n = 0 then 0 else ↑√↑n * y (n - 1)
    ext nx:ℕ → ℂy:ℕ → ℂn:ℕ⊢ (if n = 0 then 0 else ↑√↑n * (x + y) (n - 1)) =
  ((fun n => if n = 0 then 0 else ↑√↑n * x (n - 1)) + fun n => if n = 0 then 0 else ↑√↑n * y (n - 1)) n
    simp only [Pi.add_apply]x:ℕ → ℂy:ℕ → ℂn:ℕ⊢ (if n = 0 then 0 else ↑√↑n * (x (n - 1) + y (n - 1))) =
  (if n = 0 then 0 else ↑√↑n * x (n - 1)) + if n = 0 then 0 else ↑√↑n * y (n - 1)
    ring_nfx:ℕ → ℂy:ℕ → ℂn:ℕ⊢ (if n = 0 then 0 else ↑√↑n * x (n - 1) + ↑√↑n * y (n - 1)) =
  (if n = 0 then 0 else ↑√↑n * x (n - 1)) + if n = 0 then 0 else ↑√↑n * y (n - 1)
    split_ifsposx:ℕ → ℂy:ℕ → ℂn:ℕh✝:n = 0⊢ 0 = 0 + 0negx:ℕ → ℂy:ℕ → ℂn:ℕh✝:¬n = 0⊢ ↑√↑n * x (n - 1) + ↑√↑n * y (n - 1) = ↑√↑n * x (n - 1) + ↑√↑n * y (n - 1) <;>posx:ℕ → ℂy:ℕ → ℂn:ℕh✝:n = 0⊢ 0 = 0 + 0negx:ℕ → ℂy:ℕ → ℂn:ℕh✝:¬n = 0⊢ ↑√↑n * x (n - 1) + ↑√↑n * y (n - 1) = ↑√↑n * x (n - 1) + ↑√↑n * y (n - 1) simpAll goals completed! 🐙
  map_smul' := by⊢ ∀ (m : ℂ) (x : ℕ → ℂ), a_dag (m • x) = (RingHom.id ℂ) m • a_dag x
    intro m xm:ℂx:ℕ → ℂ⊢ a_dag (m • x) = (RingHom.id ℂ) m • a_dag x
    unfold a_dagm:ℂx:ℕ → ℂ⊢ (fun n => if n = 0 then 0 else ↑√↑n * (m • x) (n - 1)) =
  (RingHom.id ℂ) m • fun n => if n = 0 then 0 else ↑√↑n * x (n - 1)
    ext nm:ℂx:ℕ → ℂn:ℕ⊢ (if n = 0 then 0 else ↑√↑n * (m • x) (n - 1)) = ((RingHom.id ℂ) m • fun n => if n = 0 then 0 else ↑√↑n * x (n - 1)) n
    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, mul_ite, mul_zero]m:ℂx:ℕ → ℂn:ℕ⊢ (if n = 0 then 0 else ↑√↑n * (m * x (n - 1))) = if n = 0 then 0 else m * (↑√↑n * x (n - 1))
    ring_nfAll goals completed! 🐙
}

def ε (n : ℕ) (c : ℂ) : ℕ → ℂ := fun i => ite (i = n) c 0

Verify that a_dag really is the transpose of a.


lemma a_dag_eq (i j : ℕ) : a_dag (ε i 1) j = star (a (ε j 1) i) := byi:ℕj:ℕ⊢ a_dag (ε i 1) j = star (a (ε j 1) i)
    unfold a a_dag εi:ℕj:ℕ⊢ (if j = 0 then 0 else ↑√↑j * if j - 1 = i then 1 else 0) = star (↑√(↑i + 1) * if i + 1 = j then 1 else 0)
    simp only [mul_ite, mul_one, mul_zero, RCLike.star_def]i:ℕj:ℕ⊢ (if j = 0 then 0 else if j - 1 = i then ↑√↑j else 0) = (starRingEnd ℂ) (if i + 1 = j then ↑√(↑i + 1) else 0)
    split_ifs with _ _ _ g₃posi:ℕj:ℕ_✝:j = 0_:i + 1 = j⊢ 0 = (starRingEnd ℂ) ↑√(↑i + 1)negi:ℕj:ℕ_✝:j = 0_:¬i + 1 = j⊢ 0 = (starRingEnd ℂ) 0posi:ℕj:ℕ_✝:¬j = 0_:j - 1 = ig₃:i + 1 = j⊢ ↑√↑j = (starRingEnd ℂ) ↑√(↑i + 1)negi:ℕj:ℕ_✝:¬j = 0_:j - 1 = ig₃:¬i + 1 = j⊢ ↑√↑j = (starRingEnd ℂ) 0posi:ℕj:ℕ_✝:¬j = 0_:¬j - 1 = ih✝:i + 1 = j⊢ 0 = (starRingEnd ℂ) ↑√(↑i + 1)negi:ℕj:ℕ_✝:¬j = 0_:¬j - 1 = ih✝:¬i + 1 = j⊢ 0 = (starRingEnd ℂ) 0
    all_goals try omegaAll goals completed! 🐙
    all_goals try exact Eq.symm ((fun {z} ↦ Complex.conj_eq_iff_re.mpr) rfl)All goals completed! 🐙
    rw [← g₃posi:ℕj:ℕ_✝:¬j = 0_:j - 1 = ig₃:i + 1 = j⊢ ↑√↑(i + 1) = (starRingEnd ℂ) ↑√(↑i + 1)posi:ℕj:ℕ_✝:¬j = 0_:j - 1 = ig₃:i + 1 = j⊢ ↑√↑(i + 1) = (starRingEnd ℂ) ↑√(↑i + 1)]posi:ℕj:ℕ_✝:¬j = 0_:j - 1 = ig₃:i + 1 = j⊢ ↑√↑(i + 1) = (starRingEnd ℂ) ↑√(↑i + 1);simpAll goals completed! 🐙

Verify that a |n + 1⟩ = √(n + 1) |n ⟩


lemma verify_a (n : ℕ) :
    a (ε (n + 1) 1) =
       ε n (√(n + 1))  := byn:ℕ⊢ a (ε (n + 1) 1) = ε n ↑√(↑n + 1)
  unfold a εn:ℕ⊢ (fun n_1 => ↑√(↑n_1 + 1) * if n_1 + 1 = n + 1 then 1 else 0) = fun i => if i = n then ↑√(↑n + 1) else 0
  ext in:ℕi:ℕ⊢ (↑√(↑i + 1) * if i + 1 = n + 1 then 1 else 0) = if i = n then ↑√(↑n + 1) else 0
  simp only [Nat.add_right_cancel_iff, mul_ite, mul_one, mul_zero]n:ℕi:ℕ⊢ (if i = n then ↑√(↑i + 1) else 0) = if i = n then ↑√(↑n + 1) else 0
  split_ifs with g₀posn:ℕi:ℕg₀:i = n⊢ ↑√(↑i + 1) = ↑√(↑n + 1)negn:ℕi:ℕg₀:¬i = n⊢ 0 = 0
  ·posn:ℕi:ℕg₀:i = n⊢ ↑√(↑i + 1) = ↑√(↑n + 1) rw [g₀posn:ℕi:ℕg₀:i = n⊢ ↑√(↑n + 1) = ↑√(↑n + 1)All goals completed! 🐙]All goals completed! 🐙
  ·negn:ℕi:ℕg₀:¬i = n⊢ 0 = 0 rflAll goals completed! 🐙

Verify that a† ∣n⟩ = √(n+1) ∣n+1⟩.


lemma verify_a_dag (n : ℕ) :
    a_dag (ε n 1) = ε (n + 1) (√(n + 1))  := byn:ℕ⊢ a_dag (ε n 1) = ε (n + 1) ↑√(↑n + 1)
  unfold a_dag εn:ℕ⊢ (fun n_1 => if n_1 = 0 then 0 else ↑√↑n_1 * if n_1 - 1 = n then 1 else 0) = fun i => if i = n + 1 then ↑√(↑n + 1) else 0
  ext in:ℕi:ℕ⊢ (if i = 0 then 0 else ↑√↑i * if i - 1 = n then 1 else 0) = if i = n + 1 then ↑√(↑n + 1) else 0
  split_ifs with _ _ _ hposn:ℕi:ℕ_✝:i = 0_:i = n + 1⊢ 0 = ↑√(↑n + 1)negn:ℕi:ℕ_✝:i = 0_:¬i = n + 1⊢ 0 = 0posn:ℕi:ℕ_✝:¬i = 0_:i - 1 = nh:i = n + 1⊢ ↑√↑i * 1 = ↑√(↑n + 1)negn:ℕi:ℕ_✝:¬i = 0_:i - 1 = nh:¬i = n + 1⊢ ↑√↑i * 1 = 0posn:ℕi:ℕ_✝:¬i = 0_:¬i - 1 = nh✝:i = n + 1⊢ ↑√↑i * 0 = ↑√(↑n + 1)negn:ℕi:ℕ_✝:¬i = 0_:¬i - 1 = nh✝:¬i = n + 1⊢ ↑√↑i * 0 = 0
  all_goals try omegaAll goals completed! 🐙
  ·negn:ℕi:ℕ_✝:i = 0_:¬i = n + 1⊢ 0 = 0 rflAll goals completed! 🐙
  ·posn:ℕi:ℕ_✝:¬i = 0_:i - 1 = nh:i = n + 1⊢ ↑√↑i * 1 = ↑√(↑n + 1) rw [hposn:ℕi:ℕ_✝:¬i = 0_:i - 1 = nh:i = n + 1⊢ ↑√↑(n + 1) * 1 = ↑√(↑n + 1)posn:ℕi:ℕ_✝:¬i = 0_:i - 1 = nh:i = n + 1⊢ ↑√↑(n + 1) * 1 = ↑√(↑n + 1)]posn:ℕi:ℕ_✝:¬i = 0_:i - 1 = nh:i = n + 1⊢ ↑√↑(n + 1) * 1 = ↑√(↑n + 1); simpAll goals completed! 🐙
  ·negn:ℕi:ℕ_✝:¬i = 0_:¬i - 1 = nh✝:¬i = n + 1⊢ ↑√↑i * 0 = 0 simpAll goals completed! 🐙

              

lemma verify_a_dag_a (n : ℕ) (x : ℕ → ℂ) :
    a_dag (a x) n = n * x n  := byn:ℕx:ℕ → ℂ⊢ a_dag (a x) n = ↑n * x n
  unfold a_dag an:ℕx:ℕ → ℂ⊢ (if n = 0 then 0 else ↑√↑n * (↑√(↑(n - 1) + 1) * x (n - 1 + 1))) = ↑n * x n
  split_ifs with gposn:ℕx:ℕ → ℂg:n = 0⊢ 0 = ↑n * x nnegn:ℕx:ℕ → ℂg:¬n = 0⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x (n - 1 + 1)) = ↑n * x n
  ·posn:ℕx:ℕ → ℂg:n = 0⊢ 0 = ↑n * x n rw [gposn:ℕx:ℕ → ℂg:n = 0⊢ 0 = ↑0 * x 0posn:ℕx:ℕ → ℂg:n = 0⊢ 0 = ↑0 * x 0]posn:ℕx:ℕ → ℂg:n = 0⊢ 0 = ↑0 * x 0;simpAll goals completed! 🐙
  ·negn:ℕx:ℕ → ℂg:¬n = 0⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x (n - 1 + 1)) = ↑n * x n have h : n - 1 + 1 = n := byn:ℕx:ℕ → ℂ⊢ a_dag (a x) n = ↑n * x nnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x (n - 1 + 1)) = ↑n * x n omeganegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x (n - 1 + 1)) = ↑n * x nnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x (n - 1 + 1)) = ↑n * x n
    repeat rw [hnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x n) = ↑n * x nnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x n) = ↑n * x n]negn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√(↑(n - 1) + 1) * x n) = ↑n * x n
    norm_castnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√↑(n - 1 + 1) * x n) = ↑n * x n
    rw [hnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√↑n * x n) = ↑n * x nnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√↑n * x n) = ↑n * x n]negn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * (↑√↑n * x n) = ↑n * x n
    rw [← mul_assocnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * ↑√↑n * x n = ↑n * x nnegn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * ↑√↑n * x n = ↑n * x n]negn:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * ↑√↑n * x n = ↑n * x n
    congrneg.e_an:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ ↑√↑n * ↑√↑n = ↑n
    norm_castneg.e_an:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ √↑n * √↑n = ↑n
    refine Real.mul_self_sqrt ?_neg.e_an:ℕx:ℕ → ℂg:¬n = 0h:n - 1 + 1 = n⊢ 0 ≤ ↑n
    simpAll goals completed! 🐙

lemma verify_a_a_dag (n : ℕ) (x : ℕ → ℂ) :
    a (a_dag x) n = (n + 1) * x n  := byn:ℕx:ℕ → ℂ⊢ a (a_dag x) n = (↑n + 1) * x n
  unfold a_dag an:ℕx:ℕ → ℂ⊢ ↑√(↑n + 1) * (fun n => if n = 0 then 0 else ↑√↑n * x (n - 1)) (n + 1) = (↑n + 1) * x n
  simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, Nat.cast_add, Nat.cast_one,
    add_tsub_cancel_right]n:ℕx:ℕ → ℂ⊢ ↑√(↑n + 1) * (↑√(↑n + 1) * x n) = (↑n + 1) * x n
  rw [← mul_assocn:ℕx:ℕ → ℂ⊢ ↑√(↑n + 1) * ↑√(↑n + 1) * x n = (↑n + 1) * x nn:ℕx:ℕ → ℂ⊢ ↑√(↑n + 1) * ↑√(↑n + 1) * x n = (↑n + 1) * x n]n:ℕx:ℕ → ℂ⊢ ↑√(↑n + 1) * ↑√(↑n + 1) * x n = (↑n + 1) * x n
  congre_an:ℕx:ℕ → ℂ⊢ ↑√(↑n + 1) * ↑√(↑n + 1) = ↑n + 1
  norm_caste_an:ℕx:ℕ → ℂ⊢ √↑(n + 1) * √↑(n + 1) = ↑(n + 1)
  refine Real.mul_self_sqrt ?_e_an:ℕx:ℕ → ℂ⊢ 0 ≤ ↑(n + 1)
  norm_caste_an:ℕx:ℕ → ℂ⊢ 0 ≤ n + 1
  omegaAll goals completed! 🐙

lemma commutation_relation :
    a ∘ a_dag - a_dag ∘ a = id := by⊢ a ∘ a_dag - a_dag ∘ a = id
  unfold a a_dag⊢ (((fun x n => ↑√(↑n + 1) * x (n + 1)) ∘ fun x n => if n = 0 then 0 else ↑√↑n * x (n - 1)) -
    (fun x n => if n = 0 then 0 else ↑√↑n * x (n - 1)) ∘ fun x n => ↑√(↑n + 1) * x (n + 1)) =
  id
  ext x ix:ℕ → ℂi:ℕ⊢ (((fun x n => ↑√(↑n + 1) * x (n + 1)) ∘ fun x n => if n = 0 then 0 else ↑√↑n * x (n - 1)) -
      (fun x n => if n = 0 then 0 else ↑√↑n * x (n - 1)) ∘ fun x n => ↑√(↑n + 1) * x (n + 1))
    x i =
  id x i
  simp only [Pi.sub_apply, Function.comp_apply, Nat.add_eq_zero_iff, one_ne_zero, and_false,
    ↓reduceIte, Nat.cast_add, Nat.cast_one, add_tsub_cancel_right, id_eq]x:ℕ → ℂi:ℕ⊢ (↑√(↑i + 1) * (↑√(↑i + 1) * x i) - if i = 0 then 0 else ↑√↑i * (↑√(↑(i - 1) + 1) * x (i - 1 + 1))) = x i
  split_ifs with g₀posx:ℕ → ℂi:ℕg₀:i = 0⊢ ↑√(↑i + 1) * (↑√(↑i + 1) * x i) - 0 = x inegx:ℕ → ℂi:ℕg₀:¬i = 0⊢ ↑√(↑i + 1) * (↑√(↑i + 1) * x i) - ↑√↑i * (↑√(↑(i - 1) + 1) * x (i - 1 + 1)) = x i
  ·posx:ℕ → ℂi:ℕg₀:i = 0⊢ ↑√(↑i + 1) * (↑√(↑i + 1) * x i) - 0 = x i rw [g₀posx:ℕ → ℂi:ℕg₀:i = 0⊢ ↑√(↑0 + 1) * (↑√(↑0 + 1) * x 0) - 0 = x 0posx:ℕ → ℂi:ℕg₀:i = 0⊢ ↑√(↑0 + 1) * (↑√(↑0 + 1) * x 0) - 0 = x 0]posx:ℕ → ℂi:ℕg₀:i = 0⊢ ↑√(↑0 + 1) * (↑√(↑0 + 1) * x 0) - 0 = x 0;simpAll goals completed! 🐙
  ·negx:ℕ → ℂi:ℕg₀:¬i = 0⊢ ↑√(↑i + 1) * (↑√(↑i + 1) * x i) - ↑√↑i * (↑√(↑(i - 1) + 1) * x (i - 1 + 1)) = x i norm_castnegx:ℕ → ℂi:ℕg₀:¬i = 0⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑(i - 1 + 1) * x (i - 1 + 1)) = x i
    have : i - 1 + 1 = i := by⊢ a ∘ a_dag - a_dag ∘ a = idnegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑(i - 1 + 1) * x (i - 1 + 1)) = x i omeganegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑(i - 1 + 1) * x (i - 1 + 1)) = x inegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑(i - 1 + 1) * x (i - 1 + 1)) = x i
    rw [thisnegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑i * x i) = x inegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑i * x i) = x i]negx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * (↑√↑(i + 1) * x i) - ↑√↑i * (↑√↑i * x i) = x i
    repeat rw [← mul_assocnegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * (↑√↑i * x i) = x inegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * ↑√↑i * x i = x i]negx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * (↑√↑i * x i) = x inegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * ↑√↑i * x i = x inegx:ℕ → ℂi:ℕg₀:¬i = 0this:i - 1 + 1 = i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * ↑√↑i * x i = x i
    have : (i + 1) * x i - i * x i = x i := by⊢ a ∘ a_dag - a_dag ∘ a = idnegx:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * ↑√↑i * x i = x i
        ring_nfnegx:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * ↑√↑i * x i = x inegx:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * x i - ↑√↑i * ↑√↑i * x i = x i
    rw [← thisnegx:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * ((↑i + 1) * x i - ↑i * x i) - ↑√↑i * ↑√↑i * ((↑i + 1) * x i - ↑i * x i) =
  (↑i + 1) * x i - ↑i * x inegx:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * ((↑i + 1) * x i - ↑i * x i) - ↑√↑i * ↑√↑i * ((↑i + 1) * x i - ↑i * x i) =
  (↑i + 1) * x i - ↑i * x i]negx:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) * ((↑i + 1) * x i - ↑i * x i) - ↑√↑i * ↑√↑i * ((↑i + 1) * x i - ↑i * x i) =
  (↑i + 1) * x i - ↑i * x i
    congrneg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) = ↑i + 1neg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑i * ↑√↑i = ↑i
    ·neg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑(i + 1) * ↑√↑(i + 1) = ↑i + 1 norm_castneg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ √↑(i + 1) * √↑(i + 1) = ↑(i + 1)
      refine Real.mul_self_sqrt ?_neg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ 0 ≤ ↑(i + 1)
      linarithAll goals completed! 🐙
    ·neg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ ↑√↑i * ↑√↑i = ↑i norm_castneg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ √↑i * √↑i = ↑i
      refine Real.mul_self_sqrt ?_neg.e_a.e_ax:ℕ → ℂi:ℕg₀:¬i = 0this✝:i - 1 + 1 = ithis:(↑i + 1) * x i - ↑i * x i = x i⊢ 0 ≤ ↑i
      simpAll goals completed! 🐙def coherentState (α : ℂ) : ℕ → ℂ :=
    fun n : ℕ => Real.exp (-‖α‖^2 / 2) * α ^ n / √(n.factorial)def probabilityOf (n : ℕ) (α : ℂ) : NNReal :=
    ⟨‖coherentState α n‖^2, byn:ℕα:ℂ⊢ 0 ≤ ‖coherentState α n‖ ^ 2 simpAll goals completed! 🐙⟩

Coherent state has a Poisson distribution.


lemma probabilityOf_eq_poisson_C (n : ℕ) (α : ℂ) :
    let Λ := ⟨‖α‖ ^ 2, sq_nonneg ‖α‖⟩
    probabilityOf n α =
    ProbabilityTheory.poissonMeasure Λ {n} := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}
  unfold probabilityOf ProbabilityTheory.poissonMeasure coherentStaten:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑⟨‖↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ n / ↑√↑n.factorial‖ ^ 2, ⋯⟩ =
  (MeasureTheory.Measure.sum fun n =>
      ENNReal.ofReal (Real.exp (-↑Λ) * ↑Λ ^ n / ↑n.factorial) • MeasureTheory.Measure.dirac n)
    {n}
  simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow,
    Complex.ofReal_ofNat, Complex.norm_div, Complex.norm_mul, norm_pow, Complex.norm_real,
    Real.norm_eq_abs, MeasurableSpace.measurableSet_top, MeasureTheory.Measure.sum_apply,
    MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.dirac_apply', Set.indicator_singleton,
    Pi.one_apply, smul_eq_mul]n:ℕα:ℂ⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / |√↑n.factorial|) ^ 2, ⋯⟩ =
  ∑' (i : ℕ), ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ i / ↑i.factorial) * Pi.single n 1 i
  have : |√(n.factorial : ℝ)| = √(n.factorial : ℝ) := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}n:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / |√↑n.factorial|) ^ 2, ⋯⟩ =
  ∑' (i : ℕ), ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ i / ↑i.factorial) * Pi.single n 1 i simpn:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / |√↑n.factorial|) ^ 2, ⋯⟩ =
  ∑' (i : ℕ), ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ i / ↑i.factorial) * Pi.single n 1 in:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / |√↑n.factorial|) ^ 2, ⋯⟩ =
  ∑' (i : ℕ), ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ i / ↑i.factorial) * Pi.single n 1 i
  simp_rw [n:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / |√↑n.factorial|) ^ 2, ⋯⟩ =
  ∑' (i : ℕ), ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ i / ↑i.factorial) * Pi.single n 1 ithisn:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / √↑n.factorial) ^ 2, ⋯⟩ =
  ∑' (i : ℕ), ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ i / ↑i.factorial) * Pi.single n 1 i]
  simp only [Pi.single, Function.update, eq_rec_constant, Pi.zero_apply, dite_eq_ite, mul_ite,
    mul_one, mul_zero, tsum_ite_eq]n:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / √↑n.factorial) ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)
  simp_rw [n:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ n / √↑n.factorial) ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)← mul_divn:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨(‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * (‖α‖ ^ n / √↑n.factorial)) ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * (↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial))]
  field_simpn:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / √↑n.factorial ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)
  have : √↑n.factorial ^ 2 = (n.factorial : ℝ) := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}n:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / √↑n.factorial ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)
    refine Real.sq_sqrt ?_n:ℕα:ℂthis:|√↑n.factorial| = √↑n.factorial⊢ 0 ≤ ↑n.factorialn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / √↑n.factorial ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)
    simpn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / √↑n.factorial ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)n:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / √↑n.factorial ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)
  simp_rw [n:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / √↑n.factorial ^ 2, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)thisn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ↑⟨‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial, ⋯⟩ =
  ENNReal.ofReal (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial)]
  congrn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  max (Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial) 0
  rw [max_eq_leftn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorialn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorialn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorialn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial]n:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorialn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial
  ·n:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial have (a b : ℝ) (h : a = b) : a / n.factorial = b / n.factorial := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}n:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial
        rw [hn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factoriala:ℝb:ℝh:a = b⊢ b / ↑n.factorial = b / ↑n.factorialn:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial]n:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorialn:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 / ↑n.factorial =
  Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial
    apply thisn:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorial⊢ ‖Complex.exp (-(↑‖α‖ ^ 2 / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n
    norm_castn:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorial⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)
    have (a b c d : ℝ) (hab : a = b) (hcd : c = d) :
        a * c = b * d := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}n:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n) rw [hab,n:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factoriala:ℝb:ℝc:ℝd:ℝhab:a = bhcd:c = d⊢ b * c = b * dn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)hcdn:ℕα:ℂthis✝¹:|√↑n.factorial| = √↑n.factorialthis✝:√↑n.factorial ^ 2 = ↑n.factorialthis:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factoriala:ℝb:ℝc:ℝd:ℝhab:a = bhcd:c = d⊢ b * d = b * dn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)]n:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)n:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 * (‖α‖ ^ n) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)
    apply thishabn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)hcdn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ (‖α‖ ^ n) ^ 2 = ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)
    ·habn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) norm_casthabn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      have : ‖α‖^2 ≥ 0 := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}habn:ℕα:ℂthis✝³:|√↑n.factorial| = √↑n.factorialthis✝²:√↑n.factorial ^ 2 = ↑n.factorialthis✝¹:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis:‖α‖ ^ 2 ≥ 0⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) simphabn:ℕα:ℂthis✝³:|√↑n.factorial| = √↑n.factorialthis✝²:√↑n.factorial ^ 2 = ↑n.factorialthis✝¹:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis:‖α‖ ^ 2 ≥ 0⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)habn:ℕα:ℂthis✝³:|√↑n.factorial| = √↑n.factorialthis✝²:√↑n.factorial ^ 2 = ↑n.factorialthis✝¹:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis:‖α‖ ^ 2 ≥ 0⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      have (r : ℝ) :
        Complex.exp (-(r/2)) = Real.exp (-(r/2)) := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}habn:ℕα:ℂthis✝⁴:|√↑n.factorial| = √↑n.factorialthis✝³:√↑n.factorial ^ 2 = ↑n.factorialthis✝²:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝¹:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝:‖α‖ ^ 2 ≥ 0this:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) simphabn:ℕα:ℂthis✝⁴:|√↑n.factorial| = √↑n.factorialthis✝³:√↑n.factorial ^ 2 = ↑n.factorialthis✝²:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝¹:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝:‖α‖ ^ 2 ≥ 0this:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)habn:ℕα:ℂthis✝⁴:|√↑n.factorial| = √↑n.factorialthis✝³:√↑n.factorial ^ 2 = ↑n.factorialthis✝²:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝¹:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝:‖α‖ ^ 2 ≥ 0this:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))⊢ ‖Complex.exp (-(↑(‖α‖ ^ 2) / 2))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      rw [thishabn:ℕα:ℂthis✝⁴:|√↑n.factorial| = √↑n.factorialthis✝³:√↑n.factorial ^ 2 = ↑n.factorialthis✝²:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝¹:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝:‖α‖ ^ 2 ≥ 0this:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))⊢ ‖↑(Real.exp (-(‖α‖ ^ 2 / 2)))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)habn:ℕα:ℂthis✝⁴:|√↑n.factorial| = √↑n.factorialthis✝³:√↑n.factorial ^ 2 = ↑n.factorialthis✝²:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝¹:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝:‖α‖ ^ 2 ≥ 0this:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))⊢ ‖↑(Real.exp (-(‖α‖ ^ 2 / 2)))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)]habn:ℕα:ℂthis✝⁴:|√↑n.factorial| = √↑n.factorialthis✝³:√↑n.factorial ^ 2 = ↑n.factorialthis✝²:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝¹:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝:‖α‖ ^ 2 ≥ 0this:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))⊢ ‖↑(Real.exp (-(‖α‖ ^ 2 / 2)))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      have (r : ℝ) : ‖Complex.ofReal (Real.exp r)‖ = Real.exp r := byn:ℕα:ℂ⊢ let Λ := ⟨‖α‖ ^ 2, ⋯⟩;
↑(probabilityOf n α) = (ProbabilityTheory.poissonMeasure Λ) {n}habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp r⊢ ‖↑(Real.exp (-(‖α‖ ^ 2 / 2)))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) simphabn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp r⊢ ‖↑(Real.exp (-(‖α‖ ^ 2 / 2)))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp r⊢ ‖↑(Real.exp (-(‖α‖ ^ 2 / 2)))‖ ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      rw [thishabn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp r⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp r⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)]habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp r⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      have h₀ (r : ℝ) : (Real.exp r) ^ (2:ℝ) = Real.exp (r * 2) :=
        Eq.symm (Real.exp_mul r 2)habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      have h₁ (r : ℝ) : (Real.exp r) ^ (2:ℝ) = Real.exp r ^ 2 :=
        Real.rpow_two (Real.exp r)habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)h₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      simp_rw [habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)h₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)h₁habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2h₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ Real.exp (-(‖α‖ ^ 2 / 2)) ^ 2 = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)] at h₀
      rw [h₀habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2h₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ Real.exp (-(‖α‖ ^ 2 / 2) * 2) = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2h₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ Real.exp (-(‖α‖ ^ 2 / 2) * 2) = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)]habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2h₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ Real.exp (-(‖α‖ ^ 2 / 2) * 2) = Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)
      congrhabn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2h₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ -(‖α‖ ^ 2 / 2) * 2 = -↑⟨‖α‖ ^ 2, ⋯⟩
      simp only [neg_mul, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
        IsUnit.div_mul_cancel, neg_inj]habn:ℕα:ℂthis✝⁵:|√↑n.factorial| = √↑n.factorialthis✝⁴:√↑n.factorial ^ 2 = ↑n.factorialthis✝³:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis✝²:∀ (a b c d : ℝ), a = b → c = d → a * c = b * dthis✝¹:‖α‖ ^ 2 ≥ 0this✝:∀ (r : ℝ), Complex.exp (-(↑r / 2)) = ↑(Real.exp (-(r / 2)))this:∀ (r : ℝ), ‖↑(Real.exp r)‖ = Real.exp rh₁:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp r ^ 2h₀:∀ (r : ℝ), Real.exp r ^ 2 = Real.exp (r * 2)⊢ ‖α‖ ^ 2 = ↑⟨‖α‖ ^ 2, ⋯⟩
      norm_castAll goals completed! 🐙
    ·hcdn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ (‖α‖ ^ n) ^ 2 = ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n) rw [pow_right_commhcdn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ (‖α‖ ^ 2) ^ n = ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)hcdn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ (‖α‖ ^ 2) ^ n = ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)]hcdn:ℕα:ℂthis✝²:|√↑n.factorial| = √↑n.factorialthis✝¹:√↑n.factorial ^ 2 = ↑n.factorialthis✝:∀ (a b : ℝ), a = b → a / ↑n.factorial = b / ↑n.factorialthis:∀ (a b c d : ℝ), a = b → c = d → a * c = b * d⊢ (‖α‖ ^ 2) ^ n = ↑(⟨‖α‖ ^ 2, ⋯⟩ ^ n)
      congrAll goals completed! 🐙
  ·n:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n / ↑n.factorial apply div_nonneghan:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ nhbn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ ↑n.factorial
    ·han:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) * ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n apply mul_nonnegha.han:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩)hbn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n
      ·ha.han:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ Real.exp (-↑⟨‖α‖ ^ 2, ⋯⟩) apply Real.exp_nonnegAll goals completed! 🐙
      ·hbn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ ↑⟨‖α‖ ^ 2, ⋯⟩ ^ n simpAll goals completed! 🐙
    ·hbn:ℕα:ℂthis✝:|√↑n.factorial| = √↑n.factorialthis:√↑n.factorial ^ 2 = ↑n.factorial⊢ 0 ≤ ↑n.factorial simpAll goals completed! 🐙

The only eigenvectors of a are the coherent states.


lemma coherentState_only_eigenvector (α : ℂ) (v : ℕ → ℂ) :
    a v = α • v ↔
    v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α := byα:ℂv:ℕ → ℂ⊢ a v = α • v ↔ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α
  constructormpα:ℂv:ℕ → ℂ⊢ a v = α • v → v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αmprα:ℂv:ℕ → ℂ⊢ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α → _root_.a v = α • v
  intro hvmpα:ℂv:ℕ → ℂhv:a v = α • v⊢ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αmprα:ℂv:ℕ → ℂ⊢ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α → _root_.a v = α • v
  ext nmpα:ℂv:ℕ → ℂhv:a v = α • vn:ℕ⊢ v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nmprα:ℂv:ℕ → ℂ⊢ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α → _root_.a v = α • v
  induction n with
  | zero =>mp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) 0
    unfold coherentStatemp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ n / ↑√↑n.factorial) 0
    simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow,
      Complex.ofReal_ofNat, Pi.smul_apply, pow_zero, mul_one, Nat.factorial_zero, Nat.cast_one,
      Real.sqrt_one, Complex.ofReal_one, div_one, smul_eq_mul]mp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = Complex.exp (↑‖α‖ ^ 2 / 2) * v 0 * Complex.exp (-↑‖α‖ ^ 2 / 2)
    field_simpmp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * Complex.exp (↑‖α‖ ^ 2 / 2) * Complex.exp (-(↑‖α‖ ^ 2 / 2))
    rw [mul_assocmp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * (Complex.exp (↑‖α‖ ^ 2 / 2) * Complex.exp (-(↑‖α‖ ^ 2 / 2)))mp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * (Complex.exp (↑‖α‖ ^ 2 / 2) * Complex.exp (-(↑‖α‖ ^ 2 / 2)))]mp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * (Complex.exp (↑‖α‖ ^ 2 / 2) * Complex.exp (-(↑‖α‖ ^ 2 / 2)))
    rw [← Complex.exp_addmp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * Complex.exp (↑‖α‖ ^ 2 / 2 + -(↑‖α‖ ^ 2 / 2))mp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * Complex.exp (↑‖α‖ ^ 2 / 2 + -(↑‖α‖ ^ 2 / 2))]mp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * Complex.exp (↑‖α‖ ^ 2 / 2 + -(↑‖α‖ ^ 2 / 2))
    field_simpmp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * Complex.exp (↑‖α‖ ^ 2 * (1 + -1) / 2)
    ring_nfmp.zeroα:ℂv:ℕ → ℂhv:a v = α • v⊢ v 0 = v 0 * Complex.exp 0
    simpAll goals completed! 🐙
  | succ n hn =>mp.succα:ℂv:ℕ → ℂhv:a v = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
    unfold a at hvmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
    have h₀ := congrFun hv nmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = (α • v) n⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
    simp only [Pi.smul_apply, smul_eq_mul] at h₀mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v n⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
    have : v (n + 1) = α * v n / √(n + 1) := byα:ℂv:ℕ → ℂ⊢ a v = α • v ↔ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
      field_simpα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v n⊢ v (n + 1) * ↑√(↑n + 1) = α * v nmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
      rw [← h₀,α:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v n⊢ v (n + 1) * ↑√(↑n + 1) = ↑√(↑n + 1) * v (n + 1)mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) mul_commα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v n⊢ ↑√(↑n + 1) * v (n + 1) = ↑√(↑n + 1) * v (n + 1)mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)]mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ v (n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
    rw [this,mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * v n / ↑√(↑n + 1) = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n / ↑√(↑n + 1) =
  ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) hnmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n / ↑√(↑n + 1) =
  ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n / ↑√(↑n + 1) =
  ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)]mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n / ↑√(↑n + 1) =
  ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)
    unfold coherentStatemp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ n / ↑√↑n.factorial) n / ↑√(↑n + 1) =
  ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ n / ↑√↑n.factorial) (n + 1)
    field_simpmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-(‖α‖ ^ 2 / 2))) * α ^ n / ↑√↑n.factorial) n =
  ↑√(↑n + 1) *
    ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-(‖α‖ ^ 2 / 2))) * α ^ n / ↑√↑n.factorial) (n + 1)
    ring_nfmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α *
    ((Complex.exp (↑‖α‖ ^ 2 * (1 / 2)) * v 0) • fun n => α ^ n * ↑(Real.exp (‖α‖ ^ 2 * (-1 / 2))) * (↑√↑n.factorial)⁻¹)
      n =
  ↑√(1 + ↑n) *
    ((Complex.exp (↑‖α‖ ^ 2 * (1 / 2)) * v 0) • fun n => α ^ n * ↑(Real.exp (‖α‖ ^ 2 * (-1 / 2))) * (↑√↑n.factorial)⁻¹)
      (1 + n)
    simp only [one_div, Complex.ofReal_exp, Complex.ofReal_mul, Complex.ofReal_pow,
      Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_one, Complex.ofReal_ofNat,
      Pi.smul_apply, smul_eq_mul]mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 * (α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑n.factorial)⁻¹)) =
  ↑√(1 + ↑n) *
    (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 * (α ^ (1 + n) * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑(1 + n).factorial)⁻¹))
    rw [pow_addmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 * (α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑n.factorial)⁻¹)) =
  ↑√(1 + ↑n) *
    (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 *
      (α ^ 1 * α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑(1 + n).factorial)⁻¹))mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 * (α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑n.factorial)⁻¹)) =
  ↑√(1 + ↑n) *
    (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 *
      (α ^ 1 * α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑(1 + n).factorial)⁻¹))]mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 * (α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑n.factorial)⁻¹)) =
  ↑√(1 + ↑n) *
    (Complex.exp (↑‖α‖ ^ 2 * 2⁻¹) * v 0 *
      (α ^ 1 * α ^ n * Complex.exp (↑‖α‖ ^ 2 * (-1 / 2)) * (↑√↑(1 + n).factorial)⁻¹))
    field_simpmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * v 0 * α ^ n / ↑√↑n.factorial = α * v 0 * α ^ n * ↑√(1 + ↑n) / ↑√↑(1 + n).factorial
    ring_nfmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * α ^ n * v 0 * (↑√↑n.factorial)⁻¹ = α * α ^ n * v 0 * ↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹
    repeat rw [mul_assocmp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * α ^ n * (v 0 * (↑√↑n.factorial)⁻¹) = α * α ^ n * v 0 * ↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (α ^ n * (v 0 * (↑√↑n.factorial)⁻¹)) = α * (α ^ n * (v 0 * (↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹)))]mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (α ^ n * (v 0 * (↑√↑n.factorial)⁻¹)) = α * α ^ n * (v 0 * (↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹))mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (α ^ n * (v 0 * (↑√↑n.factorial)⁻¹)) = α * (α ^ n * (v 0 * (↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹)))mp.succα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ α * (α ^ n * (v 0 * (↑√↑n.factorial)⁻¹)) = α * (α ^ n * (v 0 * (↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹)))
    congrmp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹
    field_simpmp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ 1 / ↑√↑n.factorial = ↑√(1 + ↑n) / ↑√↑(1 + n).factorial
    ring_nfmp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(1 + ↑n) * (↑√↑(1 + n).factorial)⁻¹
    rw [add_commmp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑(1 + n).factorial)⁻¹mp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑(1 + n).factorial)⁻¹]mp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑(1 + n).factorial)⁻¹
    nth_rw 2 [add_commmp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑(n + 1).factorial)⁻¹]mp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis:v (n + 1) = α * v n / ↑√(↑n + 1)⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑(n + 1).factorial)⁻¹
    have : (n+1).factorial = (n+1) * n.factorial := rflmp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis✝:v (n + 1) = α * v n / ↑√(↑n + 1)this:(n + 1).factorial = (n + 1) * n.factorial⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑(n + 1).factorial)⁻¹
    rw [thismp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis✝:v (n + 1) = α * v n / ↑√(↑n + 1)this:(n + 1).factorial = (n + 1) * n.factorial⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑((n + 1) * n.factorial))⁻¹mp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis✝:v (n + 1) = α * v n / ↑√(↑n + 1)this:(n + 1).factorial = (n + 1) * n.factorial⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑((n + 1) * n.factorial))⁻¹]mp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis✝:v (n + 1) = α * v n / ↑√(↑n + 1)this:(n + 1).factorial = (n + 1) * n.factorial⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * (↑√↑((n + 1) * n.factorial))⁻¹
    norm_nummp.succ.e_a.e_a.e_aα:ℂv:ℕ → ℂhv:(fun n => ↑√(↑n + 1) * v (n + 1)) = α • vn:ℕhn:v n = ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nh₀:↑√(↑n + 1) * v (n + 1) = α * v nthis✝:v (n + 1) = α * v n / ↑√(↑n + 1)this:(n + 1).factorial = (n + 1) * n.factorial⊢ (↑√↑n.factorial)⁻¹ = ↑√(↑n + 1) * ((↑√↑n.factorial)⁻¹ * (↑√(↑n + 1))⁻¹)
    field_simpAll goals completed! 🐙
  intro hmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α⊢ a v = α • v
  rw [hmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α⊢ a ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) = α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α⊢ a ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) = α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α]mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α⊢ a ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) = α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α
  unfold amprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α⊢ (fun n => ↑√(↑n + 1) * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1)) =
  α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α
  ext nmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕ⊢ ↑√(↑n + 1) * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) =
  (α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n
  have : (Complex.exp (↑‖α‖ ^ 2 / 2)) ≠ 0 := byα:ℂv:ℕ → ℂ⊢ a v = α • v ↔ v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) =
  (α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n simpmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) =
  (α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) nmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) =
  (α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n
  field_simpmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) (n + 1) =
  (α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState α) n
  unfold coherentStatemprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) *
    ((Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ n / ↑√↑n.factorial) (n + 1) =
  (α • (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • fun n => ↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ n / ↑√↑n.factorial) n
  simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow,
    Complex.ofReal_ofNat, Pi.smul_apply, smul_eq_mul]mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0 * (Complex.exp (-↑‖α‖ ^ 2 / 2) * α ^ (n + 1) / ↑√↑(n + 1).factorial)) =
  α * (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0 * (Complex.exp (-↑‖α‖ ^ 2 / 2) * α ^ n / ↑√↑n.factorial))
  field_simpmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * v 0 * α ^ (n + 1) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorial
  ring_nfmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(1 + ↑n) * v 0 * α * α ^ n * (↑√↑(1 + n).factorial)⁻¹ = v 0 * α * α ^ n * (↑√↑n.factorial)⁻¹
  field_simpmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(1 + ↑n) * v 0 * α * α ^ n / ↑√↑(1 + n).factorial = v 0 * α * α ^ n / ↑√↑n.factorial
  rw [mul_assoc,mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(1 + ↑n) * v 0 * (α * α ^ n) / ↑√↑(1 + n).factorial = v 0 * α * α ^ n / ↑√↑n.factorialmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorial add_comm 1 n,mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(1 + ↑n) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorialmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorial add_comm 1 (n:ℝ)mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorialmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorial]mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorial
  have : (n+1).factorial = (n+1) * n.factorial := rflmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis✝:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0this:(n + 1).factorial = (n + 1) * n.factorial⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑(n + 1).factorial = v 0 * α * α ^ n / ↑√↑n.factorial
  rw [thismprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis✝:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0this:(n + 1).factorial = (n + 1) * n.factorial⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑((n + 1) * n.factorial) = v 0 * α * α ^ n / ↑√↑n.factorialmprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis✝:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0this:(n + 1).factorial = (n + 1) * n.factorial⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑((n + 1) * n.factorial) = v 0 * α * α ^ n / ↑√↑n.factorial]mprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis✝:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0this:(n + 1).factorial = (n + 1) * n.factorial⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / ↑√↑((n + 1) * n.factorial) = v 0 * α * α ^ n / ↑√↑n.factorial
  norm_nummprα:ℂv:ℕ → ℂh:v = (Complex.exp (↑‖α‖ ^ 2 / 2) * v 0) • coherentState αn:ℕthis✝:Complex.exp (↑‖α‖ ^ 2 / 2) ≠ 0this:(n + 1).factorial = (n + 1) * n.factorial⊢ ↑√(↑n + 1) * v 0 * (α * α ^ n) / (↑√(↑n + 1) * ↑√↑n.factorial) = v 0 * α * α ^ n / ↑√↑n.factorial
  field_simpAll goals completed! 🐙



lemma eigenvector_coherentState (α : ℂ) :
    a (coherentState α) = α • coherentState α := byα:ℂ⊢ a (coherentState α) = α • coherentState α
  rw [coherentState_only_eigenvector α (coherentState α)α:ℂ⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState αα:ℂ⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α]α:ℂ⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
  have : Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1 := byα:ℂ⊢ a (coherentState α) = α • coherentState αα:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
    unfold coherentStateα:ℂ⊢ Complex.exp (↑‖α‖ ^ 2 / 2) * (↑(Real.exp (-‖α‖ ^ 2 / 2)) * α ^ 0 / ↑√↑(Nat.factorial 0)) = 1α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
    simp only [Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow,
      Complex.ofReal_ofNat, pow_zero, mul_one, Nat.factorial_zero, Nat.cast_one, Real.sqrt_one,
      Complex.ofReal_one, div_one]α:ℂ⊢ Complex.exp (↑‖α‖ ^ 2 / 2) * Complex.exp (-↑‖α‖ ^ 2 / 2) = 1α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
    rw [← Complex.exp_addα:ℂ⊢ Complex.exp (↑‖α‖ ^ 2 / 2 + -↑‖α‖ ^ 2 / 2) = 1α:ℂ⊢ Complex.exp (↑‖α‖ ^ 2 / 2 + -↑‖α‖ ^ 2 / 2) = 1α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α]α:ℂ⊢ Complex.exp (↑‖α‖ ^ 2 / 2 + -↑‖α‖ ^ 2 / 2) = 1α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
    field_simpα:ℂ⊢ Complex.exp (↑‖α‖ ^ 2 * (1 + -1) / 2) = 1α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
    ring_nfα:ℂ⊢ Complex.exp 0 = 1α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
    simpα:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState αα:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = (Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0) • coherentState α
  rw [thisα:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = 1 • coherentState αα:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = 1 • coherentState α]α:ℂthis:Complex.exp (↑‖α‖ ^ 2 / 2) * coherentState α 0 = 1⊢ coherentState α = 1 • coherentState α
  simpAll goals completed! 🐙

None of the coherentState eigenvectors are proportional.

lemma distinct_eigenvectors_a (α β c : ℂ)
    (hc : coherentState α = c • coherentState β) : α = β := byα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState β⊢ α = β
  have h₀ := congrFun hc 0α:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βh₀:coherentState α 0 = (c • coherentState β) 0⊢ α = β
  have h₁ := congrFun hc 1α:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βh₀:coherentState α 0 = (c • coherentState β) 0h₁:coherentState α 1 = (c • coherentState β) 1⊢ α = β
  simp [coherentState] at h₀ h₁α:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βh₀:Complex.exp (-↑‖α‖ ^ 2 / 2) = c * Complex.exp (-↑‖β‖ ^ 2 / 2)h₁:Complex.exp (-↑‖α‖ ^ 2 / 2) * α = c * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)⊢ α = β
  by_cases hc₀ : c = 0posα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βh₀:Complex.exp (-↑‖α‖ ^ 2 / 2) = c * Complex.exp (-↑‖β‖ ^ 2 / 2)h₁:Complex.exp (-↑‖α‖ ^ 2 / 2) * α = c * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)hc₀:c = 0⊢ α = βnegα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βh₀:Complex.exp (-↑‖α‖ ^ 2 / 2) = c * Complex.exp (-↑‖β‖ ^ 2 / 2)h₁:Complex.exp (-↑‖α‖ ^ 2 / 2) * α = c * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)hc₀:¬c = 0⊢ α = β
  ·posα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βh₀:Complex.exp (-↑‖α‖ ^ 2 / 2) = c * Complex.exp (-↑‖β‖ ^ 2 / 2)h₁:Complex.exp (-↑‖α‖ ^ 2 / 2) * α = c * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)hc₀:c = 0⊢ α = β subst cposα:ℂβ:ℂhc:coherentState α = 0 • coherentState βh₀:Complex.exp (-↑‖α‖ ^ 2 / 2) = 0 * Complex.exp (-↑‖β‖ ^ 2 / 2)h₁:Complex.exp (-↑‖α‖ ^ 2 / 2) * α = 0 * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)⊢ α = β
    simp at h₀All goals completed! 🐙
  generalize Complex.exp (-↑‖α‖ ^ 2 / 2) = A at *negα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βhc₀:¬c = 0A:ℂh₀:A = c * Complex.exp (-↑‖β‖ ^ 2 / 2)h₁:A * α = c * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)⊢ α = β
  subst Anegα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βhc₀:¬c = 0h₁:c * Complex.exp (-↑‖β‖ ^ 2 / 2) * α = c * (Complex.exp (-↑‖β‖ ^ 2 / 2) * β)⊢ α = β
  field_simp at h₁negα:ℂβ:ℂc:ℂhc:coherentState α = c • coherentState βhc₀:¬c = 0h₁:α = β⊢ α = β
  exact h₁All goals completed! 🐙

Formal eigenvectors for a_dag (not in ℓ²(ℂ)) (fails at n=0) .


lemma a_dagalmost_eigenvector {α : ℂ} (hα : α ≠ 0) {n : ℕ} (hn : n ≠ 0) :
    a_dag (fun n => √(n.factorial) / α^n) n =
      α • (fun n => √(n.factorial) / α^n) n := byα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0⊢ a_dag (fun n => ↑√↑n.factorial / α ^ n) n = α • (fun n => ↑√↑n.factorial / α ^ n) n
  unfold a_dagα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0⊢ (if n = 0 then 0 else ↑√↑n * (fun n => ↑√↑n.factorial / α ^ n) (n - 1)) = α • (fun n => ↑√↑n.factorial / α ^ n) n
  split_ifs with g₀posα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:n = 0⊢ 0 = α • (fun n => ↑√↑n.factorial / α ^ n) nnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (fun n => ↑√↑n.factorial / α ^ n) (n - 1) = α • (fun n => ↑√↑n.factorial / α ^ n) n
  ·posα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:n = 0⊢ 0 = α • (fun n => ↑√↑n.factorial / α ^ n) n tautoAll goals completed! 🐙
  ·negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (fun n => ↑√↑n.factorial / α ^ n) (n - 1) = α • (fun n => ↑√↑n.factorial / α ^ n) n simp only [smul_eq_mul]negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑n.factorial / α ^ n)
    rw [← Nat.mul_factorial_pred hnnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑(n * (n - 1).factorial) / α ^ n)negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑(n * (n - 1).factorial) / α ^ n)]negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑(n * (n - 1).factorial) / α ^ n)
    norm_numnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑n * ↑√↑(n - 1).factorial / α ^ n)
    have : Complex.ofReal √( (n-1).factorial) ≠ 0 := byα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0⊢ a_dag (fun n => ↑√↑n.factorial / α ^ n) n = α • (fun n => ↑√↑n.factorial / α ^ n) nnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this:↑√↑(n - 1).factorial ≠ 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑n * ↑√↑(n - 1).factorial / α ^ n)
      simp only [ne_eq, Complex.ofReal_eq_zero, Nat.cast_nonneg, Real.sqrt_eq_zero,
        Nat.cast_eq_zero]α:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0⊢ ¬(n - 1).factorial = 0negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this:↑√↑(n - 1).factorial ≠ 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑n * ↑√↑(n - 1).factorial / α ^ n)
      exact Nat.factorial_ne_zero (n - 1)negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this:↑√↑(n - 1).factorial ≠ 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑n * ↑√↑(n - 1).factorial / α ^ n)negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this:↑√↑(n - 1).factorial ≠ 0⊢ ↑√↑n * (↑√↑(n - 1).factorial / α ^ (n - 1)) = α * (↑√↑n * ↑√↑(n - 1).factorial / α ^ n)
    field_simpnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this:↑√↑(n - 1).factorial ≠ 0⊢ ↑√↑n * α ^ n = ↑√↑n * α ^ (n - 1) * α
    have : α ^ n = α * α ^ (n - 1) := byα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0⊢ a_dag (fun n => ↑√↑n.factorial / α ^ n) n = α • (fun n => ↑√↑n.factorial / α ^ n) nnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this✝:↑√↑(n - 1).factorial ≠ 0this:α ^ n = α * α ^ (n - 1)⊢ ↑√↑n * α ^ n = ↑√↑n * α ^ (n - 1) * α
      exact Eq.symm (mul_pow_sub_one hn α)negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this✝:↑√↑(n - 1).factorial ≠ 0this:α ^ n = α * α ^ (n - 1)⊢ ↑√↑n * α ^ n = ↑√↑n * α ^ (n - 1) * αnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this✝:↑√↑(n - 1).factorial ≠ 0this:α ^ n = α * α ^ (n - 1)⊢ ↑√↑n * α ^ n = ↑√↑n * α ^ (n - 1) * α
    rw [thisnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this✝:↑√↑(n - 1).factorial ≠ 0this:α ^ n = α * α ^ (n - 1)⊢ ↑√↑n * (α * α ^ (n - 1)) = ↑√↑n * α ^ (n - 1) * αnegα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this✝:↑√↑(n - 1).factorial ≠ 0this:α ^ n = α * α ^ (n - 1)⊢ ↑√↑n * (α * α ^ (n - 1)) = ↑√↑n * α ^ (n - 1) * α]negα:ℂhα:α ≠ 0n:ℕhn:n ≠ 0g₀:¬n = 0this✝:↑√↑(n - 1).factorial ≠ 0this:α ^ n = α * α ^ (n - 1)⊢ ↑√↑n * (α * α ^ (n - 1)) = ↑√↑n * α ^ (n - 1) * α
    ring_nfAll goals completed! 🐙

              lemma a_dag_nullspace
    {v : ℕ → ℂ} (hv : a_dag v = 0) : v = 0 := byv:ℕ → ℂhv:a_dag v = 0⊢ v = 0
  unfold a_dag at hvv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0⊢ v = 0
  ext nv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕ⊢ v n = 0 n
  induction n with
  | zero =>zerov:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0⊢ v 0 = 0 0
    have := congrFun hv 1zerov:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0this:(if 1 = 0 then 0 else ↑√↑1 * v (1 - 1)) = 0 1⊢ v 0 = 0 0
    simp at this ⊢zerov:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0this:v 0 = 0⊢ v 0 = 0
    tautoAll goals completed! 🐙
  | succ n hn =>succv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0 n⊢ v (n + 1) = 0 (n + 1)
    have := congrFun hv (n + 2)succv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0 nthis:(if n + 2 = 0 then 0 else ↑√↑(n + 2) * v (n + 2 - 1)) = 0 (n + 2)⊢ v (n + 1) = 0 (n + 1)
    simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, and_false, ↓reduceIte, Nat.cast_add,
      Nat.cast_ofNat, Nat.add_one_sub_one, Pi.zero_apply, mul_eq_zero,
      Complex.ofReal_eq_zero] at this hn hv ⊢succv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0this:√(↑n + 2) = 0 ∨ v (n + 1) = 0⊢ v (n + 1) = 0
    cases this with
    | inl h =>succ.inlv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0h:√(↑n + 2) = 0⊢ v (n + 1) = 0
      exfalsosucc.inlv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0h:√(↑n + 2) = 0⊢ False
      revert hsucc.inlv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0⊢ √(↑n + 2) = 0 → False
      refine Real.sqrt_ne_zero'.mpr ?_succ.inlv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0⊢ 0 < ↑n + 2
      linarithAll goals completed! 🐙
    | inr h =>succ.inrv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = 0n:ℕhn:v n = 0h:v (n + 1) = 0⊢ v (n + 1) = 0
      tautoAll goals completed! 🐙

lemma no_a_dag_eigenvector (α : ℂ) (v : ℕ → ℂ) :
    a_dag v = α • v ↔ v = 0 := byα:ℂv:ℕ → ℂ⊢ a_dag v = α • v ↔ v = 0
  constructormpα:ℂv:ℕ → ℂ⊢ a_dag v = α • v → v = 0mprα:ℂv:ℕ → ℂ⊢ v = 0 → a_dag v = α • v
  ·mpα:ℂv:ℕ → ℂ⊢ a_dag v = α • v → v = 0 intro hvmpα:ℂv:ℕ → ℂhv:a_dag v = α • v⊢ v = 0
    by_cases hα : α = 0posα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:α = 0⊢ v = 0negα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0⊢ v = 0
    ·posα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:α = 0⊢ v = 0 subst αposv:ℕ → ℂhv:a_dag v = 0 • v⊢ v = 0; apply a_dag_nullspaceposv:ℕ → ℂhv:a_dag v = 0 • v⊢ a_dag v = 0; rw [hvposv:ℕ → ℂhv:a_dag v = 0 • v⊢ 0 • v = 0posv:ℕ → ℂhv:a_dag v = 0 • v⊢ 0 • v = 0]posv:ℕ → ℂhv:a_dag v = 0 • v⊢ 0 • v = 0; simpAll goals completed! 🐙
    have := congrFun hv 0negα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0this:a_dag v 0 = (α • v) 0⊢ v = 0
    unfold a_dag at thisnegα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0this:(if 0 = 0 then 0 else ↑√↑0 * v (0 - 1)) = (α • v) 0⊢ v = 0
    ext nnegα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0this:(if 0 = 0 then 0 else ↑√↑0 * v (0 - 1)) = (α • v) 0n:ℕ⊢ v n = 0 n
    induction n with
    | zero =>neg.zeroα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0this:(if 0 = 0 then 0 else ↑√↑0 * v (0 - 1)) = (α • v) 0⊢ v 0 = 0 0 simp at this ⊢neg.zeroα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0this:α = 0 ∨ v 0 = 0⊢ v 0 = 0;tautoAll goals completed! 🐙
    | succ n hn =>neg.succα:ℂv:ℕ → ℂhv:a_dag v = α • vhα:¬α = 0this:(if 0 = 0 then 0 else ↑√↑0 * v (0 - 1)) = (α • v) 0n:ℕhn:v n = 0 n⊢ v (n + 1) = 0 (n + 1)
      unfold a_dag at hvneg.succα:ℂv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = α • vhα:¬α = 0this:(if 0 = 0 then 0 else ↑√↑0 * v (0 - 1)) = (α • v) 0n:ℕhn:v n = 0 n⊢ v (n + 1) = 0 (n + 1)
      have := congrFun hv (n+1)neg.succα:ℂv:ℕ → ℂhv:(fun n => if n = 0 then 0 else ↑√↑n * v (n - 1)) = α • vhα:¬α = 0this✝:(if 0 = 0 then 0 else ↑√↑0 * v (0 - 1)) = (α • v) 0n:ℕhn:v n = 0 nthis:(if n + 1 = 0 then 0 else ↑√↑(n + 1) * v (n + 1 - 1)) = (α • v) (n + 1)⊢ v (n + 1) = 0 (n + 1)
      simp_allAll goals completed! 🐙
  intromprα:ℂv:ℕ → ℂa✝:v = 0⊢ a_dag v = α • v
  subst vmprα:ℂ⊢ a_dag 0 = α • 0
  unfold a_dagmprα:ℂ⊢ (fun n => if n = 0 then 0 else ↑√↑n * 0 (n - 1)) = α • 0
  simpmprα:ℂ⊢ (fun n => 0) = 0
  rflAll goals completed! 🐙

lemma commutationRelation : ⁅aLin, a_dagLin⁆ = 1 := by⊢ ⁅aLin, a_dagLin⁆ = 1
  simp only [Bracket.bracket]⊢ aLin * a_dagLin - a_dagLin * aLin = 1
  unfold aLin a_dagLin⊢ { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } *
      { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } -
    { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } *
      { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } =
  1
  ext x ix:ℕ → ℂi:ℕ⊢ ({ toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } *
        { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } -
      { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } *
        { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 })
    x i =
  1 x i
  change _ = id x ix:ℕ → ℂi:ℕ⊢ ({ toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } *
        { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } -
      { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } *
        { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 })
    x i =
  id x i
  rw [← commutation_relationx:ℕ → ℂi:ℕ⊢ ({ toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } *
        { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } -
      { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } *
        { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 })
    x i =
  (a ∘ a_dag - a_dag ∘ a) x ix:ℕ → ℂi:ℕ⊢ ({ toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } *
        { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } -
      { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } *
        { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 })
    x i =
  (a ∘ a_dag - a_dag ∘ a) x i]x:ℕ → ℂi:ℕ⊢ ({ toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 } *
        { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } -
      { toFun := a_dag, map_add' := a_dagLin._proof_1, map_smul' := a_dagLin._proof_2 } *
        { toFun := a, map_add' := aLin._proof_1, map_smul' := aLin._proof_2 })
    x i =
  (a ∘ a_dag - a_dag ∘ a) x i
  simpAll goals completed! 🐙


/-- The `coherentState` with parameter `0` is just the first basis vector. -/
example : coherentState 0 = fun n => ite (n = 0) 1 0 := by⊢ coherentState 0 = fun n => if n = 0 then 1 else 0
  unfold coherentState⊢ (fun n => ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ n / ↑√↑n.factorial) = fun n => if n = 0 then 1 else 0
  ext nn:ℕ⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ n / ↑√↑n.factorial = if n = 0 then 1 else 0
  split_ifs with g₀posn:ℕg₀:n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ n / ↑√↑n.factorial = 1negn:ℕg₀:¬n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ n / ↑√↑n.factorial = 0
  ·posn:ℕg₀:n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ n / ↑√↑n.factorial = 1 subst npos⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ 0 / ↑√↑(Nat.factorial 0) = 1;simpAll goals completed! 🐙
  ·negn:ℕg₀:¬n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 ^ n / ↑√↑n.factorial = 0 rw [zero_pow g₀negn:ℕg₀:¬n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 / ↑√↑n.factorial = 0negn:ℕg₀:¬n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 / ↑√↑n.factorial = 0]negn:ℕg₀:¬n = 0⊢ ↑(Real.exp (-‖0‖ ^ 2 / 2)) * 0 / ↑√↑n.factorial = 0
    simpAll goals completed! 🐙

The coherent state belongs to ℓ²(ℂ).


def coherentState_ℓ2 (α : ℂ) : lp (fun _ : ℕ => ℂ) 2 := {
  val := coherentState α
  property := byα:ℂ⊢ coherentState α ∈ lp (fun x => ℂ) 2
    simp only [lp, Memℓp, OfNat.ofNat_ne_zero, ↓reduceIte, ENNReal.ofNat_ne_top, Summable,
      ENNReal.toReal_ofNat, Real.rpow_ofNat, AddSubgroup.mem_mk, AddSubmonoid.mem_mk,
      AddSubsemigroup.mem_mk, Set.mem_setOf_eq, coherentState, Complex.ofReal_exp,
      Complex.ofReal_div, Complex.ofReal_neg, Complex.ofReal_pow, Complex.ofReal_ofNat,
      Complex.norm_div, Complex.norm_mul, norm_pow, Complex.norm_real, Real.norm_eq_abs]α:ℂ⊢ ∃ a, HasSum (fun i => (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ i / |√↑i.factorial|) ^ 2) a
    use (‖Complex.exp (-↑‖α‖ ^ 2 / 2)^2 * Complex.exp (‖α‖^2)‖)hα:ℂ⊢ HasSum (fun i => (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ i / |√↑i.factorial|) ^ 2)
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖
    suffices HasSum (fun i : ℕ ↦ ( ‖α‖ ^ i
      / |√↑i.factorial|) ^ 2)
      ‖Complex.exp (↑‖α‖ ^ 2)‖ byα:ℂthis:HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ i / |√↑i.factorial|) ^ 2)
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
      simp_rw [α:ℂthis:HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ i / |√↑i.factorial|) ^ 2)
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖div_powα:ℂthis:HasSum (fun i => (‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2)
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖] at *
      simp_rw [α:ℂthis:HasSum (fun i => (‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ * ‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2)
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖mul_pow,α:ℂthis:HasSum (fun i => (‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => ‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ ^ 2 * (‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2)
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖ ← mul_divα:ℂthis:HasSum (fun i => (‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => ‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ ^ 2 * ((‖α‖ ^ i) ^ 2 / |√↑i.factorial| ^ 2))
  ‖Complex.exp (-↑‖α‖ ^ 2 / 2) ^ 2 * Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖]
      simp only [sq_abs, Nat.cast_nonneg, Real.sq_sqrt, Complex.norm_mul, norm_pow] at *α:ℂthis:HasSum (fun i => (‖α‖ ^ i) ^ 2 / ↑i.factorial) ‖Complex.exp (↑‖α‖ ^ 2)‖⊢ HasSum (fun i => ‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ ^ 2 * ((‖α‖ ^ i) ^ 2 / ↑i.factorial))
  (‖Complex.exp (-↑‖α‖ ^ 2 / 2)‖ ^ 2 * ‖Complex.exp (↑‖α‖ ^ 2)‖)hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
      exact HasSum.const_smul (γ := ℝ) _ thishα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖hα:ℂ⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
    have (r : ℝ) : |√r| = √r := byα:ℂ⊢ coherentState α ∈ lp (fun x => ℂ) 2hα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
      rw [abs_eq_selfα:ℂr:ℝ⊢ 0 ≤ √rα:ℂr:ℝ⊢ 0 ≤ √rhα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖]α:ℂr:ℝ⊢ 0 ≤ √rhα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
      simphα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖hα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
    simp_rw [hα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / |√↑i.factorial|) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖this,hα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i / √↑i.factorial) ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖ div_powhα:ℂthis:∀ (r : ℝ), |√r| = √r⊢ HasSum (fun i => (‖α‖ ^ i) ^ 2 / √↑i.factorial ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖]
    have (i : ℕ) : (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i := pow_right_comm ‖α‖ i 2hα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i⊢ HasSum (fun i => (‖α‖ ^ i) ^ 2 / √↑i.factorial ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖
    simp_rw [hα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i⊢ HasSum (fun i => (‖α‖ ^ i) ^ 2 / √↑i.factorial ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖thishα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i⊢ HasSum (fun i => (‖α‖ ^ 2) ^ i / √↑i.factorial ^ 2) ‖Complex.exp (↑‖α‖ ^ 2)‖]
    rw [← Complex.ofReal_powhα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i⊢ HasSum (fun i => (‖α‖ ^ 2) ^ i / √↑i.factorial ^ 2) ‖Complex.exp ↑(‖α‖ ^ 2)‖hα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i⊢ HasSum (fun i => (‖α‖ ^ 2) ^ i / √↑i.factorial ^ 2) ‖Complex.exp ↑(‖α‖ ^ 2)‖]hα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ i⊢ HasSum (fun i => (‖α‖ ^ 2) ^ i / √↑i.factorial ^ 2) ‖Complex.exp ↑(‖α‖ ^ 2)‖
    generalize ‖α‖^2 = Ahα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝ⊢ HasSum (fun i => A ^ i / √↑i.factorial ^ 2) ‖Complex.exp ↑A‖
    simp only [Nat.cast_nonneg, Real.sq_sqrt, Complex.norm_exp_ofReal]hα:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝ⊢ HasSum (fun i => A ^ i / ↑i.factorial) (Real.exp A)
    convert! NormedSpace.expSeries_hasSum_exp (𝕂 := ℝ) Ae'_5α:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝx✝:ℕ⊢ A ^ x✝ / ↑x✝.factorial = (NormedSpace.expSeries ℝ ℝ x✝) fun x => Ae'_6α:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝ⊢ Real.exp = NormedSpace.exp
    ·e'_5α:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝx✝:ℕ⊢ A ^ x✝ / ↑x✝.factorial = (NormedSpace.expSeries ℝ ℝ x✝) fun x => A simp [NormedSpace.expSeries]e'_5α:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝx✝:ℕ⊢ A ^ x✝ / ↑x✝.factorial = (↑x✝.factorial)⁻¹ * A ^ x✝
      field_simpAll goals completed! 🐙
    ·e'_6α:ℂthis✝:∀ (r : ℝ), |√r| = √rthis:∀ (i : ℕ), (‖α‖ ^ i) ^ 2 = (‖α‖ ^ 2) ^ iA:ℝ⊢ Real.exp = NormedSpace.exp exact Real.exp_eq_exp_ℝAll goals completed! 🐙
}