Fock space

TheoremSquared norms of the Fock kernel coefficients#✓fully proved

The squared norms of the Fock kernel coefficients are ‖z‖ ^ (2 * n) / n!.

theorem norm_sq_fock_coeff (z : ℂ) (n : ℕ) :
    ‖(starRingEnd ℂ z) ^ n / (Real.sqrt (Nat.factorial n : ℝ) : ℂ)‖ ^ (2 : ℝ) =
      (‖z‖ ^ 2) ^ n / (Nat.factorial n : ℝ)

Used by 2

Used byFock kernel coefficients lie in ℓ² · Squared norm of the Fock kernel

TheoremFock kernel coefficients lie in ℓ²#✓fully proved

The Fock kernel coefficients are in ℓ² for every z : ℂ, since ∑' n, ‖z‖ ^ (2 * n) / n! = Real.exp ‖z‖².

theorem memℓp_fockKernel (z : ℂ) :
    Memℓp (fun n : ℕ => (starRingEnd ℂ z) ^ n / (Real.sqrt (Nat.factorial n : ℝ) : ℂ)) 2

Uses 1 · Used by 1

Proof usesSquared norms of the Fock kernel coefficients

Used byReproducing kernel of the Fock space

DefinitionReproducing kernel of the Fock space#✓fully proved

The Fock kernel at z: the ℓ²(ℕ, ℂ) sequence with coefficients (conj z)ⁿ / √(n!).

noncomputable def fockKernel (z : ℂ) : ℓ²(ℕ, ℂ) :=
  ⟨fun n => (starRingEnd ℂ z) ^ n / (Real.sqrt (Nat.factorial n : ℝ) : ℂ), memℓp_fockKernel z⟩

Uses 1 · Used by 17

Statement usesFock kernel coefficients lie in ℓ²

Used byCoherent state in the Fock space · Point evaluation on the Fock space · Point evaluation as a bounded functional on the Fock space · Fock-space point evaluation as a Taylor series · Fock kernel evaluated at its own point · Fock-space evaluation of a single monomial · Fock-space evaluation at the origin is the constant coefficient · Fock kernel at the origin is the first basis vector · Inner product of two coherent states · Inner product of two Fock kernels is an exponential · Conjugate reproducing property of the Fock kernel · Coherent states are unit vectors · Norm of Fock-space point evaluation · Norm of the Fock kernel · Modulus of the inner product of two Fock kernels · Squared norm of the Fock kernel · Absolute convergence of Taylor series in the Fock space

TheoremFock kernel at the origin is the first basis vector#✓fully proved

The Fock kernel at 0 is the first standard basis vector.

theorem fockKernel_zero :
    fockKernel (0 : ℂ) = lp.single 2 0 (1 : ℂ)

Uses 1 · Used by 1

Statement usesReproducing kernel of the Fock space

Used byFock-space evaluation at the origin is the constant coefficient

TheoremSquared norm of the Fock kernel#✓fully proved

The squared norm of the Fock kernel is Real.exp ‖z‖².

theorem norm_sq_fockKernel (z : ℂ) :
    ‖fockKernel z‖ ^ 2 = Real.exp (‖z‖ ^ 2)

Uses 2 · Used by 1

Statement usesReproducing kernel of the Fock space

Proof usesSquared norms of the Fock kernel coefficients

Used byNorm of the Fock kernel

TheoremNorm of the Fock kernel#✓fully proved

The norm of the Fock kernel is Real.exp (‖z‖² / 2).

theorem norm_fockKernel (z : ℂ) :
    ‖fockKernel z‖ = Real.exp (‖z‖ ^ 2 / 2)

Uses 2 · Used by 2

Statement usesReproducing kernel of the Fock space

Proof usesSquared norm of the Fock kernel

Used byCoherent states are unit vectors · Norm of Fock-space point evaluation

DefinitionPoint evaluation on the Fock space#✓fully proved

Point evaluation on the Fock space: the inner product with the Fock kernel.

noncomputable def fockEval (z : ℂ) (a : ℓ²(ℕ, ℂ)) : ℂ :=
  ⟪fockKernel z, a⟫

Uses 1 · Used by 7

Statement usesReproducing kernel of the Fock space

Used byReproducing property of the Fock kernel · Fock-space point evaluation as a Taylor series · Fock kernel evaluated at its own point · Fock-space evaluation of a single monomial · Fock-space evaluation at the origin is the constant coefficient · Conjugate reproducing property of the Fock kernel · Pointwise bound for Fock-space functions

TheoremFock-space point evaluation as a Taylor series#✓fully proved

Point evaluation is the Taylor series ∑' n, a n * zⁿ / √(n!).

theorem fockEval_eq_tsum (z : ℂ) (a : ℓ²(ℕ, ℂ)) :
    fockEval z a = ∑' n, a n * z ^ n / (Real.sqrt (Nat.factorial n : ℝ) : ℂ)

Uses 2

Statement usesPoint evaluation on the Fock space

Proof usesReproducing kernel of the Fock space

TheoremAbsolute convergence of Taylor series in the Fock space#✓fully proved

The Taylor series of a Fock-space function converges absolutely at every point of ℂ.

theorem summable_fockEval_terms (z : ℂ) (a : ℓ²(ℕ, ℂ)) :
    Summable (fun n => a n * z ^ n / (Real.sqrt (Nat.factorial n : ℝ) : ℂ))

Uses 1

Proof usesReproducing kernel of the Fock space

DefinitionPoint evaluation as a bounded functional on the Fock space#✓fully proved

Point evaluation as a bounded linear functional on the Fock space.

noncomputable def fockEvalCLM (z : ℂ) : ℓ²(ℕ, ℂ) →L[ℂ] ℂ :=
  innerSL ℂ (fockKernel z)

Uses 1 · Used by 3

Statement usesReproducing kernel of the Fock space

Used byReproducing property of the Fock kernel · Norm of Fock-space point evaluation · Pointwise bound for Fock-space functions

TheoremReproducing property of the Fock kernel#✓fully proved

The bounded point-evaluation functional acts by the inner product with the Fock kernel.

theorem fockEvalCLM_apply (z : ℂ) (a : ℓ²(ℕ, ℂ)) :
    fockEvalCLM z a = fockEval z a

Uses 2 · Used by 1

Statement usesPoint evaluation on the Fock space · Point evaluation as a bounded functional on the Fock space

Used byPointwise bound for Fock-space functions

TheoremNorm of Fock-space point evaluation#✓fully proved

The operator norm of point evaluation is Real.exp (‖z‖² / 2).

theorem norm_fockEvalCLM (z : ℂ) :
    ‖fockEvalCLM z‖ = Real.exp (‖z‖ ^ 2 / 2)

Uses 3 · Used by 1

Statement usesPoint evaluation as a bounded functional on the Fock space

Proof usesReproducing kernel of the Fock space · Norm of the Fock kernel

Used byPointwise bound for Fock-space functions

TheoremPointwise bound for Fock-space functions#✓fully proved

The pointwise bound for Fock-space functions: ‖f(z)‖ ≤ ‖f‖ * Real.exp (‖z‖² / 2).

theorem norm_fockEval_le (z : ℂ) (a : ℓ²(ℕ, ℂ)) :
    ‖fockEval z a‖ ≤ ‖a‖ * Real.exp (‖z‖ ^ 2 / 2)

Uses 4

Statement usesPoint evaluation on the Fock space

Proof usesPoint evaluation as a bounded functional on the Fock space · Reproducing property of the Fock kernel · Norm of Fock-space point evaluation

TheoremFock-space evaluation at the origin is the constant coefficient#✓fully proved

Evaluation at 0 is the constant Taylor coefficient.

theorem fockEval_zero (a : ℓ²(ℕ, ℂ)) :
    fockEval (0 : ℂ) a = a 0

Uses 3

Statement usesPoint evaluation on the Fock space

Proof usesReproducing kernel of the Fock space · Fock kernel at the origin is the first basis vector

TheoremFock-space evaluation of a single monomial#✓fully proved

Evaluation of a monomial c * zⁿ / √(n!) (a single Taylor coefficient).

theorem fockEval_single (z : ℂ) (n : ℕ) (c : ℂ) :
    fockEval z (lp.single 2 n c) = c * z ^ n / (Real.sqrt (Nat.factorial n : ℝ) : ℂ)

Uses 2

Statement usesPoint evaluation on the Fock space

Proof usesReproducing kernel of the Fock space

TheoremConjugate reproducing property of the Fock kernel#✓fully proved

The reproducing property in the other order: ⟪a, k_z⟫ = conj (f(z)).

theorem inner_fockKernel_right (z : ℂ) (a : ℓ²(ℕ, ℂ)) :
    ⟪a, fockKernel z⟫ = (starRingEnd ℂ) (fockEval z a)

Uses 2

Statement usesPoint evaluation on the Fock space · Reproducing kernel of the Fock space

TheoremInner product of two Fock kernels is an exponential#✓fully proved

The inner product of two Fock kernels is the Fock kernel function Complex.exp (z * conj w).

theorem inner_fockKernel_fockKernel (z w : ℂ) :
    ⟪fockKernel z, fockKernel w⟫ = Complex.exp (z * (starRingEnd ℂ w))

Uses 1 · Used by 3

Statement usesReproducing kernel of the Fock space

Used byFock kernel evaluated at its own point · Inner product of two coherent states · Modulus of the inner product of two Fock kernels

TheoremModulus of the inner product of two Fock kernels#✓fully proved

The norm of the inner product of two Fock kernels is Real.exp (z * conj w).re.

theorem norm_inner_fockKernel_fockKernel (z w : ℂ) :
    ‖⟪fockKernel z, fockKernel w⟫‖ = Real.exp (z * (starRingEnd ℂ w)).re

Uses 2

Statement usesReproducing kernel of the Fock space

Proof usesInner product of two Fock kernels is an exponential

TheoremFock kernel evaluated at its own point#✓fully proved

Evaluation of the kernel at its own point: f_z(k_z) = Real.exp ‖z‖², so the pointwise bound is sharp.

theorem fockEval_fockKernel (z : ℂ) :
    fockEval z (fockKernel z) = ((Real.exp (‖z‖ ^ 2) : ℝ) : ℂ)

Uses 3

Statement usesPoint evaluation on the Fock space · Reproducing kernel of the Fock space

Proof usesInner product of two Fock kernels is an exponential

DefinitionNormalized monomials in the Fock space#✓fully proved

The normalized monomial eₙ(z) = zⁿ / √(n!), represented by the nth standard basis vector in the Taylor-coefficient model of Fock space.

@[reducible] noncomputable def fockMonomial (n : ℕ) : ℓ²(ℕ, ℂ) :=
  lp.single 2 n (1 : ℂ)

Used by 3

Used byFock coefficients as inner products with normalized monomials · Normalized Fock monomials are orthonormal standard basis vectors · Normalized Fock monomials form an orthonormal family

TheoremNormalized Fock monomials are orthonormal standard basis vectors#✓fully proved

The rescaled monomials eₙ(z) = zⁿ / √(n!), i.e. the standard basis vectors of the coefficient model, are orthonormal.

theorem fockMonomial_orthonormal (m n : ℕ) :
    ⟪fockMonomial m, fockMonomial n⟫_ℂ =
      if m = n then (1 : ℂ) else 0

Uses 1 · Used by 1

Statement usesNormalized monomials in the Fock space

Used byNormalized Fock monomials form an orthonormal family

TheoremNormalized Fock monomials form an orthonormal family#✓fully proved

The normalized monomial family satisfies Mathlib's standard orthonormal predicate.

theorem orthonormal_fockMonomial : Orthonormal ℂ fockMonomial

Uses 2

Statement usesNormalized monomials in the Fock space

Proof usesNormalized Fock monomials are orthonormal standard basis vectors

TheoremFock coefficients as inner products with normalized monomials#✓fully proved

The coefficient of a at n is the inner product with eₙ.

theorem fockCoeff_eq_inner (a : ℓ²(ℕ, ℂ)) (n : ℕ) :
    a n = ⟪fockMonomial n, a⟫

Uses 1

Statement usesNormalized monomials in the Fock space

DefinitionCoherent state in the Fock space#✓fully proved

The coherent state at z: the normalized Fock kernel, ĉ_z = Real.exp (-‖z‖² / 2) • k_z.

noncomputable def fockCoherent (z : ℂ) : ℓ²(ℕ, ℂ) :=
  ((Real.exp (-‖z‖ ^ 2 / 2) : ℝ) : ℂ) • fockKernel z

Uses 1 · Used by 3

Statement usesReproducing kernel of the Fock space

Used byInner product of two coherent states · Coherent states are unit vectors · Gaussian overlap of coherent states

TheoremCoherent states are unit vectors#✓fully proved

Coherent states are unit vectors.

theorem norm_fockCoherent (z : ℂ) : ‖fockCoherent z‖ = 1

Uses 3

Statement usesCoherent state in the Fock space

Proof usesReproducing kernel of the Fock space · Norm of the Fock kernel

TheoremInner product of two coherent states#✓fully proved

The inner product of two coherent states.

theorem inner_fockCoherent_fockCoherent (z w : ℂ) :
    ⟪fockCoherent z, fockCoherent w⟫ =
      Complex.exp (z * (starRingEnd ℂ w) -
        (((‖z‖ ^ 2 + ‖w‖ ^ 2) / 2 : ℝ) : ℂ))

Uses 3 · Used by 1

Statement usesCoherent state in the Fock space

Proof usesReproducing kernel of the Fock space · Inner product of two Fock kernels is an exponential

Used byGaussian overlap of coherent states

TheoremGaussian overlap of coherent states#✓fully proved

The overlap of two coherent states is Gaussian: ‖⟪ĉ_z, ĉ_w⟫‖ = Real.exp (-‖z - w‖² / 2).

theorem norm_inner_fockCoherent_fockCoherent (z w : ℂ) :
    ‖⟪fockCoherent z, fockCoherent w⟫‖ = Real.exp (-‖z - w‖ ^ 2 / 2)

Uses 2

Statement usesCoherent state in the Fock space

Proof usesInner product of two coherent states

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.