OAI/Probability/SKRatio/Gaussian/PlantedEmpirical.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Planted.modelField line 16
  2. lemma OAI.SKRatio.Planted.modelField_measurable line 19
  3. lemma OAI.SKRatio.Planted.fieldLaw_eq_affine_map line 23
  4. lemma OAI.SKRatio.Planted.fieldLaw_secondMoment line 33
  5. lemma OAI.SKRatio.Planted.common_field_convergence line 44
  6. lemma OAI.SKRatio.Planted.modelField_squareTails line 71
  7. lemma OAI.SKRatio.Planted.modelField_empirical line 97
  8. lemma OAI.SKRatio.Planted.augmentedField_event_eq line 145
  9. theorem OAI.SKRatio.Planted.augmentedField_empirical line 156
  10. theorem OAI.SKRatio.Planted.augmentedField_squareTails line 170
  11. theorem OAI.SKRatio.Planted.augmentedField_secondMoment line 182