OAI/Probability/SKRatio/Variational/ScalarTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Bins.variance_bilinear_field_error line 20
2. lemma OAI.SKRatio.Bins.deterministic_corrected_error line 43
3. lemma OAI.SKRatio.Bins.quantized_siteNorm_le line 55
4. theorem OAI.SKRatio.Bins.reducedForm_upper_rare line 68
5. theorem OAI.SKRatio.Planted.formBad_rare_of_scalar line 168
6. theorem OAI.SKRatio.Planted.ratio_cutoff_of_scalar line 196