Configuration space of the harmonic oscillator

The configuration space is defined as a one-dimensional smooth manifold, modeled on ℝ, with a chosen coordinate.

structure ClassicalMechanics.HarmonicOscillator.ConfigurationSpace : Type

The configuration space of the harmonic oscillator.

• val : ℝ

  The underlying real coordinate.

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.ext {x y : ConfigurationSpace} (h : x.val = y.val) : x = y

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.ext_iff {x y : ConfigurationSpace} : x = y ↔ x.val = y.val

Algebraic and analytical structure

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instZero : Zero ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instZero = { zero := { val := 0 } }

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instOfNatOfNatNat : OfNat ConfigurationSpace 0

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instOfNatOfNatNat = { ofNat := { val := 0 } }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.zero_val : val 0 = 0

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instAdd : Add ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instAdd = { add := fun (x y : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => { val := x.val + y.val } }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.add_val (x y : ConfigurationSpace) : (x + y).val = x.val + y.val

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNeg : Neg ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNeg = { neg := fun (x : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => { val := -x.val } }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.neg_val (x : ConfigurationSpace) : (-x).val = -x.val

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instSub : Sub ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instSub = { sub := fun (x y : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => { val := x.val - y.val } }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.sub_val (x y : ConfigurationSpace) : (x - y).val = x.val - y.val

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instSMulReal : SMul ℝ ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instSMulReal = { smul := fun (r : ℝ) (x : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => { val := r * x.val } }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.smul_val (r : ℝ) (x : ConfigurationSpace) : (r • x).val = r * x.val

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instCoeFunForallFinOfNatNatReal : CoeFun ConfigurationSpace fun (x : ConfigurationSpace) => Fin 1 → ℝ

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instCoeFunForallFinOfNatNatReal = { coe := fun (x : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) (x_1 : Fin 1) => x.val }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.apply_zero (x : ConfigurationSpace) : (fun (x_1 : Fin 1) => x.val) 0 = x.val

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.apply_eq_val (x : ConfigurationSpace) (i : Fin 1) : (fun (x_1 : Fin 1) => x.val) i = x.val

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instAddGroup : AddGroup ConfigurationSpace

Equations

• One or more equations did not get rendered due to their size.

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instAddCommGroup : AddCommGroup ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instAddCommGroup = { toAddGroup := ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instAddGroup, add_comm := ⋯ }

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instModuleReal : Module ℝ ConfigurationSpace

Equations

• One or more equations did not get rendered due to their size.

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNorm : Norm ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNorm = { norm := fun (x : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => ‖x.val‖ }

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instDist : Dist ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instDist = { dist := fun (x y : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => ‖x - y‖ }

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.dist_eq_val (x y : ConfigurationSpace) : dist x y = ‖x.val - y.val‖

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instSeminormedAddCommGroup : SeminormedAddCommGroup ConfigurationSpace

Equations

• One or more equations did not get rendered due to their size.

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNormedAddCommGroup : NormedAddCommGroup ConfigurationSpace

Equations

• One or more equations did not get rendered due to their size.

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNormedSpaceReal : NormedSpace ℝ ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instNormedSpaceReal = { toModule := ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instModuleReal, norm_smul_le := ⋯ }

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instInnerReal : Inner ℝ ConfigurationSpace

Equations

• ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instInnerReal = { inner := fun (x y : ClassicalMechanics.HarmonicOscillator.ConfigurationSpace) => x.val * y.val }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.inner_def (x y : ConfigurationSpace) : inner ℝ x y = x.val * y.val

noncomputable instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instInnerProductSpaceReal : InnerProductSpace ℝ ConfigurationSpace

Equations

• One or more equations did not get rendered due to their size.

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.differentiable_inner_self : Differentiable ℝ fun (x : ConfigurationSpace) => inner ℝ x x

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.differentiableAt_inner_self (x : ConfigurationSpace) : DifferentiableAt ℝ (fun (y : ConfigurationSpace) => inner ℝ y y) x

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.contDiff_inner_self (n : WithTop ℕ∞) : ContDiff ℝ n fun (x : ConfigurationSpace) => inner ℝ x x

noncomputable def ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.toRealLM : ConfigurationSpace →ₗ[ℝ] ℝ

Linear map sending a configuration space element to its underlying real value.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.fromRealLM : ℝ →ₗ[ℝ] ConfigurationSpace

Linear map embedding a real value into the configuration space.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.toRealCLM : ConfigurationSpace →L[ℝ] ℝ

Continuous linear map sending a configuration space element to its underlying real value.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.fromRealCLM : ℝ →L[ℝ] ConfigurationSpace

Continuous linear map embedding a real value into the configuration space.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.valHomeomorphism : ConfigurationSpace ≃ₜ ℝ

Homeomorphism between configuration space and ℝ given by ConfigurationSpace.val.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instChartedSpaceReal : ChartedSpace ℝ ConfigurationSpace

The structure of a charted space on ConfigurationSpace.

Equations

• One or more equations did not get rendered due to their size.

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instIsManifoldRealModelWithCornersSelfTopWithTopENat : IsManifold (modelWithCornersSelf ℝ ℝ) ⊤ ConfigurationSpace

The structure of a smooth manifold on ConfigurationSpace.

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instFiniteDimensionalReal : FiniteDimensional ℝ ConfigurationSpace

instance ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.instCompleteSpace : CompleteSpace ConfigurationSpace

Map to space

def ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.toSpace (q : ConfigurationSpace) : Space 1

The position in one-dimensional space associated to the configuration.

Equations

• q.toSpace = { val := fun (x : Fin 1) => q.val }

@[simp]

theorem ClassicalMechanics.HarmonicOscillator.ConfigurationSpace.toSpace_apply (q : ConfigurationSpace) (i : Fin 1) : q.toSpace.val i = q.val