OAI/Probability/FreeIsing/Posterior/FiniteIsingFilteringRepresentation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.FiniteIsingFiltering.State line 17
  2. def OAI.Problem367.FiniteIsingFiltering.signal line 20
  3. lemma OAI.Problem367.FiniteIsingFiltering.measurable_signal line 23
  4. def OAI.Problem367.FiniteIsingFiltering.observationFiltration line 29
  5. lemma OAI.Problem367.FiniteIsingFiltering.observationFiltration_le_signal line 36
  6. lemma OAI.Problem367.FiniteIsingFiltering.observationFiltration_eq_comap line 46
  7. abbrev OAI.Problem367.FiniteIsingFiltering.mean line 57
  8. abbrev OAI.Problem367.FiniteIsingFiltering.covariance line 61
  9. lemma OAI.Problem367.FiniteIsingFiltering.mean_eq_fieldMean line 66
  10. lemma OAI.Problem367.FiniteIsingFiltering.covariance_eq_fieldCovariance line 78
  11. lemma OAI.Problem367.FiniteIsingFiltering.abs_mean_le_one line 90
  12. lemma OAI.Problem367.FiniteIsingFiltering.abs_covariance_le_two line 99
  13. lemma OAI.Problem367.FiniteIsingFiltering.stronglyAdapted_mean line 110
  14. lemma OAI.Problem367.FiniteIsingFiltering.stronglyAdapted_covariance line 130
  15. lemma OAI.Problem367.FiniteIsingFiltering.continuous_mean line 151
  16. lemma OAI.Problem367.FiniteIsingFiltering.continuous_covariance line 162
  17. lemma OAI.Problem367.FiniteIsingFiltering.progressive_mean line 172
  18. lemma OAI.Problem367.FiniteIsingFiltering.progressive_covariance line 179
  19. lemma OAI.Problem367.FiniteIsingFiltering.memLp_mean line 186
  20. lemma OAI.Problem367.FiniteIsingFiltering.memLp_covariance line 196