OAI/Probability/FreeIsing/Ising/InnovationIndependence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.IsingInnovation.spin_bound line 19
  2. theorem OAI.Problem367.IsingInnovation.innovation_martingale line 27
  3. theorem OAI.Problem367.IsingInnovation.innovation_increment_law_and_indep line 37
  4. theorem OAI.Problem367.IsingInnovation.innovation_increment_indep_filtration line 78
  5. theorem OAI.Problem367.IsingInnovation.innovation_future_indep_filtration line 89
  6. theorem OAI.Problem367.IsingInnovation.innovation_strict_future_indep line 105
  7. def OAI.Problem367.IsingInnovation.uniformObservationFiltration line 124
  8. theorem OAI.Problem367.IsingInnovation.uniformInnovation_future_indep_filtration line 133