OAI/Probability/GaussianPropeller/Translation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.Translation.map_density_comp line 17
  2. lemma OAI.GaussianPropeller.Translation.product_density line 29
  3. lemma OAI.GaussianPropeller.Translation.pi_gaussian_density line 67
  4. def OAI.GaussianPropeller.Translation.stdDensity line 76
  5. lemma OAI.GaussianPropeller.Translation.measurable_stdDensity line 79
  6. lemma OAI.GaussianPropeller.Translation.stdGaussian_density line 84
  7. lemma OAI.GaussianPropeller.Translation.stdDensity_pos line 95
  8. lemma OAI.GaussianPropeller.Translation.stdDensity_eq line 101
  9. lemma OAI.GaussianPropeller.Translation.stdDensity_add line 111
  10. lemma OAI.GaussianPropeller.Translation.stdGaussian_map_add line 119
  11. lemma OAI.GaussianPropeller.Translation.translated_integral line 138
  12. lemma OAI.GaussianPropeller.Translation.integrable_exp_inner line 150
  13. lemma OAI.GaussianPropeller.Translation.integrableExpSet_neg_inner_restrict line 159
  14. lemma OAI.GaussianPropeller.Translation.translation_derivative line 168