OAI/Probability/PosteriorReplicas/Geometry/BaseGeometry.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.PosteriorReplicas.matrixRealMeasurableSpace line 10
  2. instance OAI.PosteriorReplicas.matrixRealBorelSpace line 13
  3. lemma OAI.PosteriorReplicas.measurable_matrix_inv_real line 18
  4. lemma OAI.PosteriorReplicas.continuous_rowGram line 23
  5. lemma OAI.PosteriorReplicas.measurable_liftLabel line 27
  6. lemma OAI.PosteriorReplicas.continuous_liftLabel line 32
  7. lemma OAI.PosteriorReplicas.measurable_kernelComponent line 35
  8. lemma OAI.PosteriorReplicas.liftLabel_eq_pairingLift line 40
  9. lemma OAI.PosteriorReplicas.rowGram_eq_gram line 41
  10. lemma OAI.PosteriorReplicas.kernelComponent_eq_starProjection line 43
  11. lemma OAI.PosteriorReplicas.labels_liftLabel line 49
  12. lemma OAI.PosteriorReplicas.labels_kernelComponent line 52
  13. def OAI.PosteriorReplicas.basePoint line 61
  14. lemma OAI.PosteriorReplicas.measurable_basePoint line 67
  15. lemma OAI.PosteriorReplicas.baseFiber_eq_map line 71
  16. lemma OAI.PosteriorReplicas.measurable_basePoint_fixed line 75
  17. instance OAI.PosteriorReplicas.(instance at line 81) line 81
  18. lemma OAI.PosteriorReplicas.labels_basePoint line 86
  19. lemma OAI.PosteriorReplicas.measurable_parametric_map line 95
  20. lemma OAI.PosteriorReplicas.measurable_baseFiber line 107
  21. def OAI.PosteriorReplicas.baseKernel line 112
  22. instance OAI.PosteriorReplicas.(instance at line 116) line 116
  23. lemma OAI.PosteriorReplicas.measurable_tiltMass line 119