Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `InnerProductSpace'`, `core`, `equivL2`, `fromL2`, `toInnerProductSpaceWithL2`, `toInnerWithL2`, `toL2`, `toNormWithL2`, `toNormedAddCommGroupWitL2`, `toNormedSpaceWithL2`, `toNorm₂`, `Norm₂`, `norm₂`, `instCoreOfInnerProductSpace'`, `instInnerOfInnerProductSpace'`, `instInnerProd_physLean`, `instInnerProductSpace'`, `instInnerProductSpace'Forall`, `instInnerProductSpace'Prod`, `«term‖_‖₂»`	20
Theorems `inner'`, `inner'`, `inner'`, `fromL2_inner_left`, `fromL2_toL2`, `inner_top_equiv_norm`, `instCompleteSpaceWithLpOfNatENNReal`, `norm_withLp2_eq_norm2`, `norm₂_sq_eq_re_inner`, `ofLp_inner_left`, `toL2_fromL2`, `toL2_inner_left`, `toLp_inner_left`, `ext_inner_left'`, `ext_inner_right'`, `inner_add_left'`, `inner_add_right'`, `inner_conj_symm'`, `inner_neg_left'`, `inner_neg_right'`, `inner_self_eq_zero'`, `inner_smul_left'`, `inner_smul_right'`, `inner_sub_left'`, `inner_sub_right'`, `inner_sum'`, `inner_zero_left'`, `inner_zero_right'`, `isBoundedBilinearMap_inner'`, `prod_inner_apply'`, `real_inner_comm'`, `real_inner_self_nonneg'`	32
Total	52

ContDiff

Theorems

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

ContDiffAt

Theorems

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

Continuous

Theorems

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

InnerProductSpace'

Definitions

Name	Category	Theorems
`core` 📖	CompOp	2 math math: `norm₂_sq_eq_re_inner`, `inner_top_equiv_norm`
`equivL2` 📖	CompOp	—
`fromL2` 📖	CompOp	6 math math: `fromL2_inner_left`, `ContinuousLinearMap.hasAdjoint`, `toL2_fromL2`, `toL2_inner_left`, `adjoint_eq_clm_adjoint`, `fromL2_toL2`
`toInnerProductSpaceWithL2` 📖	CompOp	2 math math: `ContinuousLinearMap.hasAdjoint`, `adjoint_eq_clm_adjoint`
`toInnerWithL2` 📖	CompOp	4 math math: `fromL2_inner_left`, `ofLp_inner_left`, `toL2_inner_left`, `toLp_inner_left`
`toL2` 📖	CompOp	6 math math: `fromL2_inner_left`, `ContinuousLinearMap.hasAdjoint`, `toL2_fromL2`, `toL2_inner_left`, `adjoint_eq_clm_adjoint`, `fromL2_toL2`
`toNormWithL2` 📖	CompOp	1 math math: `norm_withLp2_eq_norm2`
`toNormedAddCommGroupWitL2` 📖	CompOp	7 math math: `fromL2_inner_left`, `ContinuousLinearMap.hasAdjoint`, `toL2_fromL2`, `toL2_inner_left`, `instCompleteSpaceWithLpOfNatENNReal`, `adjoint_eq_clm_adjoint`, `fromL2_toL2`
`toNormedSpaceWithL2` 📖	CompOp	—
`toNorm₂` 📖	CompOp	2 math math: `norm₂_sq_eq_re_inner`, `norm_withLp2_eq_norm2`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromL2_inner_left` 📖	mathematical	—	`instInnerOfInnerProductSpace'` `toNormedAddCommGroupWitL2` `fromL2` `toInnerWithL2` `toL2`	—	—
`fromL2_toL2` 📖	mathematical	—	`toNormedAddCommGroupWitL2` `fromL2` `toL2`	—	—
`inner_top_equiv_norm` 📖	mathematical	—	`core`	—	—
`instCompleteSpaceWithLpOfNatENNReal` 📖	mathematical	—	`toNormedAddCommGroupWitL2`	—	—
`norm_withLp2_eq_norm2` 📖	mathematical	—	`toNormWithL2` `Norm₂.norm₂` `toNorm₂`	—	`norm₂_sq_eq_re_inner`
`norm₂_sq_eq_re_inner` 📖	mathematical	—	`Norm₂.norm₂` `toNorm₂` `core`	—	—
`ofLp_inner_left` 📖	mathematical	—	`instInnerOfInnerProductSpace'` `toInnerWithL2`	—	`fromL2_inner_left`
`toL2_fromL2` 📖	mathematical	—	`toNormedAddCommGroupWitL2` `toL2` `fromL2`	—	—
`toL2_inner_left` 📖	mathematical	—	`toInnerWithL2` `toNormedAddCommGroupWitL2` `toL2` `instInnerOfInnerProductSpace'` `fromL2`	—	—
`toLp_inner_left` 📖	mathematical	—	`toInnerWithL2` `instInnerOfInnerProductSpace'`	—	`toL2_inner_left`

Norm₂

Definitions

Name	Category	Theorems
`norm₂` 📖	CompOp	2 math math: `InnerProductSpace'.norm₂_sq_eq_re_inner`, `InnerProductSpace'.norm_withLp2_eq_norm2`

(root)

Definitions

Name	Category	Theorems
`InnerProductSpace'` 📖	CompData	—
`Norm₂` 📖	CompData	—
`instCoreOfInnerProductSpace'` 📖	CompOp	—
`instInnerOfInnerProductSpace'` 📖	CompOp	53 math math: `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `HasVarAdjoint.adjoint`, `IsTestFunction.inner`, `ContDiffAt.inner'`, `InnerProductSpace'.fromL2_inner_left`, `ClassicalMechanics.HarmonicOscillator.hamiltonian_eq`, `ClassicalMechanics.HarmonicOscillator.kineticEnergy_eq`, `inner_zero_right'`, `HasAdjoint.smul_right`, `Continuous.inner'`, `real_inner_self_nonneg'`, `InnerProductSpace'.ofLp_inner_left`, `HasAdjoint.adjoint_inner_right`, `HasAdjFDerivAt.inner`, `inner_sum'`, `inner_neg_left'`, `HasAdjFDerivAt.smul`, `InnerProductSpace'.toL2_inner_left`, `inner_sub_right'`, `IsTestFunction.inner_right`, `inner_zero_left'`, `inner_smul_right'`, `deriv_inner_apply'`, `ContDiff.inner'`, `fderiv_inner_apply'`, `real_inner_comm'`, `inner_add_right'`, `prod_inner_apply'`, `inner_add_left'`, `HasFDerivAt.inner'`, `IsTestFunction.inner_left`, `ClassicalMechanics.hamiltons_equations_varGradient`, `inner_self_eq_zero'`, `ClassicalMechanics.HarmonicOscillator.potentialEnergy_deriv`, `inner_sub_left'`, `ClassicalMechanics.HarmonicOscillator.lagrangian_eq`, `inner_conj_symm'`, `inner_smul_left'`, `ClassicalMechanics.HarmonicOscillator.kineticEnergy_deriv`, `ClassicalMechanics.HarmonicOscillator.energy_deriv`, `InnerProductSpace'.toLp_inner_left`, `isBoundedBilinearMap_inner'`, `inner_neg_right'`, `ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae`, `Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential`, `HasAdjoint.adjoint_inner_left`, `adjFDeriv_inner`, `divergence_smul`, `ClassicalMechanics.HarmonicOscillator.potentialEnergy_eq`, `adjFDeriv_smul`, `DifferentiableAt.inner'`, `ClassicalMechanics.Lagrangian.isTotalTimeDerivativeVelocity`
`instInnerProd_physLean` 📖	CompOp	1 math math: `prod_inner_apply'`
`instInnerProductSpace'` 📖	CompOp	31 math math: `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField`, `HasVarAdjoint.gradient`, `ClassicalMechanics.HarmonicOscillator.hamiltonian_eq`, `ClassicalMechanics.HarmonicOscillator.kineticEnergy_eq`, `ClassicalMechanics.euler_lagrange_varGradient`, `HasVarAdjoint.grad`, `Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt`, `HasVarAdjDerivAt.gradient`, `HasAdjFDerivAt.inner`, `gradient_eq_adjFDeriv`, `Electromagnetism.ElectromagneticPotential.kineticTerm_hasVarGradientAt`, `Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt`, `ClassicalMechanics.hamiltons_equations_varGradient`, `HasVarAdjoint.div`, `ClassicalMechanics.HarmonicOscillator.potentialEnergy_deriv`, `ClassicalMechanics.HarmonicOscillator.lagrangian_eq`, `Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_eq_add_gradKineticTerm`, `ClassicalMechanics.HarmonicOscillator.kineticEnergy_deriv`, `ClassicalMechanics.HarmonicOscillator.energy_deriv`, `ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae`, `Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential`, `adjFDeriv_inner`, `divergence_smul`, `ClassicalMechanics.HarmonicOscillator.potentialEnergy_eq`, `HasVarAdjDerivAt.grad`, `Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_gradLagrangian`, `adjFDeriv_smul`, `HasVarAdjDerivAt.div`, `Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component`, `ClassicalMechanics.Lagrangian.isTotalTimeDerivativeVelocity`
`instInnerProductSpace'Forall` 📖	CompOp	—
`instInnerProductSpace'Prod` 📖	CompOp	14 math math: `HasVarAdjDerivAt.prod`, `adjFDeriv_uncurry`, `adjFDeriv_fst`, `HasAdjoint.prodMk`, `adjFDeriv_prod_fst`, `hasAdjFDerivAt_uncurry`, `HasAdjFDerivAt.inner`, `ClassicalMechanics.hamiltons_equations_varGradient`, `adjFDeriv_prod_snd`, `ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae`, `adjFDeriv_inner`, `HasVarAdjoint.prod`, `adjFDeriv_snd`, `HasAdjFDerivAt.prodMk`
`«term‖_‖₂»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_inner_left'` 📖	—	`instInnerOfInnerProductSpace'`	—	—	—
`ext_inner_right'` 📖	—	`instInnerOfInnerProductSpace'`	—	—	—
`inner_add_left'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_add_right'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_conj_symm'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_neg_left'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_neg_right'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_self_eq_zero'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_smul_left'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_smul_right'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_sub_left'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_sub_right'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_sum'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	`InnerProductSpace'.ofLp_inner_left`
`inner_zero_left'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`inner_zero_right'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`isBoundedBilinearMap_inner'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	`inner_add_left'` `inner_smul_left'` `inner_add_right'` `inner_smul_right'` `InnerProductSpace'.inner_top_equiv_norm` `InnerProductSpace'.norm_withLp2_eq_norm2` `InnerProductSpace'.norm₂_sq_eq_re_inner`
`prod_inner_apply'` 📖	mathematical	—	`instInnerProd_physLean` `instInnerOfInnerProductSpace'`	—	—
`real_inner_comm'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—
`real_inner_self_nonneg'` 📖	mathematical	—	`instInnerOfInnerProductSpace'`	—	—

---

← Back to Index