OAI/Probability/FreeIsing/Stochastic/FiniteObservationFiltrationLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.FiniteIsingFiltering.observationFiltration_mono_of_subset line 16
2. theorem OAI.Problem367.FiniteIsingFiltering.observationFiltration_le_arrayObservationFiltration line 26
3. theorem OAI.Problem367.FiniteIsingFiltering.observationFiltration_monotone line 37
4. theorem OAI.Problem367.FiniteIsingFiltering.observationFiltration_time_monotone line 43
5. theorem OAI.Problem367.FiniteIsingFiltering.iSup_observationFiltration_eq_arrayObservationFiltration line 49