HasVarAdjoint

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

Statistics

Metric	Count
Definitions HasVarAdjoint	1
Theorems add, adjFDeriv_apply, adjoint, clm_apply, comp, congr_fun, deriv, div, ext', fderiv_apply, fst, grad, gradient, id, mul_left, mul_right, neg, of_eq, of_neg, prod, smul_left, smul_right, snd, sub, sum, symm, test_fun_preserving, test_fun_preserving', unique, unique_on_test_functions, zero	31
Total	32

HasVarAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	HasVarAdjoint	—	—	test_fun_preserving IsTestFunction.add test_fun_preserving' inner_add_left' inner_add_right' IsTestFunction.integrable IsTestFunction.inner adjoint IsLocalizedFunctionTransform.add ext'
adjFDeriv_apply 📖	mathematical	—	HasVarAdjoint adjFDeriv divergence	—	IsTestFunction.adjFDeriv IsTestFunction.smul_right IsTestFunction.neg IsTestFunction.divergence DifferentiableAt.hasAdjFDerivAt IsTestFunction.differentiable HasAdjoint.adjoint_inner_left HasAdjFDerivAt.hasAdjoint_fderiv inner_sum' IsTestFunction.integrable inner_smul_right' IsTestFunction.mul_right IsTestFunction.comp_left ContDiff.inner' IsTestFunction.contDiff IsTestFunction.of_fderiv fderiv_inner_apply' inner_zero_left' IsTestFunction.mul_left IsTestFunction.smooth IsTestFunction.fderiv_apply IsTestFunction.inner_left inner_zero_right' divergence_eq_sum_fderiv' inner_neg_right' real_inner_comm'
adjoint 📖	mathematical	HasVarAdjoint IsTestFunction	instInnerOfInnerProductSpace'	—	—
clm_apply 📖	mathematical	—	HasVarAdjoint adjoint	—	IsTestFunction.family_linearMap_comp InnerProductSpace'.instCompleteSpaceWithLpOfNatENNReal adjoint_eq_clm_adjoint IsTestFunction.comp_left IsTestFunction.contDiff IsTestFunction.supp HasAdjoint.adjoint_inner_right HasAdjoint.congr_adj ContinuousLinearMap.hasAdjoint
comp 📖	—	HasVarAdjoint	—	—	test_fun_preserving test_fun_preserving' adjoint IsLocalizedFunctionTransform.fun_comp ext'
congr_fun 📖	—	HasVarAdjoint	—	—	test_fun_preserving test_fun_preserving' adjoint ext'
deriv 📖	mathematical	—	HasVarAdjoint	—	DifferentiableAt.inner' IsTestFunction.differentiable IsTestFunction.integrable IsTestFunction.deriv IsTestFunction.inner IsTestFunction.inner_right IsTestFunction.contDiff deriv_inner_apply' inner_neg_right' IsLocalizedFunctionTransform.neg IsLocalizedFunctionTransform.deriv
div 📖	mathematical	—	HasVarAdjoint Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instInnerProductSpace' Space.div Space.grad	—	of_neg Space.instFiniteDimensionalReal Space.instBorelSpace symm grad IsLocalizedFunctionTransform.grad
ext' 📖	mathematical	HasVarAdjoint	IsLocalizedFunctionTransform	—	—
fderiv_apply 📖	mathematical	—	HasVarAdjoint	—	IsTestFunction.fderiv_apply IsTestFunction.neg IsTestFunction.integrable IsTestFunction.inner_right IsTestFunction.contDiff IsTestFunction.of_fderiv inner_neg_right' fderiv_inner_apply' IsTestFunction.differentiable IsLocalizedFunctionTransform.neg IsLocalizedFunctionTransform.fderiv
fst 📖	—	HasVarAdjoint instInnerProductSpace'Prod	—	—	IsTestFunction.prod_fst test_fun_preserving test_fun_preserving' IsTestFunction.prodMk IsTestFunction.zero inner_zero_right' adjoint ext'
grad 📖	mathematical	—	HasVarAdjoint Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instInnerProductSpace' Space.grad Space.div	—	Space.instFiniteDimensionalReal Space.instBorelSpace clm_apply HasAdjoint.adjoint Space.basis_repr_inner_eq comp gradient Space.grad_eq_gradiant
gradient 📖	mathematical	—	HasVarAdjoint Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instInnerProductSpace' Space.instSeminormedAddCommGroup Space.div Space.basis	—	congr_fun Space.instFiniteDimensionalReal Space.instBorelSpace of_eq adjFDeriv_apply divergence_eq_space_div IsTestFunction.differentiable IsLocalizedFunctionTransform.neg IsLocalizedFunctionTransform.div_comp_repr gradient_eq_adjFDeriv
id 📖	mathematical	—	HasVarAdjoint	—	IsLocalizedFunctionTransform.id
mul_left 📖	—	HasVarAdjoint instInnerProductSpace'	—	—	test_fun_preserving IsTestFunction.mul_left test_fun_preserving' adjoint ext'
mul_right 📖	—	HasVarAdjoint instInnerProductSpace'	—	—	test_fun_preserving IsTestFunction.mul_right test_fun_preserving' adjoint ext'
neg 📖	—	HasVarAdjoint	—	—	test_fun_preserving IsTestFunction.neg test_fun_preserving' inner_neg_left' inner_neg_right' adjoint IsLocalizedFunctionTransform.neg ext'
of_eq 📖	—	HasVarAdjoint IsLocalizedFunctionTransform	—	—	test_fun_preserving test_fun_preserving' adjoint
of_neg 📖	—	HasVarAdjoint	—	—	neg
prod 📖	mathematical	HasVarAdjoint	instInnerProductSpace'Prod	—	test_fun_preserving IsTestFunction.prodMk test_fun_preserving' IsTestFunction.prod_fst IsTestFunction.prod_snd IsTestFunction.add IsTestFunction.integrable IsTestFunction.inner_right IsTestFunction.contDiff adjoint inner_add_right' ext'
smul_left 📖	—	HasVarAdjoint	—	—	test_fun_preserving IsTestFunction.smul_left test_fun_preserving' inner_smul_left' adjoint ext'
smul_right 📖	—	HasVarAdjoint	—	—	test_fun_preserving IsTestFunction.smul_left test_fun_preserving' inner_smul_left' adjoint ext'
snd 📖	—	HasVarAdjoint instInnerProductSpace'Prod	—	—	IsTestFunction.prod_snd test_fun_preserving test_fun_preserving' IsTestFunction.prodMk IsTestFunction.zero inner_zero_right' adjoint ext'
sub 📖	—	HasVarAdjoint	—	—	add neg
sum 📖	—	HasVarAdjoint	—	—	zero add
symm 📖	—	HasVarAdjoint IsLocalizedFunctionTransform	—	—	test_fun_preserving' test_fun_preserving real_inner_comm' adjoint
test_fun_preserving 📖	—	HasVarAdjoint IsTestFunction	—	—	—
test_fun_preserving' 📖	—	HasVarAdjoint IsTestFunction	—	—	—
unique 📖	—	HasVarAdjoint	—	—	ext' IsTestFunction.smul_right unique_on_test_functions
unique_on_test_functions 📖	—	HasVarAdjoint IsTestFunction	—	—	fundamental_theorem_of_variational_calculus IsTestFunction.sub inner_sub_left' IsTestFunction.integrable IsTestFunction.inner inner_conj_symm'
zero 📖	mathematical	—	HasVarAdjoint	—	IsTestFunction.zero inner_zero_left' inner_zero_right'

(root)

Definitions

Name	Category	Theorems
HasVarAdjoint 📖	CompData	10 math math: HasVarAdjoint.gradient, HasVarAdjoint.fderiv_apply, HasVarAdjoint.clm_apply, HasVarAdjoint.grad, HasVarAdjoint.zero, HasVarAdjoint.adjFDeriv_apply, HasVarAdjoint.div, HasVarAdjoint.id, HasVarAdjoint.deriv, HasVarAdjDerivAt.adjoint

---

← Back to Index