OAI/Geometry/ProjectionBodies/GaussianMeasures.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PettyProjection.gaussianRadial line 12

    Source documentation

    The actual one-dimensional radial Gaussian moment.

    def gaussianRadial (d : ℕ) : ℝ := ∫ r in Ioi (0:ℝ),r^d*Real.exp (-(r^2))
  2. lemma OAI.PettyProjection.gaussianRadial_eq line 14
  3. lemma OAI.PettyProjection.gaussianRadial_pos line 18
  4. lemma OAI.PettyProjection.gaussianRadial_add_two line 22
  5. lemma OAI.PettyProjection.integral_radial_gaussian line 29
  6. lemma OAI.PettyProjection.surface_integral_eq_mean line 42
  7. lemma OAI.PettyProjection.homogeneous_gaussian_integral line 51

    Source documentation

    Polar separation for any positively homogeneous integrand. No smoothness or differentiability is used, and the Bochner integral has its ordinary meaning.

    lemma homogeneous_gaussian_integral {n : ℕ} [NeZero n] (k : ℕ) (f : Space n → ℝ)
    (hh : ∀ r : ℝ,0<r → ∀ x,f (r • x)=r^k*f x) :
    (∫ x,f x*Real.exp (-(‖x‖^2)))=
      (n:ℝ)*kappa n*mean (fun u : Sphere n => f u)*gaussianRadial (n-1+k) := by
…

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.kappa, OAI.PettyProjection.gaussianRadial

  8. lemma OAI.PettyProjection.norm_integrable_map line 87
  9. lemma OAI.PettyProjection.cosine_map line 94
  10. lemma OAI.PettyProjection.adjoint_ne_zero_on_range line 103
  11. lemma OAI.PettyProjection.cosine_map_pos line 113
  12. lemma OAI.PettyProjection.functional_map line 122
  13. lemma OAI.PettyProjection.cosine_map_projection line 127
  14. lemma OAI.PettyProjection.functional_map_continuous line 141
  15. def OAI.PettyProjection.projectedUnit line 180
  16. lemma OAI.PettyProjection.projectedUnit_sub line 183
  17. lemma OAI.PettyProjection.projectedUnit_convex line 189
  18. lemma OAI.PettyProjection.projectedUnit_balanced line 192
  19. lemma OAI.PettyProjection.projectedUnit_inner line 200
  20. lemma OAI.PettyProjection.projectedUnit_compact line 207
  21. def OAI.PettyProjection.RelativeGauge.project line 220
  22. lemma OAI.PettyProjection.RelativeGauge.project_body line 225
  23. lemma OAI.PettyProjection.RelativeGauge.project_le line 230
  24. lemma OAI.PettyProjection.RelativeGauge.support_cylinder_bound line 239