OAI/Algebra/DepthFive/ImmCompatibleTrace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.totalImmProfile line 11
2. theorem OAI.Problem335.totalImmProfile_get line 15
3. theorem OAI.Problem335.totalImmProfile_internal line 21
4. theorem OAI.Problem335.immNormalizedMatrix_second_trace_le_compatible line 29

   Source documentation

   The actual second trace is bounded by the compatible endpoint-path local occupation sum, with one source sum and no remaining representation hypotheses.

   theorem immNormalizedMatrix_second_trace_le_compatible
       (d : ℕ) (side : Fin (d + 1) → Bool) (a b : ℕ) :
       let A := immNormalizedMatrix (d + 1) side a b
   …

   Mentions: OAI.Problem335.immNormalizedMatrix