OAI/Analysis/FiniteFactor/Diffuse/SupportLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Nonhyperlinear.Diffuseness.one_sub_star_mul_contraction line 11
2. lemma OAI.Nonhyperlinear.Diffuseness.rangeSupport_eq_one_sub_kernel line 31
3. lemma OAI.Nonhyperlinear.Diffuseness.cesaro_star_mul_tendsto line 38