ImmFirstMomentParameters.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.immNormalizedMatrix_first_moment_lower_parameters line 16

Source documentation

The first trace of the actual finite normalized IMM matrix at the canonical occupation parameters. The path-count and geometric scale agree with the second moment normalization; there are no auxiliary matrix-identity hypotheses.

theorem immNormalizedMatrix_first_moment_lower_parameters {n : ℕ} (hn : 16 ≤ n)
    (side : Fin n → Bool) (hk : immLayerVCount side = k n)
    (hm : immLayerUCount side = m n) :
    (Fintype.card (ImmSourceIndex n side (a n) (b n)) : ℝ) *
      ((n : ℝ) ^ (n - 1) *
        (((a n : ℝ) / v n) ^ k n * (1 + (b n : ℝ) / u n) ^ m n)) *
          Real.exp (-64 / Real.sqrt (n : ℝ)) ≤
      ((immNormalizedMatrix n side (a n) (b n)).conjTranspose *
        immNormalizedMatrix n side (a n) (b n)).trace.re := by
…

Mentions: OAI.Problem335.immLayerVCount, OAI.Problem335.immLayerUCount, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immNormalizedMatrix

theorem OAI.Problem335.immNormalizedMatrix_first_moment_lower_sqrt line 41

Source documentation

A weaker square-root-exponential version is convenient for the final rank lower bound, whose constant absorbs both trace losses.

theorem immNormalizedMatrix_first_moment_lower_sqrt {n : ℕ} (hn : 16 ≤ n)
    (side : Fin n → Bool) (hk : immLayerVCount side = k n)
    (hm : immLayerUCount side = m n) :
    (Fintype.card (ImmSourceIndex n side (a n) (b n)) : ℝ) *
      ((n : ℝ) ^ (n - 1) *
        (((a n : ℝ) / v n) ^ k n * (1 + (b n : ℝ) / u n) ^ m n)) *
          Real.exp (-64 * Real.sqrt (n : ℝ)) ≤
      ((immNormalizedMatrix n side (a n) (b n)).conjTranspose *
        immNormalizedMatrix n side (a n) (b n)).trace.re := by
…

Mentions: OAI.Problem335.immLayerVCount, OAI.Problem335.immLayerUCount, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immNormalizedMatrix