OAI/Probability/ThreeStateClauses/InformationLoss.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Information Loss.

  1. def OAI.ThreeState.TreeClauses.Experiment.multisetKernel line 16
  2. lemma OAI.ThreeState.TreeClauses.Experiment.multisetKernel_zero line 31
  3. lemma OAI.ThreeState.TreeClauses.Experiment.multisetKernel_cons line 34
  4. lemma OAI.ThreeState.TreeClauses.Experiment.multisetKernel_iid line 39
  5. lemma OAI.ThreeState.TreeClauses.Experiment.observationLaw_succ line 59
  6. def OAI.ThreeState.TreeClauses.Experiment.observationExpansion line 69
  7. lemma OAI.ThreeState.TreeClauses.Experiment.observationLaw_degrades line 74
  8. lemma OAI.ThreeState.TreeClauses.Experiment.coord_center_abs_le_two line 105
  9. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_degradation_abs line 111
  10. lemma OAI.ThreeState.TreeClauses.Experiment.discrete_degradation_tv line 145
  11. lemma OAI.ThreeState.TreeClauses.Experiment.advantage_antitone line 158
  12. lemma OAI.ThreeState.TreeClauses.Experiment.advantage_tendsto line 167
  13. lemma OAI.ThreeState.TreeClauses.Experiment.integral_discreteMarginal line 184
  14. lemma OAI.ThreeState.TreeClauses.Experiment.coord_sq_le_tv line 192
  15. lemma OAI.ThreeState.TreeClauses.Experiment.integral_scaled_square line 202
  16. lemma OAI.ThreeState.TreeClauses.Experiment.estimator_tv_lower line 213