Theorems · Definition · functional analysis
Laplacian.laplacian
{E : Type v} → {F : outParam (Type w)} → [self : Laplacian E F] → E → FΔ f is the Laplacian of f. The meaning of this notation is type-dependent.
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Laplacian
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Laplacianstatement and proof · cited by 0
Cited by41
Results whose statement or proof uses this declaration.
- InnerProductSpace.HarmonicAtproof · cited by 23
- InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasisstatement · cited by 8
- SchwartzMap.laplacian_eq_sumstatement · cited by 5
- InnerProductSpace.HarmonicAt.comp_CLMproof · cited by 4
- HarmonicAt.differentiableAt_complex_partialproof · cited by 3
- InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasisstatement · cited by 3
- SchwartzMap.integral_bilinear_laplacian_right_eq_leftstatement · cited by 3
- TemperedDistribution.laplacian_eq_sumstatement · cited by 2
- InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlanestatement · cited by 2
- InnerProductSpace.HarmonicAt.const_smulproof · cited by 2
- SchwartzMap.integral_smul_laplacian_right_eq_leftstatement · cited by 1
- TemperedDistribution.laplacian_apply_applystatement · cited by 1