HasVarAdjDeriv

📁 Source: PhysLean/Mathematics/VariationalCalculus/HasVarAdjDeriv.lean

Statistics

Metric	Count
Definitions HasVarAdjDerivAt	1
Theorems add, adjoint, apply_smooth_of_smooth, apply_smooth_self, comp, congr, const, const_mul, deriv, deriv', deriv_adjoint_of_linear, diff, differentiable_linear, div, fderiv, fderiv', fmap, fst, fun_mul, grad, gradient, hasVarAdjDerivAt_of_hasVarAdjoint_of_linear, id, linearize, linearize_of_linear, mul, neg, prod, smooth_R, smooth_adjoint, smooth_at, smooth_linear, snd, sum, unique, unique_on_test_functions	36
Total	37

HasVarAdjDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	HasVarAdjDerivAt	—	—	smooth_at diff differentiable_linear linearize HasVarAdjoint.congr_fun HasVarAdjoint.add adjoint IsTestFunction.smooth smooth_R
adjoint 📖	mathematical	HasVarAdjDerivAt	HasVarAdjoint	—	—
apply_smooth_of_smooth 📖	—	HasVarAdjDerivAt	—	—	diff
apply_smooth_self 📖	—	HasVarAdjDerivAt	—	—	apply_smooth_of_smooth smooth_at
comp 📖	—	HasVarAdjDerivAt	—	—	smooth_at diff linearize HasVarAdjoint.comp adjoint HasVarAdjoint.congr_fun IsTestFunction.contDiff
congr 📖	—	HasVarAdjDerivAt	—	—	smooth_at diff fderiv_uncurry_comp_fst linearize HasVarAdjoint.congr_fun adjoint IsTestFunction.contDiff
const 📖	mathematical	—	HasVarAdjDerivAt	—	HasVarAdjoint.zero
const_mul 📖	—	HasVarAdjDerivAt instInnerProductSpace'	—	—	smooth_at IsTestFunction.zero inner_zero_right' mul
deriv 📖	—	HasVarAdjDerivAt	—	—	comp deriv' apply_smooth_self
deriv' 📖	mathematical	—	HasVarAdjDerivAt	—	function_differentiableAt_snd fderiv_uncurry_differentiable_fst_comp_snd_apply fderiv_swap HasVarAdjoint.congr_fun HasVarAdjoint.deriv IsTestFunction.smooth
deriv_adjoint_of_linear 📖	—	HasVarAdjoint	—	—	HasVarAdjoint.congr_fun IsTestFunction.contDiff
diff 📖	—	HasVarAdjDerivAt	—	—	—
differentiable_linear 📖	—	HasVarAdjDerivAt	—	—	smooth_linear
div 📖	mathematical	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	HasVarAdjDerivAt Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instInnerProductSpace' Space.div Space.grad	—	hasVarAdjDerivAt_of_hasVarAdjoint_of_linear Space.instFiniteDimensionalReal Space.instBorelSpace Space.div_add Space.div_smul function_differentiableAt_snd fderiv_uncurry_differentiable_snd_comp_fst_apply fderiv_swap function_differentiableAt_fst HasVarAdjoint.div
fderiv 📖	mathematical	—	HasVarAdjDerivAt	—	hasVarAdjDerivAt_of_hasVarAdjoint_of_linear fderiv_swap HasVarAdjoint.fderiv_apply
fderiv' 📖	—	HasVarAdjDerivAt	—	—	fderiv apply_smooth_self comp
fmap 📖	mathematical	HasAdjFDerivAt	HasVarAdjDerivAt	—	HasVarAdjoint.congr_fun IsTestFunction.contDiff IsTestFunction.supp HasAdjFDerivAt.contDiffAt_deriv HasAdjFDerivAt.hasAdjoint_fderiv HasAdjoint.adjoint_apply_zero HasAdjoint.adjoint_inner_left
fst 📖	—	HasVarAdjDerivAt instInnerProductSpace'Prod	—	—	smooth_at diff linearize smooth_R smooth_linear HasVarAdjoint.congr_fun HasVarAdjoint.fst adjoint smooth_adjoint IsTestFunction.contDiff
fun_mul 📖	—	HasVarAdjDerivAt instInnerProductSpace'	—	—	smooth_at IsTestFunction.zero inner_zero_right' mul
grad 📖	mathematical	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	HasVarAdjDerivAt Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instInnerProductSpace' Space.grad Space.div	—	hasVarAdjDerivAt_of_hasVarAdjoint_of_linear Space.instFiniteDimensionalReal Space.instBorelSpace Space.grad_eq_sum Space.grad_add Space.grad_smul fderiv_uncurry_differentiable_snd_comp_fst_apply fderiv_swap HasVarAdjoint.grad
gradient 📖	mathematical	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal	HasVarAdjDerivAt Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instInnerProductSpace' Space.instSeminormedAddCommGroup Space.div Space.basis	—	hasVarAdjDerivAt_of_hasVarAdjoint_of_linear Space.instFiniteDimensionalReal Space.instBorelSpace Space.gradient_eq_sum Space.gradient_eq_grad Space.grad_add Space.grad_eq_gradiant Space.grad_smul fderiv_uncurry_differentiable_snd_comp_fst_apply fderiv_swap HasVarAdjoint.gradient
hasVarAdjDerivAt_of_hasVarAdjoint_of_linear 📖	mathematical	HasVarAdjoint	HasVarAdjDerivAt	—	linearize_of_linear deriv_adjoint_of_linear
id 📖	mathematical	—	HasVarAdjDerivAt	—	HasVarAdjoint.id
linearize 📖	—	HasVarAdjDerivAt	—	—	—
linearize_of_linear 📖	—	—	—	—	—
mul 📖	—	HasVarAdjDerivAt instInnerProductSpace'	—	—	smooth_at diff differentiable_linear linearize HasVarAdjoint.congr_fun HasVarAdjoint.add HasVarAdjoint.mul_right adjoint apply_smooth_self HasVarAdjoint.mul_left IsTestFunction.smooth smooth_R
neg 📖	—	HasVarAdjDerivAt	—	—	smooth_at diff linearize HasVarAdjoint.congr_fun HasVarAdjoint.neg adjoint IsTestFunction.smooth
prod 📖	mathematical	HasVarAdjDerivAt	instInnerProductSpace'Prod	—	smooth_at diff smooth_R linearize smooth_linear HasVarAdjoint.congr_fun HasVarAdjoint.prod adjoint smooth_adjoint IsTestFunction.contDiff
smooth_R 📖	—	HasVarAdjDerivAt	—	—	diff
smooth_adjoint 📖	—	HasVarAdjDerivAt	—	—	diff smooth_at
smooth_at 📖	—	HasVarAdjDerivAt	—	—	—
smooth_linear 📖	—	HasVarAdjDerivAt	—	—	smooth_R
snd 📖	—	HasVarAdjDerivAt instInnerProductSpace'Prod	—	—	smooth_at diff linearize smooth_R smooth_linear HasVarAdjoint.congr_fun HasVarAdjoint.snd adjoint smooth_adjoint IsTestFunction.contDiff
sum 📖	—	HasVarAdjDerivAt	—	—	const add
unique 📖	—	HasVarAdjDerivAt	—	—	HasVarAdjoint.unique adjoint
unique_on_test_functions 📖	—	HasVarAdjDerivAt IsTestFunction	—	—	HasVarAdjoint.unique_on_test_functions adjoint

(root)

Definitions

Name	Category	Theorems
HasVarAdjDerivAt 📖	CompData	11 math math: HasVarAdjDerivAt.const, HasVarAdjDerivAt.deriv', HasVarAdjDerivAt.gradient, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, HasVarAdjDerivAt.fderiv, HasVarAdjDerivAt.id, HasVarAdjDerivAt.fmap, HasVarAdjDerivAt.grad, HasVarAdjDerivAt.hasVarAdjDerivAt_of_hasVarAdjoint_of_linear, HasVarAdjDerivAt.div, Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component

---

← Back to Index