OAI/Analysis/BernoulliCone/HarmonicKernel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Bernoulli.HarmonicKernel.profile line 13
  2. def OAI.Bernoulli.HarmonicKernel.kernelProfile line 14
  3. def OAI.Bernoulli.HarmonicKernel.potential line 15
  4. def OAI.Bernoulli.HarmonicKernel.rawKernel line 16
  5. lemma OAI.Bernoulli.HarmonicKernel.contDiff_profile line 18
  6. lemma OAI.Bernoulli.HarmonicKernel.deriv_profile line 21
  7. lemma OAI.Bernoulli.HarmonicKernel.kernelProfile_eq line 31
  8. lemma OAI.Bernoulli.HarmonicKernel.contDiff_kernelProfile line 36
  9. lemma OAI.Bernoulli.HarmonicKernel.profile_zero line 39
  10. lemma OAI.Bernoulli.HarmonicKernel.kernelProfile_zero line 42
  11. lemma OAI.Bernoulli.HarmonicKernel.kernelProfile_nonneg line 45
  12. lemma OAI.Bernoulli.HarmonicKernel.kernelProfile_pos line 49
  13. lemma OAI.Bernoulli.HarmonicKernel.contDiff_rawKernel line 54
  14. lemma OAI.Bernoulli.HarmonicKernel.contDiff_potential line 57
  15. lemma OAI.Bernoulli.HarmonicKernel.rawKernel_zero line 60
  16. lemma OAI.Bernoulli.HarmonicKernel.rawKernel_compact line 65
  17. lemma OAI.Bernoulli.HarmonicKernel.rawKernel_nonneg line 68
  18. lemma OAI.Bernoulli.HarmonicKernel.rawKernel_mass_pos line 70
  19. def OAI.Bernoulli.HarmonicKernel.scaledPotential line 77

    Source documentation

    Compact radial potential centered at a with positive radius r. Its scale derivative produces an averaging kernel by the radial Laplacian.

    def scaledPotential (r : ℝ) (a x : Space d) : ℝ := profile (‖x-a‖^2 / r^2)

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.HarmonicKernel.profile

  20. lemma OAI.Bernoulli.HarmonicKernel.contDiff_scaledPotential line 79
  21. lemma OAI.Bernoulli.HarmonicKernel.scaledPotential_zero line 83
  22. lemma OAI.Bernoulli.HarmonicKernel.scaledPotential_support line 90
  23. lemma OAI.Bernoulli.HarmonicKernel.scaledPotential_test line 97