Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Basic

For any two configurations $p$ and $q$ in the configuration space of a simple pendulum, if their angles (represented as elements of $\mathbb{R}/2\pi\mathbb{Z}$, denoted by `Real.Angle`) are equal, then the configurations $p$ and $q$ are equal.

The equivalence $\text{angleEquiv}$ defines a bijection between the configuration space of a simple pendulum, denoted by $\text{ConfigurationSpace}$, and the set of angles modulo $2\pi$, denoted by $\text{Real.Angle} \cong \mathbb{R}/2\pi\mathbb{Z}$. It maps a configuration $q$ to its corresponding angle $\theta$ and provides the inverse mapping from an angle back to a configuration.

The topological space structure on the configuration space of a simple pendulum is the topology induced by the mapping to the space of angles $\mathbb{R}/2\pi\mathbb{Z}$.

The mapping between the configuration space of a simple pendulum, denoted as $\text{ConfigurationSpace}$, and the space of angles modulo $2\pi$, denoted as $\text{Real.Angle} \cong \mathbb{R}/2\pi\mathbb{Z}$, is a homeomorphism. This identifies a physical configuration with its angular displacement from the downward vertical in a way that is both bijective and bicontinuous under the induced topology.

For a configuration $q$ of a simple pendulum with an angle $\theta$, this function returns the corresponding point on the unit circle $S^1 \subset \mathbb{C}$ given by $e^{i\theta}$.

The homeomorphism $\text{ConfigurationSpace} \cong S^1$ identifies the configuration space of a simple pendulum with the unit circle $S^1 \subset \mathbb{C}$. This map is the composition of the homeomorphism between the configuration space and the space of angles modulo $2\pi$ ($\text{Real.Angle}$) with the standard homeomorphism from the additive circle $\mathbb{R}/2\pi\mathbb{Z}$ to the unit circle.

For any configuration $q$ in the configuration space of a simple pendulum, the value of the homeomorphism $\text{circleHomeomorph}$ (which identifies the configuration space with the unit circle $S^1 \subset \mathbb{C}$) applied to $q$ is equal to $q.\text{toCircle}$.

The function maps a point $z$ on the unit circle $S^1 \subset \mathbb{C}$ to its corresponding configuration in the pendulum's configuration space. It is defined as the inverse of the homeomorphism $\text{ConfigurationSpace} \cong S^1$.

For any point $z$ on the unit circle $S^1 \subset \mathbb{C}$, applying the map $\text{ofCircle}$ to obtain a configuration and then applying the map $\text{toCircle}$ returns the original point $z$. That is, $\text{toCircle}(\text{ofCircle}(z)) = z$.

For any configuration $q$ in the configuration space of a simple pendulum, let $\text{toCircle}(q)$ be the corresponding point on the unit circle $S^1 \subset \mathbb{C}$. If we apply the inverse map $\text{ofCircle}$, which maps a point on the unit circle back to the configuration space, we recover the original configuration: $\text{ofCircle}(\text{toCircle}(q)) = q$.

The configuration space of the simple pendulum is a Hausdorff space ($T_2$ space). This property follows from the fact that the configuration space is homeomorphic to the unit circle.

The configuration space of the simple pendulum is a compact topological space. This follows from its identification via homeomorphism with the unit circle $S^1$.

The configuration space of the simple pendulum, which is homeomorphic to the unit circle $S^1$, satisfies the second-countability axiom (i.e., its topology has a countable base).

The configuration space of a simple pendulum is endowed with the structure of a charted space modeled on the 1-dimensional Euclidean space $\mathbb{R}^1$. This structure is defined by pulling back the atlas of the unit circle $S^1 \subset \mathbb{C}$ via the homeomorphism $\Phi: \text{ConfigurationSpace} \cong S^1$. Specifically, for any point $q$ in the configuration space, the local chart at $q$ is the composition of $\Phi$ and the standard chart of the unit circle at the point $\Phi(q)$.

For any configuration $q$ in the configuration space of a simple pendulum, the local chart $\varphi_q$ at $q$ (modeled on the 1-dimensional Euclidean space $\mathbb{R}^1$) is equal to the composition of the homeomorphism $\Phi: \text{ConfigurationSpace} \cong S^1$ and the standard chart $\psi_{\Phi(q)}$ of the unit circle $S^1$ at the point $\Phi(q)$.

For any configuration $q$ in the configuration space $\mathcal{C}$ of a simple pendulum, the domain (source) of the local chart at $q$ is the preimage under the homeomorphism $\Phi: \mathcal{C} \cong S^1$ (which identifies the configuration space with the unit circle) of the domain of the standard local chart of the unit circle at the point $\Phi(q)$. Mathematically, let $\psi_q$ be the chart at $q \in \mathcal{C}$ and $\varphi_{\Phi(q)}$ be the chart at $\Phi(q) \in S^1$; then $\text{source}(\psi_q) = \Phi^{-1}(\text{source}(\varphi_{\Phi(q)}))$.

For any configuration $q$ in the configuration space of a simple pendulum, the target (codomain) of the local chart at $q$—modeled on the 1-dimensional Euclidean space $\mathbb{R}^1$—is identical to the target of the local chart of the unit circle $S^1$ at the corresponding point $\text{toCircle}(q)$.

The configuration space of the simple pendulum is a one-dimensional real-analytic manifold modeled on the Euclidean space $\mathbb{R}^1$. This implies that the transition functions between coordinate charts are real-analytic (of class $C^\omega$).

This function maps a real number $\theta$, representing the angle of the pendulum rod measured from the downward vertical, to its corresponding point in the configuration space. Since the configuration space of a simple pendulum is topologically a circle, this map corresponds to the quotient map $\mathbb{R} \to \mathbb{R} / 2\pi\mathbb{Z}$, where angles $\theta$ and $\theta + 2\pi n$ (for $n \in \mathbb{Z}$) describe the same physical position.

For any real number $\theta$, let $\text{ofAngle}(\theta)$ denote the configuration of a simple pendulum at that angle. The angle associated with this configuration is equal to $\theta$ modulo $2\pi$.

For any angle $\theta \in \mathbb{R}$, the configuration of the simple pendulum at angle $\theta + 2\pi$ is the same as the configuration at angle $\theta$. Here, $\text{ofAngle}(\theta)$ represents the map from a real-valued angle (measured from the downward vertical) to the configuration space.

The angular lift $\text{ofAngle} : \mathbb{R} \to \text{ConfigurationSpace}$, which maps a real angle $\theta$ (measured from the downward vertical) to a state in the pendulum's configuration space, is periodic with period $2\pi$. That is, for any $\theta \in \mathbb{R}$, $\text{ofAngle}(\theta + 2\pi) = \text{ofAngle}(\theta)$.

Two real angles $\theta_1$ and $\theta_2$ correspond to the same physical configuration of the simple pendulum if and only if they differ by an integer multiple of $2\pi$; that is, $\text{ofAngle}(\theta_1) = \text{ofAngle}(\theta_2)$ if and only if there exists an integer $n \in \mathbb{Z}$ such that $\theta_2 = \theta_1 + 2\pi n$.

The map $\text{ofAngle} : \mathbb{R} \to \text{ConfigurationSpace}$, which assigns a configuration of the simple pendulum to a real angle $\theta$ (measured from the downward vertical), is surjective. That is, for every configuration $c$ in the configuration space, there exists at least one real angle $\theta \in \mathbb{R}$ such that $\text{ofAngle}(\theta) = c$.

The map $\text{ofAngle} : \mathbb{R} \to \text{ConfigurationSpace}$, which maps a real angle $\theta$ (measured from the downward vertical) to its corresponding point in the pendulum's configuration space, is continuous.

The map $\text{ofAngle} : \mathbb{R} \to \text{ConfigurationSpace}$, which maps a real number $\theta$ representing the angle of the pendulum rod from the downward vertical to its corresponding point in the pendulum's configuration space, is a covering map.

For any angle $\theta \in \mathbb{R}$, the image of the pendulum configuration $\text{ofAngle}(\theta)$ (representing the rod at angle $\theta$ from the downward vertical) under the identification map to the unit circle is equal to $e^{i\theta}$ (denoted by `Circle.exp θ`).

For any angle $\theta \in \mathbb{R}$, the configuration in the pendulum's configuration space corresponding to the point $e^{i\theta}$ on the unit circle is equal to the configuration at angle $\theta$ from the downward vertical. Mathematically, this is expressed as $\text{ofCircle}(e^{i\theta}) = \text{ofAngle}(\theta)$, where $e^{i\theta}$ is the exponential map from the real line to the unit circle.

The map $\text{ofAngle} : \mathbb{R} \to \text{ConfigurationSpace}$, which maps a real angle $\theta$ to the corresponding position of a simple pendulum, is real analytic (of class $\mathcal{C}^\omega$) with respect to the standard manifold structures on $\mathbb{R}$ and the configuration space.

Given a configuration $q$ in the configuration space of a simple pendulum, this function returns the cosine of its angle. If the configuration $q$ is represented by an angle $\theta \in \mathbb{R}/2\pi\mathbb{Z}$ measured from the downward vertical, then the value is $\cos \theta$.

For a configuration $q$ in the configuration space of a simple pendulum, this function returns the sine of its associated angle $\theta$, denoted as $\sin \theta$.

For any configuration $q$ in the configuration space of a simple pendulum, the cosine of the configuration $q$ is equal to the cosine of its associated angle $q.\text{angle} \in \mathbb{R}/2\pi\mathbb{Z}$ (measured from the downward vertical).

For any configuration $q$ in the configuration space of a simple pendulum, the sine of the configuration $q$ is equal to the sine of its associated angle, denoted as $\sin q = \sin(\text{angle } q)$. Here, $\text{angle } q$ refers to the configuration represented as an element of the circle $\mathbb{R}/2\pi\mathbb{Z}$ (i.e., `Real.Angle`).

For any real number $\theta$, the cosine of the pendulum configuration corresponding to the angle $\theta$ (measured from the downward vertical) is equal to $\cos \theta$.

For any real number $\theta$, the sine of the pendulum configuration corresponding to angle $\theta$ is equal to the trigonometric sine of $\theta$, denoted as $(\text{ofAngle } \theta).\sin = \sin \theta$.

For any configuration $q$ in the configuration space of a simple pendulum, the cosine and sine of its angle (denoted as $\cos q$ and $\sin q$ respectively) satisfy the Pythagorean identity: $$\cos^2 q + \sin^2 q = 1.$$

The function $\cos: \text{ConfigurationSpace} \to \mathbb{R}$, which maps a configuration $q$ of a simple pendulum to the cosine of its angle, is continuous.

The function $\sin : \text{ConfigurationSpace} \to \mathbb{R}$, which maps each configuration of a simple pendulum to the sine of its angular position, is continuous.

Given a rod of length $\ell \in \mathbb{R}$ and a configuration $q$ in the configuration space, this function returns the position of the pendulum bob in $\mathbb{R}^2$ as the vector $(\ell \sin q, -\ell \cos q)$. The pivot is located at the origin, the first coordinate represents the horizontal position, and the second coordinate represents the vertical position (pointing upwards). The bob is located at a distance $|\ell|$ from the pivot.

For a simple pendulum with rod length $\ell \in \mathbb{R}$ and configuration $q$ in the configuration space, the horizontal coordinate (the component at index 0) of the bob's position is equal to $\ell \sin q$.

For a simple pendulum with rod length $\ell \in \mathbb{R}$ and configuration $q$, the second component (the vertical coordinate) of the position of the bob in physical space, $\text{toSpace}(\ell, q)$, is equal to $-\ell \cos q$.

For a simple pendulum with rod length $\ell \in \mathbb{R}$ and an angle $\theta \in \mathbb{R}$ measured from the downward vertical, the position of the bob in the plane is given by the vector $(\ell \sin \theta, -\ell \cos \theta)$. Here, the pivot is at the origin $(0, 0)$, the first coordinate represents the horizontal axis, and the second coordinate represents the vertical axis pointing upwards.

For a simple pendulum with rod length $\ell \in \mathbb{R}$ and configuration $q$ (representing the angle from the downward vertical), the Euclidean norm of the bob's position vector $\text{toSpace } \ell \ q$ is equal to the absolute value of the rod length: $$\|\text{toSpace } \ell \ q\| = |\ell|$$ This equality expresses the rod-length constraint, where the bob's position in $\mathbb{R}^2$ is given by $(\ell \sin q, -\ell \cos q)$ relative to a pivot at the origin.

For any rod length $\ell \in \mathbb{R}$, the mapping $\text{toSpace } \ell: \text{ConfigurationSpace} \to \text{Space } 2$, which sends a configuration $q$ to the physical position $(\ell \sin q, -\ell \cos q)$ of the pendulum bob in the plane, is continuous.

For a simple pendulum with a rod of length $\ell \in \mathbb{R}$, if $\ell \neq 0$, then the map $\text{toSpace } \ell$ from the configuration space to the physical space $\mathbb{R}^2$ is injective. This implies that the configuration of the pendulum is uniquely determined by the position of its bob.

For a rod length $\ell \in \mathbb{R}$ such that $\ell \neq 0$, the map $f_\ell: \mathcal{C} \to \mathbb{R}^2$ from the configuration space $\mathcal{C}$ of the simple pendulum to the plane, defined by $q \mapsto (\ell \sin q, -\ell \cos q)$, is a closed embedding.