OAI/Probability/CubeShuffle/SchattenBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.WeightedSweep.dimension_pos line 11
2. lemma OAI.CubeShuffle.WeightedSweep.dimension_one_le line 15
3. lemma OAI.CubeShuffle.WeightedSweep.log_dimension_nonneg line 19
4. lemma OAI.CubeShuffle.WeightedSweep.schattenMoment_nonneg line 26
5. lemma OAI.CubeShuffle.WeightedSweep.schattenNorm_rpow line 29
6. lemma OAI.CubeShuffle.WeightedSweep.singularValue_le_norm line 34
7. lemma OAI.CubeShuffle.WeightedSweep.schattenMoment_le line 50