PathOccupationGroups.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.selectedPathCoordinates line 14
Source documentation
Coordinates of one path belonging to a fixed Boolean variable group, viewed in that group's own coordinate type.
```
def selectedPathCoordinates (side : σ → Bool) (p : List σ) (b : Bool) :
    Finset {x // side x = b} :=
…
```
theorem OAI.Problem335.mem_selectedPathCoordinates line 18
theorem OAI.Problem335.card_selectedPathCoordinates line 23

theorem OAI.Problem335.path_product_split line 36

Source documentation

Partitioning a squarefree path product into its two coordinate groups.

theorem path_product_split {R : Type*} [CommMonoid R]
    (side : σ → Bool) (p : List σ) (hp : p.Nodup) (f g : σ → R) :
    (p.map (fun x => if side x then f x else g x)).prod =
      (∏ x ∈ selectedPathCoordinates side p true, f x.val) *
        ∏ x ∈ selectedPathCoordinates side p false, g x.val := by
…

Mentions: OAI.Problem335.selectedPathCoordinates

theorem OAI.Problem335.pathAmplitude_sq_split line 60

Source documentation

The squared Fock amplitude is exactly the product of the derivative occupations and successor multiplication occupations, on disjoint group types.

theorem pathAmplitude_sq_split [Fintype σ] (side : σ → Bool)
    (p : List σ) (hp : p.Nodup) (d : σ →₀ ℕ) :
    ((p.map (occupationAmplitude side d)).prod) ^ 2 =
      (∏ x ∈ selectedPathCoordinates side p true, (d x.val : ℝ)) *
        ∏ x ∈ selectedPathCoordinates side p false, ((d x.val : ℝ) + 1) := by
…

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

theorem OAI.Problem335.card_selectedPathCoordinates_of_labels line 70

Source documentation

Selecting coordinates from a path selects exactly the same number as selecting its layer labels.

theorem card_selectedPathCoordinates_of_labels {ι : Type*} [DecidableEq ι]
    (side : σ → Bool) (labels : List σ) (p : List (σ × ι × ι))
    (hlabels : p.map Prod.fst = labels) (hnodup : labels.Nodup) (b : Bool) :
    (selectedPathCoordinates (fun x : σ × ι × ι => side x.1) p b).card =
      (labels.filter (fun x => side x == b)).length := by
…

Mentions: OAI.Problem335.selectedPathCoordinates

theorem OAI.Problem335.immPath_selectedCoordinates_card line 82

Source documentation

Every actual IMM path selects one coordinate in each selected layer, including when the ambient layer has inactive endpoint coordinates.

theorem immPath_selectedCoordinates_card (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (p : List (Fin n × Fin n × Fin n))
    (hp : p ∈ immPaths n hn) (b : Bool) :
    (selectedPathCoordinates (fun x : Fin n × Fin n × Fin n => side x.1) p b).card =
      (Finset.univ.filter (fun t : Fin n => side t = b)).card := by
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.selectedPathCoordinates

theorem OAI.Problem335.immPathAmplitude_sq_split line 96

Source documentation

Concrete IMM first-trace path mass in the two independent occupation groups.

theorem immPathAmplitude_sq_split (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (p : List (Fin n × Fin n × Fin n))
    (hp : p ∈ immPaths n hn) (d : (Fin n × Fin n × Fin n) →₀ ℕ) :
    ((p.map (occupationAmplitude (fun x => side x.1) d)).prod) ^ 2 =
      (∏ x ∈ selectedPathCoordinates (fun x : Fin n × Fin n × Fin n => side x.1)
        p true, (d x.val : ℝ)) *
      ∏ x ∈ selectedPathCoordinates (fun x : Fin n × Fin n × Fin n => side x.1)
        p false, ((d x.val : ℝ) + 1) :=
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.occupationAmplitude, OAI.Problem335.selectedPathCoordinates

def OAI.Problem335.complementaryPathCoordinates line 107
Source documentation
Complement-fiber version, aligned with bidegreeExponentsEquiv.
```
def complementaryPathCoordinates (side : σ → Bool) (p : List σ) :
    Finset {x // ¬side x = true} :=
…
```
theorem OAI.Problem335.mem_complementaryPathCoordinates line 111
theorem OAI.Problem335.path_product_split_complement line 116
theorem OAI.Problem335.pathAmplitude_sq_split_complement line 134
theorem OAI.Problem335.immPath_complementaryCoordinates_card line 142