OAI/Probability/FreeIsing/Ising/ContinuousCopyDensity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingContinuousCopyDensity.response line 16
  2. theorem OAI.Problem367.IsingContinuousCopyDensity.response_progressive line 20
  3. theorem OAI.Problem367.IsingContinuousCopyDensity.response_eq_raw_ae line 28
  4. theorem OAI.Problem367.IsingContinuousCopyDensity.rawObservation_progressive line 40
  5. theorem OAI.Problem367.IsingContinuousCopyDensity.rawPosterior_progressive line 47
  6. theorem OAI.Problem367.IsingContinuousCopyDensity.rawResponse_progressive line 52
  7. def OAI.Problem367.IsingContinuousCopyDensity.continuousDensity line 63
  8. theorem OAI.Problem367.IsingContinuousCopyDensity.continuousDensity_progressive line 69
  9. theorem OAI.Problem367.IsingContinuousCopyDensity.actualDensity_progressive line 78
  10. theorem OAI.Problem367.IsingContinuousCopyDensity.continuousDensity_eq_actual_ae line 95
  11. theorem OAI.Problem367.IsingContinuousCopyDensity.continuousDensity_eq_actual_prod_ae line 114
  12. theorem OAI.Problem367.IsingContinuousCopyDensity.continuousDensity_integrable line 136
  13. theorem OAI.Problem367.IsingContinuousCopyDensity.ae_all_primitive_eq_actual line 145
  14. theorem OAI.Problem367.IsingContinuousCopyDensity.ae_all_stopped_primitive_eq_actual line 156
  15. theorem OAI.Problem367.IsingContinuousCopyDensity.integral_cutoff_density_eq_actual line 169
  16. theorem OAI.Problem367.IsingContinuousCopyDensity.integral_stopDensity_eq_actual line 185
  17. theorem OAI.Problem367.IsingContinuousCopyDensity.integral_integral_stopDensity_eq_actual line 199