ConfigurationSpace

📁 Source: PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean

Statistics

Metric	Count
Definitions `ConfigurationSpace`, `ConfigurationSpace`, `fromRealCLM`, `fromRealLM`, `instAdd`, `instAddCommGroup`, `instAddGroup`, `instChartedSpaceReal`, `instCoeFunForallFinOfNatNatReal`, `instDist`, `instInnerProductSpaceReal`, `instInnerReal`, `instModuleReal`, `instNeg`, `instNorm`, `instNormedAddCommGroup`, `instNormedSpaceReal`, `instOfNatOfNatNat`, `instSMulReal`, `instSeminormedAddCommGroup`, `instSub`, `instZero`, `toRealCLM`, `toRealLM`, `toSpace`, `val`, `valHomeomorphism`, `ConfigurationSpace`	28
Theorems `add_val`, `apply_eq_val`, `apply_zero`, `contDiff_inner_self`, `differentiableAt_inner_self`, `differentiable_inner_self`, `dist_eq_val`, `ext`, `ext_iff`, `inner_def`, `instCompleteSpace`, `instFiniteDimensionalReal`, `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `neg_val`, `smul_val`, `sub_val`, `toSpace_apply`, `zero_val`	18
Total	46
⚠️ With sorry `ConfigurationSpace`, `ConfigurationSpace`	2

ClassicalMechanics.CoplanarDoublePendulum

Definitions

Name	Category	Theorems
`ConfigurationSpace` 📖 ⚠️	CompOp	—

ClassicalMechanics.HarmonicOscillator

Definitions

Name	Category	Theorems
`ConfigurationSpace` 📖	CompData	13 math math: `ConfigurationSpace.neg_val`, `ConfigurationSpace.contDiff_inner_self`, `ConfigurationSpace.instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `ConfigurationSpace.add_val`, `ConfigurationSpace.sub_val`, `ConfigurationSpace.instFiniteDimensionalReal`, `ConfigurationSpace.dist_eq_val`, `ConfigurationSpace.zero_val`, `ConfigurationSpace.instCompleteSpace`, `ConfigurationSpace.inner_def`, `ConfigurationSpace.differentiable_inner_self`, `ConfigurationSpace.differentiableAt_inner_self`, `ConfigurationSpace.smul_val`

ClassicalMechanics.HarmonicOscillator.ConfigurationSpace

Definitions

Name	Category	Theorems
`fromRealCLM` 📖	CompOp	—
`fromRealLM` 📖	CompOp	—
`instAdd` 📖	CompOp	1 math math: `add_val`
`instAddCommGroup` 📖	CompOp	3 math math: `instFiniteDimensionalReal`, `differentiable_inner_self`, `differentiableAt_inner_self`
`instAddGroup` 📖	CompOp	—
`instChartedSpaceReal` 📖	CompOp	1 math math: `instIsManifoldRealModelWithCornersSelfTopWithTopENat`
`instCoeFunForallFinOfNatNatReal` 📖	CompOp	—
`instDist` 📖	CompOp	1 math math: `dist_eq_val`
`instInnerProductSpaceReal` 📖	CompOp	—
`instInnerReal` 📖	CompOp	4 math math: `contDiff_inner_self`, `inner_def`, `differentiable_inner_self`, `differentiableAt_inner_self`
`instModuleReal` 📖	CompOp	3 math math: `instFiniteDimensionalReal`, `differentiable_inner_self`, `differentiableAt_inner_self`
`instNeg` 📖	CompOp	1 math math: `neg_val`
`instNorm` 📖	CompOp	—
`instNormedAddCommGroup` 📖	CompOp	1 math math: `contDiff_inner_self`
`instNormedSpaceReal` 📖	CompOp	1 math math: `contDiff_inner_self`
`instOfNatOfNatNat` 📖	CompOp	1 math math: `zero_val`
`instSMulReal` 📖	CompOp	1 math math: `smul_val`
`instSeminormedAddCommGroup` 📖	CompOp	4 math math: `instIsManifoldRealModelWithCornersSelfTopWithTopENat`, `instCompleteSpace`, `differentiable_inner_self`, `differentiableAt_inner_self`
`instSub` 📖	CompOp	1 math math: `sub_val`
`instZero` 📖	CompOp	—
`toRealCLM` 📖	CompOp	—
`toRealLM` 📖	CompOp	—
`toSpace` 📖	CompOp	1 math math: `toSpace_apply`
`val` 📖	CompOp	11 math math: `neg_val`, `add_val`, `sub_val`, `dist_eq_val`, `zero_val`, `inner_def`, `toSpace_apply`, `apply_zero`, `smul_val`, `ext_iff`, `apply_eq_val`
`valHomeomorphism` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_val` 📖	mathematical	—	`val` `ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instAdd`	—	—
`apply_eq_val` 📖	mathematical	—	`val`	—	—
`apply_zero` 📖	mathematical	—	`val`	—	—
`contDiff_inner_self` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instNormedAddCommGroup` `instNormedSpaceReal` `instInnerReal`	—	—
`differentiableAt_inner_self` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `instInnerReal`	—	—
`differentiable_inner_self` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `instInnerReal`	—	—
`dist_eq_val` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instDist` `val`	—	—
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`inner_def` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instInnerReal` `val`	—	—
`instCompleteSpace` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instSeminormedAddCommGroup`	—	`instFiniteDimensionalReal`
`instFiniteDimensionalReal` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instAddCommGroup` `instModuleReal`	—	`ext`
`instIsManifoldRealModelWithCornersSelfTopWithTopENat` 📖	mathematical	—	`ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instSeminormedAddCommGroup` `instChartedSpaceReal`	—	—
`neg_val` 📖	mathematical	—	`val` `ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instNeg`	—	—
`smul_val` 📖	mathematical	—	`val` `ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instSMulReal`	—	—
`sub_val` 📖	mathematical	—	`val` `ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instSub`	—	—
`toSpace_apply` 📖	mathematical	—	`Space.val` `toSpace` `val`	—	—
`zero_val` 📖	mathematical	—	`val` `ClassicalMechanics.HarmonicOscillator.ConfigurationSpace` `instOfNatOfNatNat`	—	—

ClassicalMechanics.SlidingPendulum

Definitions

Name	Category	Theorems
`ConfigurationSpace` 📖 ⚠️	CompOp	—

---

← Back to Index