ImmFirstTrace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.immRealNormalizedMatrix line 12
Source documentation
The real, nonnegative matrix underlying the actual normalized IMM map.
```
def immRealNormalizedMatrix (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ) :
    Matrix (ImmTargetIndex n side a b) (ImmSourceIndex n side a b) ℝ := by
…
```
Mentions: OAI.Problem335.ImmTargetIndex, OAI.Problem335.ImmSourceIndex
theorem OAI.Problem335.immNormalizedMatrix_eq_map_real line 19

theorem OAI.Problem335.immPathAmplitude_sq_sum_target line 33

Source documentation

Every nonzero path amplitude occurs in exactly one genuine target row. Zero-amplitude paths need no artificial target-row choice.

theorem immPathAmplitude_sq_sum_target (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (a b : ℕ) (d : ImmSourceIndex n side a b)
    (p : Fin (immPaths n hn).length) :
    (∑ e : ImmTargetIndex n side a b,
      (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) ^ 2) =
      immPathAmplitude n hn (fun x => side x.1) d.1 p ^ 2 := by
…

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

theorem OAI.Problem335.immNormalizedMatrix_first_trace_lower line 59
Source documentation
Actual normalized IMM first trace dominates the total occupation mass. Nonnegative coefficients make path-collision analysis unnecessary for this lower bound. All sources and targets are the genuine finite bidegree spaces.
```
theorem immNormalizedMatrix_first_trace_lower (n : ℕ) (hn : 0 < n)
    (side : Fin n → Bool) (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) ≤
      ((immNormalizedMatrix n side a b).conjTranspose *
        immNormalizedMatrix n side a b).trace.re := by
…
```
Mentions: OAI.Problem335.ImmSourceIndex, OAI.Problem335.immPaths, OAI.Problem335.immPathAmplitude, OAI.Problem335.immNormalizedMatrix

theorem OAI.Problem335.immNormalizedMatrix_first_trace_lower_of_average line 92

Source documentation

Uniform actual-source occupation averages lift to the normalized IMM first trace with exactly n^(n-1) endpoint paths.

theorem immNormalizedMatrix_first_trace_lower_of_average
    (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ) (L : ℝ)
    (hmean : ∀ p : Fin (immPaths n hn).length,
      L ≤ (∑ d : ImmSourceIndex n side a b,
        immPathAmplitude n hn (fun x => side x.1) d.1 p ^ 2) /
          (Fintype.card (ImmSourceIndex n side a b) : ℝ)) :
    (Fintype.card (ImmSourceIndex n side a b) : ℝ) * (n : ℝ) ^ (n - 1) * L ≤
      ((immNormalizedMatrix n side a b).conjTranspose *
        immNormalizedMatrix n side a b).trace.re := by
…

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