OAI/Probability/GaussianReplacement/ConditionalLaw.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.dependentMapKernel line 13

    Also declared: ComparatorChallenges/GaussianReplacement.lean:346 (same declaration text).

  2. lemma OAI.CurrentProjection.dependentMapKernel_markov line 17
  3. lemma OAI.CurrentProjection.dependentMapKernel_apply line 22
  4. lemma OAI.CurrentProjection.compProd_dependentMapKernel line 29
  5. lemma OAI.CurrentProjection.compProd_conditional_prod_swap line 44
  6. def OAI.CurrentProjection.scalarProjectionKernel line 59
  7. instance OAI.CurrentProjection.scalarProjectionKernel_markov line 64
  8. lemma OAI.CurrentProjection.scalarProjectionKernel_apply line 68
  9. def OAI.CurrentProjection.scalarObservation line 73
  10. lemma OAI.CurrentProjection.measurable_scalarObservation line 76
  11. def OAI.CurrentProjection.scalarObservationLaw line 79
  12. instance OAI.CurrentProjection.scalarObservationLaw_probability line 83
  13. lemma OAI.CurrentProjection.scalarObservationLaw_disintegrate line 88
  14. lemma OAI.CurrentProjection.scalarObservationLaw_fst line 97
  15. lemma OAI.CurrentProjection.scalarCube_projection line 102
  16. lemma OAI.CurrentProjection.scalarObservationLaw_kernel_ac line 111
  17. lemma OAI.CurrentProjection.scalarObservationLaw_density line 126
  18. lemma OAI.CurrentProjection.scalarObservationLaw_ae_limit line 134
  19. lemma OAI.CurrentProjection.prod_map_swap23 line 148
  20. def OAI.CurrentProjection.residualLabelObservation line 163
  21. lemma OAI.CurrentProjection.measurable_residualLabelObservation line 167
  22. def OAI.CurrentProjection.residualLabelLaw line 172
  23. instance OAI.CurrentProjection.residualLabelLaw_probability line 177
  24. lemma OAI.CurrentProjection.residualLabelLaw_fresh line 183
  25. lemma OAI.CurrentProjection.klDiv_prod_same line 199
  26. lemma OAI.CurrentProjection.residualLabelLaw_kl_le line 205
  27. def OAI.CurrentProjection.residualExact line 213
  28. lemma OAI.CurrentProjection.measurable_residualExact line 220
  29. lemma OAI.CurrentProjection.residualExact_finite line 227
  30. lemma OAI.CurrentProjection.residualCube_ae_limit_actual line 233
  31. lemma OAI.CurrentProjection.residualCube_log_bound line 253
  32. lemma OAI.CurrentProjection.residualExact_log_bound line 271
  33. lemma OAI.CurrentProjection.klDiv_map_bound_of_llr_le line 297
  34. lemma OAI.CurrentProjection.klDiv_map_cross_bound line 324
  35. lemma OAI.CurrentProjection.residualSignalLaw line 350
  36. lemma OAI.CurrentProjection.density_positive_ae line 361
  37. lemma OAI.CurrentProjection.log_le_log_scale_add line 370
  38. def OAI.CurrentProjection.hybridRowConstant line 380
  39. lemma OAI.CurrentProjection.residual_reference_bound line 382