OAI/Probability/SKGap/Posterior/BufferedPosteriorDirection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGapCutoff.Recipe.buffered_root_posterior_direction line 14
2. lemma OAI.SKGapCutoff.Static.posterior_vectorNorm_le_of_unit_dot line 105
3. def OAI.SKGapCutoff.Static.centeredSpinCovariance line 125
4. lemma OAI.SKGapCutoff.Static.centeredSpinCovariance_eq line 128
5. lemma OAI.SKGapCutoff.Static.weak_direction_center line 139