OAI/Probability/GaussianReplacement/FiberConditional.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.posterior_weight_integral line 17
  2. lemma OAI.CurrentProjection.posterior_weighted_fst line 28
  3. def OAI.CurrentProjection.sphericalPosteriorWeight line 44
  4. lemma OAI.CurrentProjection.measurable_sphericalPosteriorWeight line 47
  5. lemma OAI.CurrentProjection.fiberObservationLaw_fst line 51
  6. lemma OAI.CurrentProjection.fiberObservationLaw_weighted_fst line 57
  7. lemma OAI.CurrentProjection.sphericalPosterior_density line 77
  8. def OAI.CurrentProjection.fiberBilinearTest line 100
  9. lemma OAI.CurrentProjection.measurable_fiberBilinearTest line 104
  10. lemma OAI.CurrentProjection.fiberLeft_bilinear line 110
  11. lemma OAI.CurrentProjection.fiberLeft_bilinear_comm line 165
  12. lemma OAI.CurrentProjection.fiberLeft_quadratic line 175
  13. lemma OAI.CurrentProjection.measurable_perpendicularRowsMap line 217
  14. instance OAI.CurrentProjection.perpendicularRowsKernel_markov line 223
  15. lemma OAI.CurrentProjection.perpendicularRow_neg line 226
  16. lemma OAI.CurrentProjection.fiberPerpendicularTest_swap line 229
  17. lemma OAI.CurrentProjection.fiberPairInverse_swap line 236
  18. lemma OAI.CurrentProjection.measurable_fiberDistanceWeight line 240
  19. lemma OAI.CurrentProjection.fiberDistanceWeight_eq line 244
  20. lemma OAI.CurrentProjection.fiberDistanceWeight_ae line 251
  21. lemma OAI.CurrentProjection.perpendicularRowsKernel_lintegral line 258
  22. lemma OAI.CurrentProjection.fiberRight_bilinear line 272
  23. lemma OAI.CurrentProjection.fiberRight_bilinear_comm line 308
  24. lemma OAI.CurrentProjection.fiberRight_quadratic line 326
  25. lemma OAI.CurrentProjection.fiberRight_finite line 341
  26. lemma OAI.CurrentProjection.fiber_quadratic_eq line 350