OAI/Algebra/DepthFive/ImmSecondMomentParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.source_bound line 14
2. theorem OAI.Problem335.immNormalizedMatrix_second_moment_le_relaxed line 55

   Source documentation

   The actual finite IMM second trace is bounded by the relaxed pairing sum, with precisely one source dimension and the square of the path mean.

   theorem immNormalizedMatrix_second_moment_le_relaxed
       (L : ℕ) (side : Fin (L + 1) → Bool)
       [Nonempty {x : Fin (L + 1) × (Fin (L + 1) × Fin (L + 1)) // side x.1 = true}]
       [Nonempty {x : Fin (L + 1) × (Fin (L + 1) × Fin (L + 1)) // ¬ side x.1 = true}]
       (a b : ℕ) (ha : 0 < a) :
       let A := immNormalizedMatrix (L + 1) side a b
   …

   Mentions: OAI.Problem335.immNormalizedMatrix