ImmOperatorPaths.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.immOperatorPaths_enumeration_nodup line 15
Source documentation
Enumerating labelled matrix paths never repeats an edge list.
```
private theorem immOperatorPaths_enumeration_nodup {σ ι : Type*} [Fintype ι] [DecidableEq ι]
    (labels : List σ) (i j : ι) : (matrixEntryPaths labels i j).Nodup := by
…
```
Mentions: OAI.Problem335.matrixEntryPaths
def OAI.Problem335.immPaths line 35
Source documentation
The canonical labelled paths contributing to the endpoint IMM entry.
```
def immPaths (n : ℕ) (hn : 0 < n) : List (List (Fin n × Fin n × Fin n)) :=
…
```
theorem OAI.Problem335.immPaths_labels line 39
Source documentation
Every IMM path uses exactly one coordinate in each layer, in layer order.
```
theorem immPaths_labels (n : ℕ) (hn : 0 < n)
    (p : List (Fin n × Fin n × Fin n)) (hp : p ∈ immPaths n hn) :
    p.map Prod.fst = List.finRange n :=
…
```
Mentions: OAI.Problem335.immPaths
theorem OAI.Problem335.immPaths_get_injective line 45
Source documentation
Distinct path indices select distinct edge lists.
```
theorem immPaths_get_injective (n : ℕ) (hn : 0 < n) :
    Function.Injective (immPaths n hn).get := by
…
```
Mentions: OAI.Problem335.immPaths
theorem OAI.Problem335.immPaths_length line 51
Source documentation
The number of endpoint paths is n^(n-1).
```
theorem immPaths_length (n : ℕ) (hn : 0 < n) :
    (immPaths n hn).length = n ^ (n - 1) := by
…
```
Mentions: OAI.Problem335.immPaths
theorem OAI.Problem335.imm_eq_sum_path_products line 60
Source documentation
The endpoint IMM polynomial is the sum of its labelled path monomials.
```
theorem imm_eq_sum_path_products (n : ℕ) (hn : 0 < n) :
    imm K n = ((immPaths n hn).map fun p => (p.map (X (R := K))).prod).sum := by
…
```
Mentions: OAI.Problem335.imm, OAI.Problem335.immPaths
theorem OAI.Problem335.mixedOperator_imm_eq_sum_paths line 68
Source documentation
The full IMM polynomial operator is a sum of products of its edge operators.
```
theorem mixedOperator_imm_eq_sum_paths (n : ℕ) (hn : 0 < n)
    (isV : (Fin n × Fin n × Fin n) → Bool) :
    mixedOperator (K := K) isV (imm K n) =
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm
theorem OAI.Problem335.immPaths_nodup line 77
Source documentation
Each individual IMM path contains no repeated variable.
```
theorem immPaths_nodup (n : ℕ) (hn : 0 < n)
    (p : List (Fin n × Fin n × Fin n)) (hp : p ∈ immPaths n hn) : p.Nodup := by
…
```
Mentions: OAI.Problem335.immPaths
theorem OAI.Problem335.mixedOperator_imm_eq_sum_paths_fin line 84
Source documentation
The operator expansion indexed by the finite type of paths.
```
theorem mixedOperator_imm_eq_sum_paths_fin (n : ℕ) (hn : 0 < n)
    (isV : (Fin n × Fin n × Fin n) → Bool) :
    mixedOperator (K := K) isV (imm K n) =
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm

theorem OAI.Problem335.mixedOperator_imm_apply_eq_sum_paths line 96

Source documentation

Applying the IMM operator is the sum of its individual path actions.

theorem mixedOperator_imm_apply_eq_sum_paths (n : ℕ) (hn : 0 < n)
    (isV : (Fin n × Fin n × Fin n) → Bool)
    (f : MvPolynomial (Fin n × Fin n × Fin n) K) :
    mixedOperator isV (imm K n) f =
      ∑ p : Fin (immPaths n hn).length,
        ((((immPaths n hn).get p).map (variableOperator isV)).prod) f := by
…

Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm, OAI.Problem335.immPaths, OAI.Problem335.variableOperator

theorem OAI.Problem335.coeff_mixedOperator_imm_eq_sum_paths line 105

Source documentation

Coefficients of the IMM operator are finite sums of path coefficients.

theorem coeff_mixedOperator_imm_eq_sum_paths (n : ℕ) (hn : 0 < n)
    (isV : (Fin n × Fin n × Fin n) → Bool)
    (f : MvPolynomial (Fin n × Fin n × Fin n) K)
    (d : (Fin n × Fin n × Fin n) →₀ ℕ) :
    (mixedOperator isV (imm K n) f).coeff d =
      ∑ p : Fin (immPaths n hn).length,
        (((((immPaths n hn).get p).map (variableOperator isV)).prod) f).coeff d := by
…

Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm, OAI.Problem335.immPaths, OAI.Problem335.variableOperator

def OAI.Problem335.immInternalPathVertices line 115
Source documentation
Extend internal vertex choices by the two fixed endpoint vertices.
```
def immInternalPathVertices (d : ℕ) (p : Fin d → Fin (d + 1)) :
    Fin (d + 2) → Fin (d + 1) :=
…
```
def OAI.Problem335.immInternalPathEdges line 120
Source documentation
The edge list associated to the tuple of internal vertices.
```
def immInternalPathEdges (d : ℕ) (p : Fin d → Fin (d + 1)) :
    List (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) :=
…
```
theorem OAI.Problem335.immInternalPathVertices_start line 126
theorem OAI.Problem335.immInternalPathVertices_end line 130
theorem OAI.Problem335.immInternalPathVertices_castSucc line 134
theorem OAI.Problem335.immInternalPathVertices_succ line 140
theorem OAI.Problem335.immInternalPathVertices_injective line 147
Source documentation
Extending by endpoints does not identify different internal paths.
```
theorem immInternalPathVertices_injective (d : ℕ) :
    Function.Injective (immInternalPathVertices d) := by
…
```
Mentions: OAI.Problem335.immInternalPathVertices
theorem OAI.Problem335.immInternalPathEdges_labels line 155
Source documentation
The edge list has every layer as its first coordinate, exactly once.
```
theorem immInternalPathEdges_labels (d : ℕ) (p : Fin d → Fin (d + 1)) :
    (immInternalPathEdges d p).map Prod.fst = List.finRange (d + 1) := by
…
```
Mentions: OAI.Problem335.immInternalPathEdges
theorem OAI.Problem335.immInternalPathEdges_nodup line 161
Source documentation
Internal-vertex edge lists have no repeated variable.
```
theorem immInternalPathEdges_nodup (d : ℕ) (p : Fin d → Fin (d + 1)) :
    (immInternalPathEdges d p).Nodup := by
…
```
Mentions: OAI.Problem335.immInternalPathEdges
theorem OAI.Problem335.imm_succ_eq_sum_internal_paths line 168
Source documentation
The IMM expansion using the canonical tuple of internal vertices.
```
theorem imm_succ_eq_sum_internal_paths (d : ℕ) :
    imm K (d + 1) = ∑ p : Fin d → Fin (d + 1),
      ((immInternalPathEdges d p).map (X (R := K))).prod := by
…
```
Mentions: OAI.Problem335.imm, OAI.Problem335.immInternalPathEdges
theorem OAI.Problem335.mixedOperator_imm_succ_eq_sum_internal_paths line 176
Source documentation
The actual IMM operator as a sum over internal vertex tuples.
```
theorem mixedOperator_imm_succ_eq_sum_internal_paths (d : ℕ)
    (isV : (Fin (d + 1) × Fin (d + 1) × Fin (d + 1)) → Bool) :
    mixedOperator (K := K) isV (imm K (d + 1)) =
…
```
Mentions: OAI.Problem335.mixedOperator, OAI.Problem335.imm