OAI/Probability/PosteriorReplicas/Geometry/SphereSubspace.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PosteriorReplicas.gaussian_orthogonalProjectionOnto line 14
  2. lemma OAI.PosteriorReplicas.gaussian_subspace_map line 27
  3. lemma OAI.PosteriorReplicas.gaussian_subspace_sum line 32
  4. lemma OAI.PosteriorReplicas.subspace_sum_norm_sq line 41
  5. lemma OAI.PosteriorReplicas.normalDirection_pos_smul line 49
  6. lemma OAI.PosteriorReplicas.sphere_subspace_gaussian_integral line 55
  7. lemma OAI.PosteriorReplicas.sphere_subspace_polar_integral line 64
  8. lemma OAI.PosteriorReplicas.radial_subspace_integral line 89
  9. lemma OAI.PosteriorReplicas.scaled_subspace_integral line 106
  10. lemma OAI.PosteriorReplicas.sphere_subspace_slope_integral line 121
  11. lemma OAI.PosteriorReplicas.normalDirection_ballStretch line 139
  12. lemma OAI.PosteriorReplicas.sphere_subspace_surface_integral line 159
  13. lemma OAI.PosteriorReplicas.surface_lintegral_eq_gaussian line 189
  14. lemma OAI.PosteriorReplicas.sphere_subspace_gaussian_fiber_integral line 201
  15. lemma OAI.PosteriorReplicas.sphere_area_ratio line 225