Physlib.ClassicalMechanics.RigidBody.SolidSphere

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.ClassicalMechanics.RigidBody.Basic
public import Physlib.SpaceAndTime.Space.Integrals.Basic
public import Physlib.Meta.Linters.Sorry

The solid sphere as a rigid body

In this module we consider the solid sphere as a rigid body, and compute its mass, center of mass and inertia tensor.

@[expose] public section



lemma solidSphere_mass {d : ℕ} (m R : ℝ≥0) (hr : R ≠ 0) : (solidSphere d m R).mass = m := byd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ (solidSphere d m R).mass = ↑m
  simp only [mass, solidSphere]d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ { toFun := fun f => ↑m / volume.real (Metric.closedBall 0 ↑R) * ∫ (x : Space d) in Metric.closedBall 0 ↑R, f x,
      map_add' := ⋯, map_smul' := ⋯ }
    ⟨fun x => 1, ⋯⟩ =
  ↑m
  simp only [LinearMap.coe_mk, AddHom.coe_mk, ContMDiffMap.coeFn_mk, integral_const,
    MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter, smul_eq_mul, mul_one]d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
  have h1 : (@volume (Space d) measureSpaceOfInnerProductSpace).real
      (Metric.closedBall 0 R) ≠ 0 := byd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ (solidSphere d m R).mass = ↑md:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
    refine (measureReal_ne_zero_iff ?_).mpr ?_refine_1d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ volume (Metric.closedBall 0 ↑R) ≠ ⊤refine_2d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ volume (Metric.closedBall 0 ↑R) ≠ 0d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
    ·refine_1d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ volume (Metric.closedBall 0 ↑R) ≠ ⊤d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m apply measure_closedBall_lt_top.neAll goals completed! 🐙d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
    ·refine_2d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ volume (Metric.closedBall 0 ↑R) ≠ 0d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m apply (Metric.measure_closedBall_pos volume _ _).ne'd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ 0 < ↑Rd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
      have hr' := R.2d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0hr':0 ≤ ↑R⊢ 0 < ↑Rd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
      have hx : R.1 ≠ 0 := byd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ (solidSphere d m R).mass = ↑md:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0hr':0 ≤ ↑Rhx:↑R ≠ 0⊢ 0 < ↑Rd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m simpa using hrd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0hr':0 ≤ ↑Rhx:↑R ≠ 0⊢ 0 < ↑Rd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑md:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0hr':0 ≤ ↑Rhx:↑R ≠ 0⊢ 0 < ↑Rd:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
      apply lt_of_le_of_ne hr' (Ne.symm hx)d:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑md:ℕm:ℝ≥0R:ℝ≥0hr:R ≠ 0h1:volume.real (Metric.closedBall 0 ↑R) ≠ 0⊢ ↑m / volume.real (Metric.closedBall 0 ↑R) * volume.real (Metric.closedBall 0 ↑R) = ↑m
  field_simpAll goals completed! 🐙

The center of mass of a solid sphere located at the origin is 0.


lemma solidSphere_centerOfMass {d : ℕ} (m R : ℝ≥0) : (solidSphere d m R).centerOfMass = 0 := byd:ℕm:ℝ≥0R:ℝ≥0⊢ (solidSphere d m R).centerOfMass = 0
  ext id:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ (solidSphere d m R).centerOfMass.val i = Space.val 0 i
  simp only [centerOfMass, solidSphere, one_div, LinearMap.coe_mk, AddHom.coe_mk,
    ContMDiffMap.coeFn_mk, smul_eq_mul, Space.zero_apply, mul_eq_zero, inv_eq_zero, div_eq_zero_iff,
    coe_eq_zero]d:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ {
        ρ :=
          {
            toFun := fun f =>
              ↑m / volume.real (Metric.closedBall 0 ↑R) * ∫ (x : Space d) in Metric.closedBall 0 ↑R, f x,
            map_add' := ⋯, map_smul' := ⋯ } }.mass =
    0 ∨
  (m = 0 ∨ volume.real (Metric.closedBall 0 ↑R) = 0) ∨ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = 0
  rightd:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ (m = 0 ∨ volume.real (Metric.closedBall 0 ↑R) = 0) ∨ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = 0
  rightd:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = 0
  suffices ∫ x in Metric.closedBall (0 : Space d) R, x i ∂MeasureSpace.volume
    = -∫ x in Metric.closedBall (0 : Space d) R, x i ∂MeasureSpace.volume byd:ℕm:ℝ≥0R:ℝ≥0i:Fin dthis:∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = -∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = 0d:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = -∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i linarithd:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = -∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val id:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = -∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i
  rw [← integral_negd:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = ∫ (a : Space d) in Metric.closedBall 0 ↑R, -a.val id:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = ∫ (a : Space d) in Metric.closedBall 0 ↑R, -a.val i]d:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ ∫ (x : Space d) in Metric.closedBall 0 ↑R, x.val i = ∫ (a : Space d) in Metric.closedBall 0 ↑R, -a.val i
  simp only [← integral_indicator measurableSet_closedBall, Set.indicator, Metric.mem_closedBall]d:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ (∫ (x : Space d), if dist x 0 ≤ ↑R then x.val i else 0) = ∫ (x : Space d), if dist x 0 ≤ ↑R then -x.val i else 0
  rw [← integral_neg_eq_selfd:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ (∫ (x : Space d), if dist (-x) 0 ≤ ↑R then (-x).val i else 0) = ∫ (x : Space d), if dist x 0 ≤ ↑R then -x.val i else 0d:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ (∫ (x : Space d), if dist (-x) 0 ≤ ↑R then (-x).val i else 0) = ∫ (x : Space d), if dist x 0 ≤ ↑R then -x.val i else 0]d:ℕm:ℝ≥0R:ℝ≥0i:Fin d⊢ (∫ (x : Space d), if dist (-x) 0 ≤ ↑R then (-x).val i else 0) = ∫ (x : Space d), if dist x 0 ≤ ↑R then -x.val i else 0
  norm_numAll goals completed! 🐙

The moment of inertia tensor of a solid sphere through its center of mass is 2/5 m R^2 * I.

@[sorryful]
lemma declaration uses `sorry`solidSphere_inertiaTensor (m R : ℝ≥0) (hr : R ≠ 0) :
    (solidSphere 3 m R).inertiaTensor = (2/5 * m.1 * R.1^2) • (1 : Matrix _ _ _) := bym:ℝ≥0R:ℝ≥0hr:R ≠ 0⊢ (solidSphere 3 m R).inertiaTensor = (2 / 5 * ↑m * ↑R ^ 2) • 1
  sorryAll goals completed! 🐙