OAI/Probability/PosteriorReplicas/Measures/GaussianDifferentiation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PosteriorReplicas.radialLevel line 14
  2. def OAI.PosteriorReplicas.radialWeight line 17
  3. lemma OAI.PosteriorReplicas.exp_norm_level_ball line 23
  4. lemma OAI.PosteriorReplicas.exp_norm_level_empty line 45
  5. lemma OAI.PosteriorReplicas.radialLevel_ball line 55
  6. lemma OAI.PosteriorReplicas.radialLevel_empty line 59
  7. lemma OAI.PosteriorReplicas.measurable_radialWeight line 63
  8. lemma OAI.PosteriorReplicas.lintegral_radialWeight line 70
  9. lemma OAI.PosteriorReplicas.radialWeight_ne_top line 88
  10. def OAI.PosteriorReplicas.scaledRadial line 96
  11. lemma OAI.PosteriorReplicas.scaled_level_ratio line 100
  12. lemma OAI.PosteriorReplicas.tendsto_scaledRadial_at_ball_point line 126