an example of a motion of an object

Stream: general

[Bulhwi Cha]

I think we can specify motions of objects and prove theorems about them as follows. But I still don't know how to formally define contact force and deformation.

import Mathlib.Analysis.SpecialFunctions.Pow.Real

open Set Real NNReal

/-- The region `D` at time `0` described in rectangular coordinates. This is a right circular
cylinder with radius `1` and height `2`, whose axis is the `z`-axis.
`D₀ = { (x, y, z) ∈ ℝ³ | x² + y² = 1 ∧ 0 ≤ z ≤ 2 }`. -/
def D₀ := { P : Fin 3 → ℝ | P 0 ^ 2 + P 1 ^ 2 = 1 ∧ 0 ≤ P 2 ∧ P 2 ≤ 2 }

/-- The motion of `D` on the time interval [0, 1]. `D` rotates about the `z`-axis with rotational
speed `2π` during that time interval. If `P = (x, y, z) ∈ D₀`, `(x, y) = (cos θ, sin θ)`, and
`t ∈ [0, 1]`, then `s (P, t) = (r cos (θ + 2πt), r sin (θ + 2πt), z)`. -/
noncomputable def s {P} (_hP : P ∈ D₀) {t : ℝ} (_ht : t ∈ Icc 0 1) : Fin 3 → ℝ
  | 0 => P 0 * cos (2 * π * t) - P 1 * sin (2 * π * t)
  | 1 => P 0 * sin (2 * π * t) + P 1 * cos (2 * π * t)
  | 2 => P 2

/-- The region `D` at time `t ∈ [0, 1]` described in rectangular coordinates.
`∀ t ∈ [0, 1], D (t) = { P ∈ ℝ³ | ∃ Q ∈ D₀, P = s (Q, t) }`. -/
def D {t : ℝ} (ht : t ∈ Icc 0 1) := { P : Fin 3 → ℝ | ∃ Q, ∃ (hQ : Q ∈ D₀), P = s hQ ht }

/-- The region `D` remains the same during the time interval [0, 1]. `∀ t ∈ [0, 1], D (t) = D₀`. -/
theorem D_anytime_eq_D₀ {t : ℝ} (ht : t ∈ Icc 0 1) : D ht = D₀ := by
  ext; rename_i P
  constructor <;> simp [D]
  · intro Q hQ eq
    subst eq
    constructor <;> [skip; exact hQ.2]
    show (Q 0 * cos (2 * π * t) - Q 1 * sin (2 * π * t)) ^ 2
       + (Q 0 * sin (2 * π * t) + Q 1 * cos (2 * π * t)) ^ 2 = 1
    simp [sub_sq', add_sq']; ring_nf
    simp [mul_comm, ← mul_add, cos_sq_add_sin_sq, one_mul, add_assoc]; simpa using hQ.1
  · intro hP
    let Q : Fin 3 → ℝ
      | 0 =>   P 0 * cos (2 * π * t) + P 1 * sin (2 * π * t)
      | 1 => - P 0 * sin (2 * π * t) + P 1 * cos (2 * π * t)
      | 2 => P 2
    have hQ : Q ∈ D₀ := by
      constructor <;> [skip; exact hP.2]
      show (  P 0 * cos (2 * π * t) + P 1 * sin (2 * π * t)) ^ 2
         + (- P 0 * sin (2 * π * t) + P 1 * cos (2 * π * t)) ^ 2 = 1
      simp [add_sq']; ring_nf; simp [mul_comm, ← mul_add, cos_sq_add_sin_sq, one_mul, add_assoc]
      simpa using hP.1
    use Q, hQ
    funext; rename_i i
    match i with
    | 0 =>
      show P 0 = (  P 0 * cos (2 * π * t) + P 1 * sin (2 * π * t)) * cos (2 * π * t)
               - (- P 0 * sin (2 * π * t) + P 1 * cos (2 * π * t)) * sin (2 * π * t)
      ring_nf; rw [← mul_add, cos_sq_add_sin_sq, mul_one]
    | 1 =>
      show P 1 = (  P 0 * cos (2 * π * t) + P 1 * sin (2 * π * t)) * sin (2 * π * t)
               + (- P 0 * sin (2 * π * t) + P 1 * cos (2 * π * t)) * cos (2 * π * t)
      ring_nf; rw [mul_comm, ← mul_add, cos_sq_add_sin_sq, mul_one]
    | 2 => rfl

[Bulhwi Cha]

We should be able to visualize solid figures like D and their motions like s.