Calculus

📁 Source: PhysLean/Mathematics/InnerProductSpace/Calculus.lean

Statistics

Metric	Count
Definitions fderivInnerCLM'	1
Theorems inner', inner', deriv_inner_apply', fderiv_inner_apply'	4
Total	5

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner' 📖	mathematical	—	instInnerOfInnerProductSpace'	—	HasFDerivAt.inner'

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner' 📖	mathematical	—	instInnerOfInnerProductSpace' fderivInnerCLM'	—	isBoundedBilinearMap_inner'

(root)

Definitions

Name	Category	Theorems
fderivInnerCLM' 📖	CompOp	1 math math: HasFDerivAt.inner'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_inner_apply' 📖	mathematical	—	instInnerOfInnerProductSpace'	—	fderiv_inner_apply'
fderiv_inner_apply' 📖	mathematical	—	instInnerOfInnerProductSpace'	—	HasFDerivAt.inner'

---

← Back to Index