PathOccupationAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.sum_pathAmplitude_sq_split line 19

Source documentation

Exact source-index sum for a squarefree Fock path, expressed over the independent derivative and multiplication occupation spaces.

theorem sum_pathAmplitude_sq_split (p : List σ) (hp : p.Nodup) :
    (∑ d : {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a, b)},
      ((p.map (occupationAmplitude side d.val)).prod) ^ 2) =
    (∑ d : {d : {i // side i = true} → ℕ // ∑ i, d i = a},
      ∏ i ∈ selectedPathCoordinates side p true, (d.val i : ℝ)) *
    (∑ d : {d : {i // ¬side i = true} → ℕ // ∑ i, d i = b},
      ∏ i ∈ complementaryPathCoordinates side p, ((d.val i : ℝ) + 1)) := by
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.occupationAmplitude, OAI.Problem335.selectedPathCoordinates, OAI.Problem335.complementaryPathCoordinates

theorem OAI.Problem335.mean_pathAmplitude_sq_split line 31

Source documentation

The normalized squared amplitude is the product of the two uniform squarefree occupation means, including every inactive ambient coordinate.

theorem mean_pathAmplitude_sq_split (p : List σ) (hp : p.Nodup) :
    (∑ d : {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a, b)},
      ((p.map (occupationAmplitude side d.val)).prod) ^ 2) /
      Fintype.card {d : σ →₀ ℕ // Finsupp.weight (bidegreeWeight side) d = (a, b)} =
    ((∑ d : {d : {i // side i = true} → ℕ // ∑ i, d i = a},
      ∏ i ∈ selectedPathCoordinates side p true, (d.val i : ℝ)) /
      Fintype.card {d : {i // side i = true} → ℕ // ∑ i, d i = a}) *
    ((∑ d : {d : {i // ¬side i = true} → ℕ // ∑ i, d i = b},
      ∏ i ∈ complementaryPathCoordinates side p, ((d.val i : ℝ) + 1)) /
      Fintype.card {d : {i // ¬side i = true} → ℕ // ∑ i, d i = b}) := by
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.occupationAmplitude, OAI.Problem335.selectedPathCoordinates, OAI.Problem335.complementaryPathCoordinates