OAI/Dynamics/TriangleBilliards/SpatialSmoothing.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Euclidean radial smoothing in local charts, used to construct the global operator on the triangular double.

  1. def OAI.TriangularBilliards.SpatialSmoothing.raw line 21

    Source documentation

    An explicit smooth radial bump. It is one on the half-unit disk, positive in the unit disk and zero outside it.

    def raw (x : ℂ) : ℝ := (ContDiffBumpBase.ofInnerProductSpace ℂ).toFun 2 ((2 : ℝ) • x)
  2. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_nonneg line 23
  3. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_le_one line 26
  4. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_radial line 29
  5. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_neg line 32
  6. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_contDiff line 34
  7. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_support line 44
  8. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_hasCompactSupport line 52
  9. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_integrable line 56
  10. lemma OAI.TriangularBilliards.SpatialSmoothing.raw_integral_pos line 59
  11. def OAI.TriangularBilliards.SpatialSmoothing.rho line 65

    Source documentation

    The chosen radial mollifier of unit mass.

    def rho (x : ℂ) : ℝ := raw x / ∫ y : ℂ, raw y

    Mentions: OAI.TriangularBilliards.SpatialSmoothing.raw

  12. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_nonneg line 67
  13. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_radial line 69
  14. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_neg line 72
  15. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_contDiff line 74
  16. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_support line 76
  17. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_hasCompactSupport line 80
  18. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_integrable line 84
  19. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_integral line 86
  20. def OAI.TriangularBilliards.SpatialSmoothing.kernel line 92

    Source documentation

    Exact two-dimensional rescaling ε⁻² ρ(x/ε).

    def kernel (ε : ℝ) (x : ℂ) : ℝ := (ε ^ 2)⁻¹ * rho (ε⁻¹ • x)

    Mentions: OAI.TriangularBilliards.SpatialSmoothing.rho

  21. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_nonneg line 94
  22. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_radial line 97
  23. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_neg line 101
  24. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_contDiff line 104
  25. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_support line 108
  26. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_hasCompactSupport line 119
  27. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_integrable line 123
  28. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_integral line 126
  29. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_fderiv line 134

    Source documentation

    The actual first-derivative kernel, with its exact dimensional scaling.

    lemma kernel_fderiv (ε : ℝ) (x : ℂ) :
    fderiv ℝ (kernel ε) x = (ε ^ 3)⁻¹ • fderiv ℝ rho (ε⁻¹ • x) := by
…

    Mentions: OAI.TriangularBilliards.SpatialSmoothing.kernel, OAI.TriangularBilliards.SpatialSmoothing.rho

  30. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_fderiv_integrable line 147
  31. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_fderiv_integrable line 151
  32. def OAI.TriangularBilliards.SpatialSmoothing.derivativeMass line 156
  33. lemma OAI.TriangularBilliards.SpatialSmoothing.derivativeMass_nonneg line 158
  34. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_derivative_mass line 160
  35. lemma OAI.TriangularBilliards.SpatialSmoothing.kernel_derivative_lintegral line 168