OAI/Probability/SKRatio/Quantization/BinStability.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.siteNorm line 15
  2. lemma OAI.SKRatio.Bins.siteNorm_nonneg line 17
  3. lemma OAI.SKRatio.Bins.siteNorm_sq line 19
  4. lemma OAI.SKRatio.Bins.siteNorm_add line 22
  5. lemma OAI.SKRatio.Bins.siteNorm_le_of_abs_le line 29
  6. lemma OAI.SKRatio.Bins.siteNorm_mul_le line 45
  7. lemma OAI.SKRatio.Bins.siteMoment_abs_le line 60
  8. lemma OAI.SKRatio.Bins.siteMoment_sub line 71
  9. lemma OAI.SKRatio.Bins.siteMoment_one line 75
  10. lemma OAI.SKRatio.Bins.v_abs_le_one line 79
  11. lemma OAI.SKRatio.Bins.siteMoment_v line 81
  12. lemma OAI.SKRatio.Bins.product_error line 85
  13. lemma OAI.SKRatio.Bins.mean_constant_rows line 97
  14. theorem OAI.SKRatio.Bins.correctedForm_field_error line 103