OAI/Probability/SKRatio/Quantization/BinForm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.siteMoment line 14
  2. lemma OAI.SKRatio.Bins.siteMoment_bin line 16
  3. lemma OAI.SKRatio.Bins.momentProduct line 21
  4. def OAI.SKRatio.Bins.correctedForm line 26
  5. lemma OAI.SKRatio.Bins.deterministic_corrected line 34
  6. lemma OAI.SKRatio.Bins.diagonalForm_bin line 42
  7. lemma OAI.SKRatio.Bins.weightedForm_bin line 69
  8. theorem OAI.SKRatio.Bins.correctedForm_bin line 97