OAI/Probability/SKRatio/Quantization/BinGaussian.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatio.Bins.Coordinates line 16
  2. def OAI.SKRatio.Bins.radicalSq line 18
  3. lemma OAI.SKRatio.Bins.radicalSq_nonneg line 22
  4. def OAI.SKRatio.Bins.residualCoeff line 26
  5. def OAI.SKRatio.Bins.comparisonCoeff line 30
  6. lemma OAI.SKRatio.Bins.coeff_orthogonal line 36
  7. lemma OAI.SKRatio.Bins.comparisonCoeff_increment line 42
  8. lemma OAI.SKRatio.Bins.coeff_increment_le line 67
  9. lemma OAI.SKRatio.Bins.continuous_residualCoeff line 88
  10. lemma OAI.SKRatio.Bins.continuous_comparisonCoeff line 99
  11. def OAI.SKRatio.Bins.blockNorm line 107
  12. lemma OAI.SKRatio.Bins.blockNorm_memLp line 111
  13. lemma OAI.SKRatio.Bins.blockNorm_mean_le line 121
  14. lemma OAI.SKRatio.Bins.comparison_pointwise line 141
  15. theorem OAI.SKRatio.Bins.residual_sup_expectation_le line 169