OAI/Probability/SKRatio/Quantization/BinPartition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.binMass line 14
  2. def OAI.SKRatio.Bins.massRoot line 16
  3. def OAI.SKRatio.Bins.pullback line 18
  4. lemma OAI.SKRatio.Bins.integral_finite_partition line 21
  5. lemma OAI.SKRatio.Bins.binMass_nonneg line 31
  6. lemma OAI.SKRatio.Bins.massRoot_sq line 34
  7. lemma OAI.SKRatio.Bins.sum_binMass line 37
  8. lemma OAI.SKRatio.Bins.massRoot_unit line 41
  9. lemma OAI.SKRatio.Bins.measurable_finite_comp line 45
  10. lemma OAI.SKRatio.Bins.memLp_finite_comp line 48
  11. lemma OAI.SKRatio.Bins.measurable_pullback line 56
  12. lemma OAI.SKRatio.Bins.memLp_pullback line 59
  13. lemma OAI.SKRatio.Bins.massRoot_pos line 63
  14. lemma OAI.SKRatio.Bins.integral_pullback line 66
  15. lemma OAI.SKRatio.Bins.integral_pullback_energy line 79
  16. lemma OAI.SKRatio.Bins.pullback_normalized line 91