OAI/Probability/BinarySweep/FiniteLaws/MomentBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.conditionalOperator_apply line 12
2. theorem OAI.BinaryCoordinateSweeps.conditionalOperator_norm_le_one line 26
3. theorem OAI.BinaryCoordinateSweeps.traceMoment_le_dimension line 57
4. lemma OAI.BinaryCoordinateSweeps.logMoment_traceMoment_le_log_dimension line 93
5. theorem OAI.BinaryCoordinateSweeps.conditional_moment_of_automatic_regime line 108