OAI/Analysis/FiniteFactor/Diffuse/OperatorCesaro.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Nonhyperlinear.Diffuseness.cesaro line 19

   Source documentation

   Cesàro means of the powers of a bounded operator.

   def cesaro (S : H →L[ℂ] H) (n : ℕ) : H →L[ℂ] H :=
   …

2. lemma OAI.Nonhyperlinear.Diffuseness.pow_norm_le_one line 23
3. lemma OAI.Nonhyperlinear.Diffuseness.cesaro_norm_le_one line 35
4. lemma OAI.Nonhyperlinear.Diffuseness.cesaro_apply_norm_le line 46
5. lemma OAI.Nonhyperlinear.Diffuseness.cesaro_mul_sub line 51
6. lemma OAI.Nonhyperlinear.Diffuseness.cesaro_range_bound line 55
7. lemma OAI.Nonhyperlinear.Diffuseness.cesaro_on_range line 68