OAI/Probability/GaussianPropeller/Polar.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.Polar.integral_volume_polar line 43
  2. lemma OAI.GaussianPropeller.Polar.integral_stdGaussian_polar line 55
  3. lemma OAI.GaussianPropeller.Polar.integral_volumeIoiPow line 76
  4. lemma OAI.GaussianPropeller.Polar.integral_homogeneous line 90
  5. def OAI.GaussianPropeller.Polar.radial line 117
  6. lemma OAI.GaussianPropeller.Polar.radial_eq line 119
  7. lemma OAI.GaussianPropeller.Polar.radial_integrable line 125
  8. lemma OAI.GaussianPropeller.Polar.radial_pos line 130
  9. lemma OAI.GaussianPropeller.Polar.radial_scale line 135
  10. lemma OAI.GaussianPropeller.Polar.radial_half_zero line 153
  11. lemma OAI.GaussianPropeller.Polar.radial_half_one line 156
  12. lemma OAI.GaussianPropeller.Polar.radial_half_two line 160
  13. lemma OAI.GaussianPropeller.Polar.radial_half_three line 175
  14. lemma OAI.GaussianPropeller.Polar.radial_half_four line 179
  15. lemma OAI.GaussianPropeller.Polar.integral_radial line 196
  16. lemma OAI.GaussianPropeller.Polar.integral_radial_normalized line 210
  17. lemma OAI.GaussianPropeller.Polar.integral_norm_pow_exp line 226
  18. lemma OAI.GaussianPropeller.Polar.integral_norm line 241