Chapter BesselHarmonic
DefinitionChapterBesselHarmonicdefinitionsformalizationtimepiece
Formal definitions for the timepiece Lean 4 formalization (source chapter BookProof/ChapterBesselHarmonic.lean): generated def bundle for ChapterBesselHarmonic. See BookProof/ChapterBesselHarmonic.lean for full context.
Definition code
import Definitions.Def_ChapterLaplacianProduct import Definitions.Def_ChapterRadialLaplacian import Definitions.Def_ChapterSphericalBessel import Definitions.Def_ChapterSphericalBesselODE import Mathlib namespace BookProof.ChapterBesselHarmonic end BookProof.ChapterBesselHarmonic
Source