OAI/Probability/FreeIsing/Brownian/ArrayObservation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.arrayNaturalFiltration line 13
  2. lemma OAI.Problem367.arrayNaturalFiltration_eq_comap line 22
  3. lemma OAI.Problem367.arrayNaturalFiltration_stronglyAdapted line 29
  4. lemma OAI.Problem367.arrayNaturalFiltration_le line 40
  5. def OAI.Problem367.signalArrayFiltration line 48
  6. lemma OAI.Problem367.signalArrayFiltration_eq_comap line 56
  7. theorem OAI.Problem367.planted_array_increments_indep_signal_past line 69
  8. lemma OAI.Problem367.planted_noise_coordinate_measurePreserving line 90
  9. theorem OAI.Problem367.preBrownian_martingale_signalArrayFiltration line 102
  10. def OAI.Problem367.plantedArrayObservation line 143
  11. lemma OAI.Problem367.plantedArrayObservation_measurable line 148
  12. def OAI.Problem367.arrayObservationFiltration line 156
  13. lemma OAI.Problem367.arrayObservationFiltration_le_signalArrayFiltration line 164
  14. theorem OAI.Problem367.preBrownian_array_observation_innovation_martingale line 183