Project-declaredLean 4.32.0
Deriv gaussian eq phys Hermite mul gaussian
Physlib.deriv_gaussian_eq_physHermite_mul_gaussian
Project documentation
The Physicists Hermite polynomial are defined as polynomials over ā¤ in X recursively with physHermite 0 = 1 and physHermite (n + 1) = 2 ā¢ X * physHermite n - derivative (physHermite n). This polynomial will often be cast as a function ā ā ā by evaluating the polynomial at X. -/ noncomputable def physHermite : ā ā Polynomial ā¤ | 0 => 1 | n + 1...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.