PhysHermite

📁 Source: PhysLean/Mathematics/SpecialFunctions/PhysHermite.lean

Statistics

Metric	Count
Definitions `instCoeFunPolynomialIntForallReal_physLean`, `physHermite`	2
Theorems `coeff_physHermite_of_lt`, `coeff_physHermite_self_succ`, `coeff_physHermite_succ_succ`, `coeff_physHhermite_succ_zero`, `cos_mem_physHermite_span_topologicalClosure`, `degree_physHermite`, `deriv_gaussian_eq_physHermite_mul_gaussian`, `deriv_physHermite`, `deriv_physHermite'`, `deriv_physHermite_differentiableAt`, `derivative_physHermite`, `derivative_physHermite_succ`, `fderiv_physHermite`, `guassian_integrable_polynomial`, `guassian_integrable_polynomial_cons`, `integral_physHermite_mul_physHermite_eq_integral_deriv`, `integral_physHermite_mul_physHermite_eq_integral_deriv_exp`, `integral_physHermite_mul_physHermite_eq_integral_deriv_inductive`, `iterate_derivative_physHermite_of_gt`, `iterate_derivative_physHermite_self`, `iterated_deriv_physHermite_eq_aeval`, `natDegree_physHermite`, `physHermite_differentiableAt`, `physHermite_eq_aeval`, `physHermite_eq_deriv_gaussian`, `physHermite_eq_deriv_gaussian'`, `physHermite_eq_iterate`, `physHermite_gaussian_integrable`, `physHermite_leadingCoeff`, `physHermite_ne_zero`, `physHermite_norm`, `physHermite_norm_cons`, `physHermite_one`, `physHermite_orthogonal`, `physHermite_orthogonal_cons`, `physHermite_orthogonal_lt`, `physHermite_parity`, `physHermite_pow`, `physHermite_succ`, `physHermite_succ'`, `physHermite_succ_fun`, `physHermite_succ_fun'`, `physHermite_zero`, `physHermite_zero_apply`, `polynomial_mem_physHermite_span`, `polynomial_mem_physHermite_span_induction`	46
Total	48

PhysLean

Definitions

Name	Category	Theorems
`instCoeFunPolynomialIntForallReal_physLean` 📖	CompOp	—
`physHermite` 📖	CompOp	30 math math: `deriv_physHermite_differentiableAt`, `physHermite_pow`, `degree_physHermite`, `physHermite_eq_iterate`, `integral_physHermite_mul_physHermite_eq_integral_deriv`, `physHermite_eq_aeval`, `integral_physHermite_mul_physHermite_eq_integral_deriv_inductive`, `physHermite_succ'`, `coeff_physHermite_of_lt`, `physHermite_zero`, `coeff_physHermite_self_succ`, `coeff_physHermite_succ_succ`, `polynomial_mem_physHermite_span`, `physHermite_succ_fun'`, `physHermite_succ`, `iterated_deriv_physHermite_eq_aeval`, `iterate_derivative_physHermite_self`, `iterate_derivative_physHermite_of_gt`, `physHermite_leadingCoeff`, `derivative_physHermite_succ`, `physHermite_gaussian_integrable`, `derivative_physHermite`, `coeff_physHhermite_succ_zero`, `deriv_physHermite`, `physHermite_differentiableAt`, `physHermite_succ_fun`, `natDegree_physHermite`, `polynomial_mem_physHermite_span_induction`, `physHermite_one`, `cos_mem_physHermite_span_topologicalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_physHermite_of_lt` 📖	mathematical	—	`physHermite`	—	`coeff_physHermite_succ_succ`
`coeff_physHermite_self_succ` 📖	mathematical	—	`physHermite`	—	`coeff_physHermite_succ_succ` `coeff_physHermite_of_lt`
`coeff_physHermite_succ_succ` 📖	mathematical	—	`physHermite`	—	`physHermite_succ`
`coeff_physHhermite_succ_zero` 📖	mathematical	—	`physHermite`	—	`physHermite_succ`
`cos_mem_physHermite_span_topologicalClosure` 📖	mathematical	—	`physHermite`	—	`polynomial_mem_physHermite_span`
`degree_physHermite` 📖	mathematical	—	`physHermite`	—	`coeff_physHermite_of_lt` `coeff_physHermite_self_succ`
`deriv_gaussian_eq_physHermite_mul_gaussian` 📖	—	—	—	—	`physHermite_zero_apply` `physHermite_succ` `derivative_physHermite`
`deriv_physHermite` 📖	mathematical	—	`physHermite`	—	`derivative_physHermite`
`deriv_physHermite'` 📖	—	—	—	—	`fderiv_physHermite`
`deriv_physHermite_differentiableAt` 📖	mathematical	—	`physHermite`	—	`iterated_deriv_physHermite_eq_aeval`
`derivative_physHermite` 📖	mathematical	—	`physHermite`	—	`derivative_physHermite_succ`
`derivative_physHermite_succ` 📖	mathematical	—	`physHermite`	—	`physHermite_one` `physHermite_succ`
`fderiv_physHermite` 📖	—	—	—	—	`physHermite_differentiableAt` `derivative_physHermite`
`guassian_integrable_polynomial` 📖	—	—	—	—	—
`guassian_integrable_polynomial_cons` 📖	—	—	—	—	—
`integral_physHermite_mul_physHermite_eq_integral_deriv` 📖	mathematical	—	`physHermite`	—	`integral_physHermite_mul_physHermite_eq_integral_deriv_inductive`
`integral_physHermite_mul_physHermite_eq_integral_deriv_exp` 📖	—	—	—	—	`physHermite_eq_deriv_gaussian'`
`integral_physHermite_mul_physHermite_eq_integral_deriv_inductive` 📖	mathematical	—	`physHermite`	—	`integral_physHermite_mul_physHermite_eq_integral_deriv_exp` `deriv_physHermite_differentiableAt` `deriv_gaussian_eq_physHermite_mul_gaussian` `physHermite_differentiableAt` `physHermite_gaussian_integrable`
`iterate_derivative_physHermite_of_gt` 📖	mathematical	—	`physHermite`	—	`natDegree_physHermite`
`iterate_derivative_physHermite_self` 📖	mathematical	—	`physHermite`	—	`coeff_physHermite_self_succ` `coeff_physHermite_of_lt`
`iterated_deriv_physHermite_eq_aeval` 📖	mathematical	—	`physHermite`	—	—
`natDegree_physHermite` 📖	mathematical	—	`physHermite`	—	`degree_physHermite`
`physHermite_differentiableAt` 📖	mathematical	—	`physHermite`	—	—
`physHermite_eq_aeval` 📖	mathematical	—	`physHermite`	—	—
`physHermite_eq_deriv_gaussian` 📖	—	—	—	—	`deriv_gaussian_eq_physHermite_mul_gaussian`
`physHermite_eq_deriv_gaussian'` 📖	—	—	—	—	`physHermite_eq_deriv_gaussian`
`physHermite_eq_iterate` 📖	mathematical	—	`physHermite`	—	`physHermite_succ`
`physHermite_gaussian_integrable` 📖	mathematical	—	`physHermite`	—	`deriv_gaussian_eq_physHermite_mul_gaussian` `iterated_deriv_physHermite_eq_aeval` `guassian_integrable_polynomial`
`physHermite_leadingCoeff` 📖	mathematical	—	`physHermite`	—	`natDegree_physHermite` `coeff_physHermite_self_succ`
`physHermite_ne_zero` 📖	—	—	—	—	`physHermite_leadingCoeff`
`physHermite_norm` 📖	—	—	—	—	`integral_physHermite_mul_physHermite_eq_integral_deriv` `iterated_deriv_physHermite_eq_aeval` `iterate_derivative_physHermite_self`
`physHermite_norm_cons` 📖	—	—	—	—	`physHermite_norm`
`physHermite_one` 📖	mathematical	—	`physHermite`	—	`physHermite_succ`
`physHermite_orthogonal` 📖	—	—	—	—	`physHermite_orthogonal_lt`
`physHermite_orthogonal_cons` 📖	—	—	—	—	`physHermite_orthogonal`
`physHermite_orthogonal_lt` 📖	—	—	—	—	`integral_physHermite_mul_physHermite_eq_integral_deriv` `iterated_deriv_physHermite_eq_aeval` `iterate_derivative_physHermite_of_gt`
`physHermite_parity` 📖	—	—	—	—	`physHermite_one` `physHermite_succ_fun'`
`physHermite_pow` 📖	mathematical	—	`physHermite`	—	—
`physHermite_succ` 📖	mathematical	—	`physHermite`	—	—
`physHermite_succ'` 📖	mathematical	—	`physHermite`	—	`physHermite_succ` `derivative_physHermite`
`physHermite_succ_fun` 📖	mathematical	—	`physHermite`	—	`physHermite_succ'`
`physHermite_succ_fun'` 📖	mathematical	—	`physHermite`	—	`physHermite_succ'`
`physHermite_zero` 📖	mathematical	—	`physHermite`	—	—
`physHermite_zero_apply` 📖	—	—	—	—	—
`polynomial_mem_physHermite_span` 📖	mathematical	—	`physHermite`	—	`polynomial_mem_physHermite_span_induction`
`polynomial_mem_physHermite_span_induction` 📖	mathematical	—	`physHermite`	—	—

---

← Back to Index