FockPaths.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.stepOccupation line 14
Source documentation
Occupation update for one derivative or multiplication variable. Natural subtraction is harmless when the derivative coefficient vanishes.
```
def stepOccupation (isV : σ → Bool) (i : σ) (d : σ →₀ ℕ) : σ →₀ ℕ :=
…
```
def OAI.Problem335.pathOccupation line 18
Source documentation
Occupation update for a variable path, in operator-composition order.
```
def pathOccupation (isV : σ → Bool) (l : List σ) (d : σ →₀ ℕ) : σ →₀ ℕ :=
…
```
def OAI.Problem335.occupationAmplitude line 22
Source documentation
The nonnegative coefficient of one normalized creation/annihilation step.
```
def occupationAmplitude (isV : σ → Bool) (d : σ →₀ ℕ) (i : σ) : ℝ :=
…
```
lemma OAI.Problem335.occupationAmplitude_nonneg line 26
lemma OAI.Problem335.stepOccupation_apply_of_ne line 30
lemma OAI.Problem335.pathOccupation_apply_of_not_mem line 35
lemma OAI.Problem335.variableOperator_complexFockMonomial line 47
theorem OAI.Problem335.mixedOperator_path_complexFockMonomial line 57
Source documentation
Exact factorial-normalized action of a product of distinct variables. This is the sparse path-coefficient formula needed for IMM trace moments.
```
theorem mixedOperator_path_complexFockMonomial (isV : σ → Bool)
    (l : List σ) (hl : l.Nodup) (d : σ →₀ ℕ) :
    mixedOperator isV ((l.map (MvPolynomial.X : σ → MvPolynomial σ ℂ)).prod)
      (complexFockMonomial d) =
    (((l.map (occupationAmplitude isV d)).prod : ℝ) : ℂ) •
      complexFockMonomial (pathOccupation isV l d) := by
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.complexFockMonomial, OAI.Problem335.occupationAmplitude, OAI.Problem335.pathOccupation
theorem OAI.Problem335.pathAmplitude_sq line 83
Source documentation
Squaring the normalized path amplitude gives exactly the occupation polynomial, with no factorials or square roots left.
```
theorem pathAmplitude_sq (isV : σ → Bool) (l : List σ) (d : σ →₀ ℕ) :
    ((l.map (occupationAmplitude isV d)).prod) ^ 2 =
      (l.map (fun i => if isV i then (d i : ℝ) else (d i : ℝ) + 1)).prod := by
…
```
Mentions: OAI.Problem335.occupationAmplitude
lemma OAI.Problem335.occupationAmplitude_eq_zero_iff line 95
lemma OAI.Problem335.pathAmplitude_eq_zero_iff line 103
def OAI.Problem335.signedOccupation line 109
Source documentation
An occupation vector viewed as a signed exponent vector.
```
def signedOccupation (d : σ →₀ ℕ) : σ →₀ ℤ :=
…
```
lemma OAI.Problem335.signedOccupation_apply line 113
lemma OAI.Problem335.signedOccupation_injective line 117
lemma OAI.Problem335.signedOccupation_eq_iff line 125
def OAI.Problem335.occupationShift line 130
Source documentation
The signed shift of a product of variable operators.
```
def occupationShift (isV : σ → Bool) (l : List σ) : σ →₀ ℤ :=
…
```
lemma OAI.Problem335.signedOccupation_step line 134
lemma OAI.Problem335.signedOccupation_path_of_valid line 150
theorem OAI.Problem335.signedOccupation_path_of_amplitude_ne_zero line 169
Source documentation
A nonzero path amplitude guarantees that natural subtraction agrees with the signed path shift, including at every intermediate occupation.
```
theorem signedOccupation_path_of_amplitude_ne_zero (isV : σ → Bool) (l : List σ)
    (hl : l.Nodup) (d : σ →₀ ℕ)
    (hamp : (l.map (occupationAmplitude isV d)).prod ≠ 0) :
    signedOccupation (pathOccupation isV l d) = signedOccupation d + occupationShift isV l := by
…
```
Mentions: OAI.Problem335.occupationAmplitude, OAI.Problem335.signedOccupation, OAI.Problem335.pathOccupation, OAI.Problem335.occupationShift