OAI/Probability/SKRatio/Entropy/GaussianHistory.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatio.Observation.History line 13
  2. instance OAI.SKRatio.Observation.History.historyMeasurable line 20
  3. instance OAI.SKRatio.Observation.History.historyTopology line 27
  4. instance OAI.SKRatio.Observation.History.historySecondCountable line 34
  5. instance OAI.SKRatio.Observation.History.historyBorel line 41
  6. def OAI.SKRatio.Observation.History.reference line 48
  7. instance OAI.SKRatio.Observation.History.reference_probability line 52
  8. def OAI.SKRatio.Observation.History.likelihood line 61
  9. lemma OAI.SKRatio.Observation.History.likelihood_pos line 65
  10. lemma OAI.SKRatio.Observation.History.continuous_likelihood line 70
  11. lemma OAI.SKRatio.Observation.History.integrable_likelihood line 76
  12. lemma OAI.SKRatio.Observation.History.integral_likelihood line 83
  13. def OAI.SKRatio.Observation.History.density line 95
  14. lemma OAI.SKRatio.Observation.History.density_pos line 98
  15. lemma OAI.SKRatio.Observation.History.continuous_density line 109
  16. lemma OAI.SKRatio.Observation.History.integrable_density line 112
  17. lemma OAI.SKRatio.Observation.History.integral_density line 116
  18. def OAI.SKRatio.Observation.History.posterior line 123
  19. lemma OAI.SKRatio.Observation.History.density_zero line 128
  20. lemma OAI.SKRatio.Observation.History.posterior_zero line 131
  21. lemma OAI.SKRatio.Observation.History.density_succ line 137
  22. lemma OAI.SKRatio.Observation.History.posterior_succ line 146
  23. lemma OAI.SKRatio.Observation.History.posterior_avg_weight line 156
  24. lemma OAI.SKRatio.Observation.History.integrable_posterior_avg_weight line 163
  25. lemma OAI.SKRatio.Observation.History.integral_posterior_avg_weight line 168
  26. lemma OAI.SKRatio.Observation.History.posterior_mass_pos line 175
  27. lemma OAI.SKRatio.Observation.History.continuous_posterior_mass line 179
  28. lemma OAI.SKRatio.Observation.History.continuous_posterior_entropy line 184
  29. lemma OAI.SKRatio.Observation.History.integrable_posterior_entropy_weight line 188
  30. def OAI.SKRatio.Observation.History.remainingEntropy line 198
  31. lemma OAI.SKRatio.Observation.History.remainingEntropy_zero line 201
  32. lemma OAI.SKRatio.Observation.History.remainingEntropy_succ line 208
  33. lemma OAI.SKRatio.Observation.History.entropy_recurrence line 220
  34. lemma OAI.SKRatio.Observation.History.affine_lower line 246
  35. lemma OAI.SKRatio.Observation.History.exp_neg_two_le line 258
  36. lemma OAI.SKRatio.Observation.History.pow_one_sub_lower line 267
  37. lemma OAI.SKRatio.Observation.History.entropy_retention_mesh line 275
  38. theorem OAI.SKRatio.Observation.History.entropy_of_observation_estimates line 303