OAI/Probability/SKRatio/Quantization/BinNet.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Bins.norm_of_sum_sq_one line 14
2. lemma OAI.SKRatio.Bins.quadratic_vector_difference line 20
3. lemma OAI.SKRatio.Bins.variance_bilinear_difference line 46
4. abbrev OAI.SKRatio.Bins.WeightBox line 68
5. lemma OAI.SKRatio.Bins.binT_le_one line 70
6. def OAI.SKRatio.Bins.binBox line 76
7. lemma OAI.SKRatio.Bins.finiteA_parameter_tolerance line 80
8. theorem OAI.SKRatio.Bins.binForm_finite_net line 99