OAI/Algebra/DepthFive/FockMonomials.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem335.multiFactorial line 12

    Source documentation

    The product of coordinate factorials of an exponent vector.

    def multiFactorial (d : σ →₀ ℕ) : ℕ := ∏ i, (d i).factorial
…
  2. lemma OAI.Problem335.multiFactorial_pos line 15
  3. lemma OAI.Problem335.multiFactorial_add_single line 18
  4. def OAI.Problem335.fockMonomial line 36

    Source documentation

    A factorial-normalized real monomial, the algebraic part of the Bargmann--Fock basis used in the moment calculation.

    def fockMonomial (d : σ →₀ ℕ) : MvPolynomial σ ℝ :=
…
  5. lemma OAI.Problem335.sqrt_multiFactorial_pos line 40
  6. lemma OAI.Problem335.sqrt_multiFactorial_add_single line 44
  7. lemma OAI.Problem335.X_mul_fockMonomial line 50
  8. lemma OAI.Problem335.pderiv_fockMonomial_add_single line 61
  9. lemma OAI.Problem335.pderiv_fockMonomial line 76
  10. def OAI.Problem335.fockBasis line 92

    Source documentation

    The normalized monomials form a basis, by rescaling the monomial basis with nonzero coefficients.

    def fockBasis : Module.Basis (σ →₀ ℕ) ℝ (MvPolynomial σ ℝ) :=
…
  11. lemma OAI.Problem335.fockBasis_apply line 98
  12. def OAI.Problem335.complexFockMonomial line 103

    Source documentation

    Complex normalized monomials are obtained by coefficient extension.

    def complexFockMonomial (d : σ →₀ ℕ) : MvPolynomial σ ℂ :=
…
  13. lemma OAI.Problem335.complexFockMonomial_eq line 107
  14. lemma OAI.Problem335.X_mul_complexFockMonomial line 112
  15. lemma OAI.Problem335.pderiv_complexFockMonomial line 118
  16. def OAI.Problem335.complexFockBasis line 126

    Source documentation

    Complex version of the normalized monomial basis.

    def complexFockBasis : Module.Basis (σ →₀ ℕ) ℂ (MvPolynomial σ ℂ) :=
…
  17. lemma OAI.Problem335.complexFockBasis_apply line 132
  18. lemma OAI.Problem335.complexFockBasis_repr line 138