OAI/Probability/PosteriorReplicas/Geometry/BallJacobian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PosteriorReplicas.det_id_add_smulRight line 13
  2. def OAI.PosteriorReplicas.ballStretch line 35
  3. def OAI.PosteriorReplicas.ballStretchDeriv line 37
  4. lemma OAI.PosteriorReplicas.one_sub_norm_sq_pos line 43
  5. lemma OAI.PosteriorReplicas.ballStretch_eq line 48
  6. lemma OAI.PosteriorReplicas.hasFDerivAt_ballStretch line 55
  7. lemma OAI.PosteriorReplicas.det_ballStretchDeriv line 68
  8. lemma OAI.PosteriorReplicas.measurable_ballStretch line 89
  9. lemma OAI.PosteriorReplicas.ballStretch_eq_inv_sqrt line 95
  10. lemma OAI.PosteriorReplicas.one_add_norm_ballStretch_sq line 100
  11. lemma OAI.PosteriorReplicas.ballStretch_weight line 109
  12. lemma OAI.PosteriorReplicas.lintegral_ballStretch line 121