OAI/Probability/SKRatio/Quantization/BinProjected.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Planted.fieldProjection_apply line 15
  2. lemma OAI.SKRatio.Planted.fieldProjection_symmetric line 22
  3. lemma OAI.SKRatio.Planted.fieldProjection_mulVec line 26
  4. lemma OAI.SKRatio.Planted.fieldProjection_vecMul line 34
  5. lemma OAI.SKRatio.Planted.projected_bilinear line 38
  6. lemma OAI.SKRatio.Planted.fullCoeff_goe line 44
  7. lemma OAI.SKRatio.Planted.weightedForm_variance_bilinear line 72
  8. def OAI.SKRatio.Planted.rankForm line 84
  9. lemma OAI.SKRatio.Planted.rank_form_expansion line 88
  10. def OAI.SKRatio.Planted.deterministicForm line 114
  11. theorem OAI.SKRatio.Planted.reducedForm_decomposition line 120
  12. lemma OAI.SKRatio.Bins.inl_array_hasLaw line 159
  13. def OAI.SKRatio.Bins.projectedSup line 165
  14. lemma OAI.SKRatio.Bins.projectedSup_eq line 171
  15. lemma OAI.SKRatio.Bins.projectedSup_continuous line 181
  16. lemma OAI.SKRatio.Bins.le_projectedSup line 196
  17. theorem OAI.SKRatio.Bins.projectedSup_tail line 204