OAI/Analysis/FiniteFactor/Diffuse/ProjectionTrace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Nonhyperlinear.Diffuseness.projection_vector_trace line 10
2. lemma OAI.Nonhyperlinear.Diffuseness.projection_vector_trace_nonneg line 20
3. lemma OAI.Nonhyperlinear.Diffuseness.projection_difference line 26
4. lemma OAI.Nonhyperlinear.Diffuseness.projection_vector_trace_mono line 38