ImmFiniteMatrix.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.immLayerVCount line 15
Source documentation
The number of derivative layers in a layerwise partition.
```
def immLayerVCount {n : ℕ} (side : Fin n → Bool) : ℕ :=
…
```
def OAI.Problem335.immLayerUCount line 19
Source documentation
The number of multiplication layers in a layerwise partition.
```
def immLayerUCount {n : ℕ} (side : Fin n → Bool) : ℕ :=
…
```
abbrev OAI.Problem335.ImmSourceIndex line 23
Source documentation
Source exponent vectors for the finite IMM operator.
```
abbrev ImmSourceIndex (n : ℕ) (side : Fin n → Bool) (a b : ℕ) :=
…
```
abbrev OAI.Problem335.ImmTargetIndex line 27
Source documentation
Target exponent vectors for the finite IMM operator.
```
abbrev ImmTargetIndex (n : ℕ) (side : Fin n → Bool) (a b : ℕ) :=
…
```
def OAI.Problem335.immNormalizedMatrix line 32
Source documentation
The actual finite IMM map written in factorial-normalized source and target bases.
```
def immNormalizedMatrix (n : ℕ) (side : Fin n → Bool) (a b : ℕ) :
    Matrix (ImmTargetIndex n side a b) (ImmSourceIndex n side a b) ℂ :=
…
```
Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex

theorem OAI.Problem335.immNormalizedMatrix_apply line 42

Source documentation

Each finite normalized matrix entry is exactly the weighted sum of its IMM path shifts.

theorem immNormalizedMatrix_apply (n : ℕ) (hn : 0 < n) (side : Fin n → Bool)
    (a b : ℕ) (e : ImmTargetIndex n side a b) (d : ImmSourceIndex n side a b) :
    immNormalizedMatrix n side a b e d =
      ∑ p : Fin (immPaths n hn).length,
        if immPathOccupation n hn (fun x => side x.1) d.1 p = e.1
        then (immPathAmplitude n hn (fun x => side x.1) d.1 p : ℂ) else 0 := by
…

Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immNormalizedMatrix, OAI.Problem335.immPaths, OAI.Problem335.immPathOccupation, OAI.Problem335.immPathAmplitude

theorem OAI.Problem335.immNormalizedMatrix_rank line 63
Source documentation
The finite normalized matrix computes exactly the manuscript's rank measure.
```
theorem immNormalizedMatrix_rank (n : ℕ) (side : Fin n → Bool) (a b : ℕ) :
    (immNormalizedMatrix n side a b).rank =
      bidegreeRank (fun x => side x.1) a b
        (immLayerVCount side) (immLayerUCount side) (imm ℂ n) := by
…
```
Mentions: OAI.Problem335.immNormalizedMatrix, OAI.Problem335.bidegreeRank, OAI.Problem335.immLayerVCount, OAI.Problem335.immLayerUCount, OAI.Problem335.imm
def OAI.Problem335.immTargetShift line 70
Source documentation
The genuine target occupation, with an irrelevant fallback for zero-amplitude paths.
```
def immTargetShift (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ)
    [Nonempty (ImmTargetIndex n side a b)]
    (d : ImmSourceIndex n side a b) (p : Fin (immPaths n hn).length) :
    ImmTargetIndex n side a b := by
…
```
Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immPaths

theorem OAI.Problem335.immTargetShift_val_of_amplitude_ne_zero line 81

Source documentation

Nonzero paths never use the arbitrary fallback index.

theorem immTargetShift_val_of_amplitude_ne_zero (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (a b : ℕ) [Nonempty (ImmTargetIndex n side a b)]
    (d : ImmSourceIndex n side a b) (p : Fin (immPaths n hn).length)
    (hp : immPathAmplitude n hn (fun x => side x.1) d.1 p ≠ 0) :
    (immTargetShift n hn side a b d p).1 =
      immPathOccupation n hn (fun x => side x.1) d.1 p := by
…

Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immTargetShift, OAI.Problem335.immPathOccupation

theorem OAI.Problem335.immNormalizedMatrix_eq_pathShiftMatrix line 94

Source documentation

The actual normalized IMM matrix is the finite weighted path-shift matrix.

theorem immNormalizedMatrix_eq_pathShiftMatrix (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (a b : ℕ) [Nonempty (ImmTargetIndex n side a b)] :
    immNormalizedMatrix n side a b =
      pathShiftMatrix (immTargetShift n hn side a b)
        (fun d p => (immPathAmplitude n hn (fun x => side x.1) d.1 p : ℂ)) := by
…

Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.immNormalizedMatrix, OAI.Problem335.pathShiftMatrix, OAI.Problem335.immTargetShift, OAI.Problem335.immPathAmplitude

theorem OAI.Problem335.immPathOccupation_injective_of_nonzero line 114

Source documentation

Distinct nonzero path contributions cannot reach the same occupation vector.

theorem immPathOccupation_injective_of_nonzero (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (d : (Fin n × Fin n × Fin n) →₀ ℕ)
    (p q : Fin (immPaths n hn).length)
    (hp : immPathAmplitude n hn (fun x => side x.1) d p ≠ 0)
    (hq : immPathAmplitude n hn (fun x => side x.1) d q ≠ 0)
    (heq : immPathOccupation n hn (fun x => side x.1) d p =
      immPathOccupation n hn (fun x => side x.1) d q) : p = q := by
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immPathOccupation

theorem OAI.Problem335.immTargetShift_collision_zero line 137

Source documentation

Any collision of distinct finite shifts has a zero-amplitude contribution.

theorem immTargetShift_collision_zero (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (a b : ℕ) [Nonempty (ImmTargetIndex n side a b)]
    (d : ImmSourceIndex n side a b) (p q : Fin (immPaths n hn).length)
    (hpq : p ≠ q) (hs : immTargetShift n hn side a b d p =
      immTargetShift n hn side a b d q) :
    immPathAmplitude n hn (fun x => side x.1) d.1 p = 0 ∨
      immPathAmplitude n hn (fun x => side x.1) d.1 q = 0 := by
…

Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immPaths, OAI.Problem335.immTargetShift, OAI.Problem335.immPathAmplitude

theorem OAI.Problem335.immNormalizedMatrix_conjTranspose line 156

Source documentation

All entries of the normalized IMM operator are real, so adjoint equals transpose.

theorem immNormalizedMatrix_conjTranspose (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (a b : ℕ) :
    (immNormalizedMatrix n side a b).conjTranspose =
      (immNormalizedMatrix n side a b).transpose := by
…

Mentions: OAI.Problem335.immNormalizedMatrix

theorem OAI.Problem335.immNormalizedMatrix_first_trace line 170

Source documentation

The first Gram trace of the actual IMM operator is its total path occupation mass.

theorem immNormalizedMatrix_first_trace (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (a b : ℕ) [Nonempty (ImmTargetIndex n side a b)] :
    Matrix.trace ((immNormalizedMatrix n side a b).conjTranspose *
      immNormalizedMatrix n side a b) =
      ∑ d : ImmSourceIndex n side a b, ∑ p : Fin (immPaths n hn).length,
        ((immPathAmplitude n hn (fun x => side x.1) d.1 p) ^ 2 : ℝ) := by
…

Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.immNormalizedMatrix, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude