Deriv

📁 Source: Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean

Statistics

Metric	Count
Definitions derivCLM, fderivCLM, instLaplacian, instLineDeriv, iteratedPDeriv, pderivCLM	6
Theorems derivCLM_apply, fderivCLM_apply, hasDerivAt, hasFDerivAt, instContinuousLineDeriv, instLineDerivAdd, instLineDerivLeftSMulReal, instLineDerivSMul, integral_bilinear_deriv_right_eq_neg_left, integral_bilinear_laplacian_right_eq_left, integral_bilinear_lineDerivOp_right_eq_neg_left, integral_clm_comp_deriv_right_eq_neg_left, integral_clm_comp_laplacian_right_eq_left, integral_clm_comp_lineDerivOp_right_eq_neg_left, integral_mul_deriv_eq_neg_deriv_mul, integral_mul_laplacian_right_eq_left, integral_mul_lineDerivOp_right_eq_neg_left, integral_smul_deriv_right_eq_neg_left, integral_smul_laplacian_right_eq_left, integral_smul_lineDerivOp_right_eq_neg_left, iteratedLineDerivOp_eq_iteratedFDeriv, iteratedPDeriv_eq_iteratedFDeriv, iteratedPDeriv_one, iteratedPDeriv_succ_left, iteratedPDeriv_succ_right, iteratedPDeriv_zero, laplacianCLM_eq, laplacianCLM_eq', laplacian_apply, laplacian_eq_sum, lineDerivOpCLM_eq, lineDerivOp_apply, lineDerivOp_apply_eq_fderiv, lineDerivOp_compCLMOfContinuousLinearEquiv, pderivCLM_apply, tsupport_derivCLM_subset, tsupport_fderivCLM_subset, tsupport_iteratedLineDerivOp_subset, tsupport_lineDerivOp_subset	39
Total	45

SchwartzMap

Definitions

Name	Category	Theorems
derivCLM 📖	CompOp	4 math math: derivCLM_apply, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, tsupport_derivCLM_subset, TemperedDistribution.derivCLM_apply_apply
fderivCLM 📖	CompOp	5 math math: lineDerivOpCLM_eq, fderivCLM_apply, tsupport_fderivCLM_subset, fderivCLM_fourier_eq, fourier_fderivCLM_eq
instLaplacian 📖	CompOp	10 math math: laplacianCLM_eq, laplacianCLM_eq', integral_mul_laplacian_right_eq_left, integral_bilinear_laplacian_right_eq_left, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, laplacian_eq_sum, TemperedDistribution.laplacian_apply_apply, integral_smul_laplacian_right_eq_left, integral_clm_comp_laplacian_right_eq_left, laplacian_apply
instLineDeriv 📖	CompOp	26 math math: TemperedDistribution.lineDerivOpCLM_eq, lineDerivOpCLM_eq, instLineDerivLeftSMulReal, integral_clm_comp_lineDerivOp_right_eq_neg_left, lineDerivOp_fourier_eq, laplacianCLM_eq, instLineDerivAdd, fourier_lineDerivOp_eq, laplacianCLM_eq', lineDerivOp_compCLMOfContinuousLinearEquiv, tsupport_lineDerivOp_subset, instLineDerivSMul, fourierInv_lineDerivOp_eq, tsupport_iteratedLineDerivOp_subset, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, iteratedPDeriv_eq_iteratedFDeriv, iteratedLineDerivOp_eq_iteratedFDeriv, lineDerivOp_fourierInv_eq, integral_smul_lineDerivOp_right_eq_neg_left, laplacian_eq_sum, lineDerivOp_apply_eq_fderiv, integral_bilinear_lineDerivOp_right_eq_neg_left, TemperedDistribution.lineDerivOp_apply_apply, lineDerivOp_apply, instContinuousLineDeriv, integral_mul_lineDerivOp_right_eq_neg_left
iteratedPDeriv 📖	CompOp	—
pderivCLM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
derivCLM_apply 📖	mathematical	—	DFunLike.coe SchwartzMap Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike derivCLM deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
fderivCLM_apply 📖	mathematical	—	DFunLike.coe SchwartzMap ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instFunLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike fderivCLM fderiv NormedAddCommGroup.toAddCommGroup	—	RingHomIsometric.ids smulCommClass_self ContinuousLinearMap.smulCommClass
hasDerivAt 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul DFunLike.coe SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instFunLike deriv	—	DifferentiableAt.hasDerivAt differentiableAt
hasFDerivAt 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe SchwartzMap instFunLike fderiv	—	DifferentiableAt.hasFDerivAt differentiableAt
instContinuousLineDeriv 📖	mathematical	—	ContinuousLineDeriv SchwartzMap instTopologicalSpace instLineDeriv	—	ContinuousLinearMap.continuous smulCommClass_self RingHomIsometric.ids ContinuousLinearMap.smulCommClass RingHomCompTriple.ids
instLineDerivAdd 📖	mathematical	—	LineDerivAdd SchwartzMap NormedAddCommGroup.toAddCommGroup instAddCommGroup instLineDeriv	—	ContinuousLinearMap.map_add smulCommClass_self RingHomIsometric.ids ContinuousLinearMap.smulCommClass RingHomCompTriple.ids ext map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
instLineDerivLeftSMulReal 📖	mathematical	—	LineDerivLeftSMul Real SchwartzMap SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField instSMul smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Real.commRing instLineDeriv	—	smulCommClass_self ext map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
instLineDerivSMul 📖	mathematical	—	LineDerivSMul SchwartzMap instSMul DenselyNormedField.toNormedField RCLike.toDenselyNormedField instLineDeriv	—	ContinuousLinearMap.map_smul RingHomIsometric.ids smulCommClass_self ContinuousLinearMap.smulCommClass RingHomCompTriple.ids
integral_bilinear_deriv_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instFunLike deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NegZeroClass.toNeg	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable hasDerivAt integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth FiniteDimensional.rclike_to_real Real.borelSpace instIsAddHaarMeasureVolume instSecondCountableTopologyReal IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul
integral_bilinear_laplacian_right_eq_left 📖	mathematical	—	MeasureTheory.integral DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real.instRCLike instFunLike Laplacian.laplacian instLaplacian	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul laplacian_eq_sum sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousLinearMap.coe_sum' Finset.sum_apply MeasureTheory.integral_finset_sum integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth secondCountable_of_proper FiniteDimensional.proper_real IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul Finset.sum_congr integral_bilinear_lineDerivOp_right_eq_neg_left neg_neg
integral_bilinear_lineDerivOp_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap instFunLike LineDeriv.lineDerivOp instLineDeriv NegZeroClass.toNeg	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth secondCountable_of_proper FiniteDimensional.proper_real IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasTemperateGrowth HasFDerivAt.hasLineDerivAt hasFDerivAt
integral_clm_comp_deriv_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NontriviallyNormedField.toNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero instFunLike deriv Real.denselyNormedField NegZeroClass.toNeg ContinuousLinearMap.addCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.module UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid IsBoundedSMul.toUniformContinuousConstSMul ContinuousLinearMap.topologicalSpace	—	RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_bilinear_deriv_right_eq_neg_left smulCommClass_self ContinuousLinearMap.isScalarTower SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
integral_clm_comp_laplacian_right_eq_left 📖	mathematical	—	MeasureTheory.integral DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NontriviallyNormedField.toNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero instFunLike Laplacian.laplacian instLaplacian	—	RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_bilinear_laplacian_right_eq_left smulCommClass_self ContinuousLinearMap.isScalarTower SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
integral_clm_comp_lineDerivOp_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike SchwartzMap ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace Real Real.normedField IsScalarTower.to_smulCommClass' Real.instCommSemiring NontriviallyNormedField.toNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero instFunLike LineDeriv.lineDerivOp instLineDeriv NegZeroClass.toNeg	—	RingHomIsometric.ids IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_bilinear_lineDerivOp_right_eq_neg_left smulCommClass_self ContinuousLinearMap.isScalarTower SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
integral_mul_deriv_eq_neg_deriv_mul 📖	mathematical	—	MeasureTheory.integral Real NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing DFunLike.coe SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instFunLike deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	integral_bilinear_deriv_right_eq_neg_left
integral_mul_laplacian_right_eq_left 📖	mathematical	—	MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFunLike Laplacian.laplacian instLaplacian	—	integral_bilinear_laplacian_right_eq_left
integral_mul_lineDerivOp_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing DFunLike.coe SchwartzMap instFunLike LineDeriv.lineDerivOp instLineDeriv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_bilinear_lineDerivOp_right_eq_neg_left
integral_smul_deriv_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule DFunLike.coe SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instFunLike deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup Real.normedField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	—	integral_bilinear_deriv_right_eq_neg_left NormedSpace.toIsBoundedSMul Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
integral_smul_laplacian_right_eq_left 📖	mathematical	—	MeasureTheory.integral SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing RCLike.toInnerProductSpaceReal instFunLike Laplacian.laplacian instLaplacian	—	integral_bilinear_laplacian_right_eq_left NormedSpace.toIsBoundedSMul Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
integral_smul_lineDerivOp_right_eq_neg_left 📖	mathematical	—	MeasureTheory.integral SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule DFunLike.coe SchwartzMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal instFunLike LineDeriv.lineDerivOp instLineDeriv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_bilinear_lineDerivOp_right_eq_neg_left NormedSpace.toIsBoundedSMul Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
iteratedLineDerivOp_eq_iteratedFDeriv 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike LineDeriv.iteratedLineDerivOp instLineDeriv ContinuousMultilinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike iteratedFDeriv	—	LineDeriv.iteratedLineDerivOp_succ_left SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self iteratedFDeriv_succ_apply_left fderiv_continuousMultilinear_apply_const_apply Finite.of_fintype ContDiff.differentiable_iteratedFDeriv ENat.coe_lt_top smooth
iteratedPDeriv_eq_iteratedFDeriv 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike LineDeriv.iteratedLineDerivOp instLineDeriv ContinuousMultilinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike iteratedFDeriv	—	iteratedLineDerivOp_eq_iteratedFDeriv
iteratedPDeriv_one 📖	mathematical	—	LineDeriv.iteratedLineDerivOp LineDeriv.lineDerivOp	—	LineDeriv.iteratedLineDerivOp_one
iteratedPDeriv_succ_left 📖	mathematical	—	LineDeriv.iteratedLineDerivOp LineDeriv.lineDerivOp Fin.tail	—	LineDeriv.iteratedLineDerivOp_succ_left
iteratedPDeriv_succ_right 📖	mathematical	—	LineDeriv.iteratedLineDerivOp Fin.init LineDeriv.lineDerivOp	—	LineDeriv.iteratedLineDerivOp_succ_right
iteratedPDeriv_zero 📖	mathematical	—	LineDeriv.iteratedLineDerivOp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LineDeriv.iteratedLineDerivOp_zero
laplacianCLM_eq 📖	mathematical	—	DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike LineDeriv.laplacianCLM instLineDeriv instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMul instContinuousLineDeriv Laplacian.laplacian instLaplacian	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMul instContinuousLineDeriv ContinuousLinearMap.coe_sum' Finset.sum_congr Finset.sum_apply laplacian_eq_sum
laplacianCLM_eq' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring SchwartzMap InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule Real.normedField smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing NormedSpace.toModule ContinuousLinearMap.funLike LineDeriv.laplacianCLM instLineDeriv instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMul instContinuousLineDeriv Laplacian.laplacian instLaplacian	—	smulCommClass_self instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMul instContinuousLineDeriv
laplacian_apply 📖	mathematical	—	DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFunLike Laplacian.laplacian instLaplacian InnerProductSpace.instLaplacian	—	laplacian_eq_sum sum_apply InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis Finset.sum_congr Matrix.cons_val_fin_one
laplacian_eq_sum 📖	mathematical	—	Laplacian.laplacian SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLaplacian Finset.sum AddCommGroup.toAddCommMonoid instAddCommGroup Finset.univ LineDeriv.lineDerivOp instLineDeriv DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike	—	LineDeriv.laplacianCLM_eq_sum smulCommClass_self instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMul instContinuousLineDeriv instLineDerivLeftSMulReal
lineDerivOpCLM_eq 📖	mathematical	—	LineDeriv.lineDerivOpCLM SchwartzMap NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instAddCommGroup instModule instTopologicalSpace NormedAddCommGroup.toAddCommGroup instLineDeriv instLineDerivAdd instLineDerivSMul instContinuousLineDeriv ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SeminormedAddCommGroup.toAddCommGroup RingHomCompTriple.ids evalCLM fderivCLM	—	instLineDerivAdd instLineDerivSMul instContinuousLineDeriv
lineDerivOp_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike LineDeriv.lineDerivOp instLineDeriv lineDeriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup	—	DifferentiableAt.lineDeriv_eq_fderiv differentiableAt
lineDerivOp_apply_eq_fderiv 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike LineDeriv.lineDerivOp instLineDeriv ContinuousLinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike fderiv	—	—
lineDerivOp_compCLMOfContinuousLinearEquiv 📖	mathematical	—	LineDeriv.lineDerivOp SchwartzMap instLineDeriv DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.funLike compCLMOfContinuousLinearEquiv ContinuousLinearEquiv Real Real.semiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids ext RingHomCompTriple.ids ContinuousLinearEquiv.comp_right_fderiv
pderivCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike LineDeriv.lineDerivOpCLM LineDeriv.lineDerivOp	—	LineDeriv.lineDerivOpCLM_apply
tsupport_derivCLM_subset 📖	mathematical	—	Set Real Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower IsBoundedSMul.continuousSMul Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike derivCLM	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace tsupport_fderiv_apply_subset
tsupport_fderivCLM_subset 📖	mathematical	—	Set Set.instHasSubset tsupport ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero DFunLike.coe SchwartzMap ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instFunLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike fderivCLM NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	tsupport_fderiv_subset
tsupport_iteratedLineDerivOp_subset 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike LineDeriv.iteratedLineDerivOp instLineDeriv	—	Set.instReflSubset LineDeriv.iteratedLineDerivOp_succ_left HasSubset.Subset.trans Set.instIsTransSubset tsupport_lineDerivOp_subset
tsupport_lineDerivOp_subset 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike LineDeriv.lineDerivOp instLineDeriv	—	tsupport_fderiv_apply_subset

---

← Back to Index