FockBidegreeBasis.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem335.BidegreeIndex line 15
Source documentation
Exponent vectors at a fixed derivative/multiplication bidegree.
```
abbrev BidegreeIndex (isV : σ → Bool) (a b : ℕ) :=
…
```
def OAI.Problem335.bidegreeFockBasis line 23
Source documentation
The real factorial-normalized monomial basis at fixed bidegree.
```
def bidegreeFockBasis (isV : σ → Bool) (a b : ℕ) :
    Module.Basis (BidegreeIndex isV a b) ℝ (bidegreeSubmodule (K := ℝ) isV a b) :=
…
```
Mentions: OAI.Problem335.BidegreeIndex, OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.bidegreeFockBasis_apply line 29
theorem OAI.Problem335.bidegreeFockBasis_repr line 36
def OAI.Problem335.bidegreeComplexFockBasis line 45
Source documentation
The complex factorial-normalized monomial basis at fixed bidegree.
```
def bidegreeComplexFockBasis (isV : σ → Bool) (a b : ℕ) :
    Module.Basis (BidegreeIndex isV a b) ℂ (bidegreeSubmodule (K := ℂ) isV a b) :=
…
```
Mentions: OAI.Problem335.BidegreeIndex, OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.bidegreeComplexFockBasis_apply line 51
theorem OAI.Problem335.bidegreeComplexFockBasis_repr line 58
theorem OAI.Problem335.toMatrix_bidegreeComplexFockBasis_apply line 70
Source documentation
The finite Fock-basis matrix is precisely the square-root diagonal normalization of the ordinary monomial-basis matrix.
```
theorem toMatrix_bidegreeComplexFockBasis_apply (isV : σ → Bool)
    (a b c d : ℕ)
    (f : bidegreeSubmodule (K := ℂ) isV a b →ₗ[ℂ]
…
```
Mentions: OAI.Problem335.bidegreeSubmodule
theorem OAI.Problem335.rank_toMatrix_bidegreeComplexFockBasis line 89
Source documentation
Finite Fock normalization leaves the rank of the restricted operator unchanged.
```
theorem rank_toMatrix_bidegreeComplexFockBasis (isV : σ → Bool)
    (a b c d : ℕ)
    (f : bidegreeSubmodule (K := ℂ) isV a b →ₗ[ℂ]
…
```
Mentions: OAI.Problem335.bidegreeSubmodule