ActualImmRank.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Identification of the concrete rank measure with the finite normalized matrix used in the IMM trace estimates.

theorem OAI.Problem335.LowerParameters.card_immSourceIndex_eq_rankDimension line 15
theorem OAI.Problem335.LowerParameters.rankData_imm_eq_matrixRank line 26
theorem OAI.Problem335.LowerParameters.configured_imm_first_trace_lower line 35
Source documentation
The configured actual first trace, in the common normalization used by the final rank comparison.
```
theorem configured_imm_first_trace_lower {n : ℕ} (hn : 16 ≤ n) :
    rankDimension n * rankMomentScale n * Real.exp (-(64 * Real.sqrt (n : ℝ))) ≤
      ((immNormalizedMatrix n (balancedLayer (Nat.le_trans (of_decide_eq_true rfl : 4 ≤ 16) hn)) (a n) (b n)).conjTranspose *
        immNormalizedMatrix n (balancedLayer (Nat.le_trans (of_decide_eq_true rfl : 4 ≤ 16) hn)) (a n) (b n)).trace.re := by
…
```
Mentions: OAI.Problem335.LowerParameters.rankDimension, OAI.Problem335.LowerParameters.rankMomentScale, OAI.Problem335.immNormalizedMatrix, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b

theorem OAI.Problem335.LowerParameters.rankData_imm_lower_of_second_trace_bound line 47

Source documentation

After the actual first-moment estimate is discharged, the sole remaining matrix hypothesis for the configured rank lower bound is the second trace.

theorem rankData_imm_lower_of_second_trace_bound {n : ℕ} (hn : 16 ≤ n) (C : ℝ)
    (hsecond :
      (((immNormalizedMatrix n (balancedLayer (Nat.le_trans (of_decide_eq_true rfl : 4 ≤ 16) hn)) (a n) (b n)).conjTranspose *
        immNormalizedMatrix n (balancedLayer (Nat.le_trans (of_decide_eq_true rfl : 4 ≤ 16) hn)) (a n) (b n)) ^ 2).trace.re ≤
        rankDimension n * rankMomentScale n ^ 2 * Real.exp (C * Real.sqrt (n : ℝ))) :
    rankDimension n * Real.exp (-((128 + C) * Real.sqrt (n : ℝ))) ≤
      rankData n (imm ℂ n) := by
…

Mentions: OAI.Problem335.immNormalizedMatrix, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.rankDimension, OAI.Problem335.LowerParameters.rankMomentScale, OAI.Problem335.LowerParameters.rankData, OAI.Problem335.imm