OAI/Probability/GaussianPropeller/CellBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.Reduction.winning_inner_nonneg line 33
2. lemma OAI.GaussianPropeller.Reduction.active_probability_mem line 42
3. lemma OAI.GaussianPropeller.Reduction.p_eq_Φ_neg line 67
4. lemma OAI.GaussianPropeller.Reduction.loss_eq_quantile line 73
5. lemma OAI.GaussianPropeller.Reduction.loss_rationalize line 81
6. lemma OAI.GaussianPropeller.Reduction.minimal_loss_constraint line 96
7. lemma OAI.GaussianPropeller.Reduction.minimal_universal_loss line 134
8. lemma OAI.GaussianPropeller.Reduction.minimal_linear_quadratic line 150