DerivNotation

📁 Source: Mathlib/Analysis/Distribution/DerivNotation.lean

Statistics

Metric	Count
Definitions ContinuousLineDeriv, laplacian, termΔ, bilinearLineDerivTwo, iteratedLineDerivOp, iteratedLineDerivOpCLM, laplacianCLM, lineDerivOp, lineDerivOpCLM, tensorLineDerivTwo, «term∂^{_}», «term∂_{_}», LineDerivAdd, LineDerivLeftSMul, LineDerivSMul	15
Theorems continuous_lineDerivOp, continuous_iteratedLineDerivOp, iteratedLineDerivOpCLM_apply, iteratedLineDerivOp_add, iteratedLineDerivOp_const_eq_iter_lineDerivOp, iteratedLineDerivOp_fin_zero, iteratedLineDerivOp_neg, iteratedLineDerivOp_one, iteratedLineDerivOp_smul, iteratedLineDerivOp_succ_left, iteratedLineDerivOp_succ_right, iteratedLineDerivOp_sum, iteratedLineDerivOp_zero, laplacianCLM_eq_sum, lineDerivOpCLM_apply, lineDerivOp_left_neg, lineDerivOp_left_sum, lineDerivOp_left_zero, lineDerivOp_neg, lineDerivOp_sum, lineDerivOp_zero, tensorLineDerivTwo_canonicalCovariantTensor_eq_sum, tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp, lineDerivOp_add, lineDerivOp_left_add, lineDerivOp_left_smul, lineDerivOp_smul	27
Total	42

ContinuousLineDeriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_lineDerivOp 📖	mathematical	—	Continuous LineDeriv.lineDerivOp	—	—

Laplacian

Definitions

Name	Category	Theorems
laplacian 📖	CompOp	25 math math: SchwartzMap.laplacianCLM_eq, ContDiffAt.laplacian_CLM_comp_left, SchwartzMap.laplacianCLM_eq', ContDiffAt.laplacian_add, SchwartzMap.integral_mul_laplacian_right_eq_left, InnerProductSpace.laplacian_smul, TemperedDistribution.laplacian_eq_sum, SchwartzMap.integral_bilinear_laplacian_right_eq_left, ContDiffAt.laplacian_add_nhds, InnerProductSpace.laplacian_congr_nhds, InnerProductSpace.laplacianWithin_univ, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, SchwartzMap.laplacian_eq_sum, ContDiffAt.laplacian_CLM_comp_left_nhds, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, TemperedDistribution.laplacian_apply_apply, SchwartzMap.integral_smul_laplacian_right_eq_left, InnerProductSpace.laplacian_eq_iteratedDeriv_real, InnerProductSpace.laplacian_smul_nhds, InnerProductSpace.laplacian_CLE_comp_left, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, SchwartzMap.laplacian_apply, TemperedDistribution.laplacianCLM_apply
termΔ 📖	CompOp	—

LineDeriv

Definitions

Name	Category	Theorems
bilinearLineDerivTwo 📖	CompOp	—
iteratedLineDerivOp 📖	CompOp	19 math math: SchwartzMap.iteratedPDeriv_zero, SchwartzMap.iteratedPDeriv_succ_right, iteratedLineDerivOp_zero, iteratedLineDerivOp_succ_left, iteratedLineDerivOp_sum, SchwartzMap.iteratedPDeriv_one, iteratedLineDerivOpCLM_apply, SchwartzMap.tsupport_iteratedLineDerivOp_subset, iteratedLineDerivOp_fin_zero, continuous_iteratedLineDerivOp, SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv, SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv, SchwartzMap.iteratedPDeriv_succ_left, iteratedLineDerivOp_smul, iteratedLineDerivOp_one, iteratedLineDerivOp_succ_right, iteratedLineDerivOp_const_eq_iter_lineDerivOp, iteratedLineDerivOp_add, iteratedLineDerivOp_neg
iteratedLineDerivOpCLM 📖	CompOp	1 math math: iteratedLineDerivOpCLM_apply
laplacianCLM 📖	CompOp	4 math math: SchwartzMap.laplacianCLM_eq, SchwartzMap.laplacianCLM_eq', laplacianCLM_eq_sum, TemperedDistribution.laplacianCLM_apply
lineDerivOp 📖	CompOp	43 math math: ContinuousLineDeriv.continuous_lineDerivOp, lineDerivOp_left_zero, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, SchwartzMap.lineDerivOp_fourier_eq, TemperedDistribution.lineDerivOp_fourier_eq, SchwartzMap.iteratedPDeriv_succ_right, SchwartzMap.fourier_lineDerivOp_eq, TemperedDistribution.fourierInv_lineDerivOp_eq, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, iteratedLineDerivOp_succ_left, SchwartzMap.iteratedPDeriv_one, LineDerivAdd.lineDerivOp_add, SchwartzMap.tsupport_lineDerivOp_subset, laplacianCLM_eq_sum, LineDerivAdd.lineDerivOp_left_add, SchwartzMap.pderivCLM_apply, SchwartzMap.fourierInv_lineDerivOp_eq, lineDerivOp_left_sum, TemperedDistribution.fourier_lineDerivOp_eq, lineDerivOp_zero, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_eq_sum, tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp, SchwartzMap.lineDerivOp_fourierInv_eq, SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left, LineDerivLeftSMul.lineDerivOp_left_smul, SchwartzMap.laplacian_eq_sum, SchwartzMap.lineDerivOp_apply_eq_fderiv, lineDerivOp_neg, SchwartzMap.iteratedPDeriv_succ_left, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, tensorLineDerivTwo_canonicalCovariantTensor_eq_sum, iteratedLineDerivOp_one, iteratedLineDerivOp_succ_right, TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, LineDerivSMul.lineDerivOp_smul, iteratedLineDerivOp_const_eq_iter_lineDerivOp, lineDerivOpCLM_apply, SchwartzMap.lineDerivOp_apply, SchwartzMap.integral_mul_lineDerivOp_right_eq_neg_left, lineDerivOp_left_neg, lineDerivOp_sum
lineDerivOpCLM 📖	CompOp	4 math math: TemperedDistribution.lineDerivOpCLM_eq, SchwartzMap.lineDerivOpCLM_eq, SchwartzMap.pderivCLM_apply, lineDerivOpCLM_apply
tensorLineDerivTwo 📖	CompOp	2 math math: tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp, tensorLineDerivTwo_canonicalCovariantTensor_eq_sum
«term∂^{_}»»} 📖	CompOp	—
«term∂_{_}»»} 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_iteratedLineDerivOp 📖	mathematical	—	Continuous iteratedLineDerivOp	—	continuous_id Continuous.comp ContinuousLineDeriv.continuous_lineDerivOp
iteratedLineDerivOpCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike iteratedLineDerivOpCLM iteratedLineDerivOp	—	—
iteratedLineDerivOp_add 📖	mathematical	—	iteratedLineDerivOp AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	LineDerivAdd.lineDerivOp_add
iteratedLineDerivOp_const_eq_iter_lineDerivOp 📖	mathematical	—	iteratedLineDerivOp Nat.iterate lineDerivOp	—	iteratedLineDerivOp_succ_left Function.iterate_succ_apply'
iteratedLineDerivOp_fin_zero 📖	mathematical	—	iteratedLineDerivOp	—	—
iteratedLineDerivOp_neg 📖	mathematical	—	iteratedLineDerivOp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_neg AddMonoidHom.instAddMonoidHomClass iteratedLineDerivOp_add
iteratedLineDerivOp_one 📖	mathematical	—	iteratedLineDerivOp lineDerivOp	—	—
iteratedLineDerivOp_smul 📖	mathematical	—	iteratedLineDerivOp	—	LineDerivSMul.lineDerivOp_smul
iteratedLineDerivOp_succ_left 📖	mathematical	—	iteratedLineDerivOp lineDerivOp Fin.tail	—	—
iteratedLineDerivOp_succ_right 📖	mathematical	—	iteratedLineDerivOp Fin.init lineDerivOp	—	iteratedLineDerivOp_succ_left Fin.tail_init_eq_init_tail
iteratedLineDerivOp_sum 📖	mathematical	—	iteratedLineDerivOp Finset.sum AddCommGroup.toAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass iteratedLineDerivOp_add
iteratedLineDerivOp_zero 📖	mathematical	—	iteratedLineDerivOp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass iteratedLineDerivOp_add
laplacianCLM_eq_sum 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike laplacianCLM Finset.sum Finset.univ lineDerivOp OrthonormalBasis Real.instRCLike OrthonormalBasis.instFunLike	—	ContinuousLinearMap.coe_sum' Finset.sum_congr Finset.sum_apply
lineDerivOpCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike lineDerivOpCLM lineDerivOp	—	—
lineDerivOp_left_neg 📖	mathematical	—	lineDerivOp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_neg AddMonoidHom.instAddMonoidHomClass LineDerivAdd.lineDerivOp_left_add
lineDerivOp_left_sum 📖	mathematical	—	lineDerivOp Finset.sum AddCommGroup.toAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass LineDerivAdd.lineDerivOp_left_add
lineDerivOp_left_zero 📖	mathematical	—	lineDerivOp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass LineDerivAdd.lineDerivOp_left_add
lineDerivOp_neg 📖	mathematical	—	lineDerivOp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_neg AddMonoidHom.instAddMonoidHomClass LineDerivAdd.lineDerivOp_add
lineDerivOp_sum 📖	mathematical	—	lineDerivOp Finset.sum AddCommGroup.toAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass LineDerivAdd.lineDerivOp_add
lineDerivOp_zero 📖	mathematical	—	lineDerivOp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass LineDerivAdd.lineDerivOp_add
tensorLineDerivTwo_canonicalCovariantTensor_eq_sum 📖	mathematical	—	DFunLike.coe LinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring TensorProduct AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike tensorLineDerivTwo InnerProductSpace.canonicalCovariantTensor Finset.sum Finset.univ lineDerivOp OrthonormalBasis OrthonormalBasis.instFunLike	—	InnerProductSpace.canonicalCovariantTensor_eq_sum map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp
tensorLineDerivTwo_eq_lineDerivOp_lineDerivOp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike tensorLineDerivTwo TensorProduct.tmul lineDerivOp	—	TensorProduct.lift.tmul

LineDerivAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lineDerivOp_add 📖	mathematical	—	LineDeriv.lineDerivOp AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
lineDerivOp_left_add 📖	mathematical	—	LineDeriv.lineDerivOp AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—

LineDerivLeftSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lineDerivOp_left_smul 📖	mathematical	—	LineDeriv.lineDerivOp	—	—

LineDerivSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lineDerivOp_smul 📖	mathematical	—	LineDeriv.lineDerivOp	—	—

(root)

Definitions

Name	Category	Theorems
ContinuousLineDeriv 📖	CompData	2 math math: TemperedDistribution.instContinuousLineDeriv, SchwartzMap.instContinuousLineDeriv
LineDerivAdd 📖	CompData	2 math math: SchwartzMap.instLineDerivAdd, TemperedDistribution.instLineDerivAdd
LineDerivLeftSMul 📖	CompData	2 math math: SchwartzMap.instLineDerivLeftSMulReal, TemperedDistribution.instLineDerivLeftSMulReal
LineDerivSMul 📖	CompData	3 math math: SchwartzMap.instLineDerivSMul, TemperedDistribution.instLineDerivSMulReal, TemperedDistribution.instLineDerivSMulComplex

---

← Back to Index