OAI/Analysis/MarkovType/FiniteConditionalAverage.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FiniteLaw.fiberWeight line 15
  2. def OAI.MarkovSuperreflexivity.FiniteLaw.fiberMass line 18
  3. def OAI.MarkovSuperreflexivity.FiniteLaw.normalizedFiberWeight line 21
  4. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberWeight_nonneg line 24
  5. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberMass_nonneg line 30
  6. theorem OAI.MarkovSuperreflexivity.FiniteLaw.mass_le_fiberMass line 34
  7. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberMass_pos_of_mass_pos line 43
  8. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberWeight_eq_zero_of_fiberMass_eq_zero line 47
  9. theorem OAI.MarkovSuperreflexivity.FiniteLaw.normalizedFiberWeight_nonneg line 54
  10. theorem OAI.MarkovSuperreflexivity.FiniteLaw.sum_normalizedFiberWeight line 59
  11. def OAI.MarkovSuperreflexivity.FiniteLaw.fiberSum line 70
  12. def OAI.MarkovSuperreflexivity.FiniteLaw.conditionalMean line 73
  13. def OAI.MarkovSuperreflexivity.FiniteLaw.conditionalAverage line 76
  14. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberSum_eq_zero_of_fiberMass_eq_zero line 79
  15. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalMean_eq_zero_of_fiberMass_eq_zero line 86
  16. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalMean_eq_sum_normalizedFiberWeight line 91
  17. theorem OAI.MarkovSuperreflexivity.FiniteLaw.mass_smul_conditionalMean line 96
  18. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalAverage_eq_of_key_eq line 103
  19. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberSum_key line 108
  20. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalMean_key line 115
  21. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalAverage_key_of_mass_pos line 120
  22. theorem OAI.MarkovSuperreflexivity.FiniteLaw.mass_smul_conditionalAverage_key line 125
  23. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberSum_eq_vexpect_indicator line 134
  24. theorem OAI.MarkovSuperreflexivity.FiniteLaw.sum_fiberSum line 144
  25. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_key line 152
  26. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_key_smul line 161
  27. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_key_smul_eq_zero line 171
  28. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_key_indicator_eq_zero line 177
  29. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_conditionalAverage line 184
  30. theorem OAI.MarkovSuperreflexivity.FiniteLaw.vexpect_key_smul_conditionalAverage line 191
  31. theorem OAI.MarkovSuperreflexivity.FiniteLaw.fiberSum_conditionalAverage_comp line 203
  32. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalAverage_tower line 212
  33. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_pair_key_right line 225
  34. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_pair_key_left line 235
  35. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_pair_conditionalAverage line 245
  36. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_conditionalAverage line 258
  37. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalMean_norm_rpow_le line 265
  38. theorem OAI.MarkovSuperreflexivity.FiniteLaw.conditionalAverage_norm_rpow_le line 280
  39. theorem OAI.MarkovSuperreflexivity.FiniteLaw.expect_norm_conditionalAverage_rpow_le line 286