Physlib.Electromagnetism.Dynamics.Basic

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.Relativity.SpeedOfLight
public import Mathlib.Analysis.Real.Sqrt

Free space

i. Overview

In this module we define a type FreeSpace which encapsulates the electric permittivity and magnetic permeability of free space, that is the physical constants which make it up.

We prove basic properties from this definition, and define the speed of light in free space in terms of these constants.

ii. Key results

FreeSpace : The structure encapsulating the electric permittivity and magnetic permeability of free space.

FreeSpace.c : The speed of light in free space.

iii. Table of contents

A. The definition of the free space type

B. Positivity properties

C. The speed of light

iv. References

@[expose] public section

A. The definition of the free space type

Free space consists of the specification of the electric permittivity and the magnetic permeability.

The permittivity.

The permeability.

              structure FreeSpace where  ε₀ : ℝ  μ₀ : ℝ
  ε₀_pos : 0 < ε₀
  μ₀_pos : 0 < μ₀

B. Positivity properties

              @[simp]
lemma ε₀_nonneg : 0 ≤ 𝓕.ε₀ := le_of_lt 𝓕.ε₀_pos@[simp]
lemma μ₀_nonneg : 0 ≤ 𝓕.μ₀ := le_of_lt 𝓕.μ₀_pos@[simp]
lemma ε₀_ne_zero : 𝓕.ε₀ ≠ 0 := ne_of_gt 𝓕.ε₀_pos@[simp]
lemma μ₀_ne_zero : 𝓕.μ₀ ≠ 0 := ne_of_gt 𝓕.μ₀_pos

C. The speed of light

              lemma c_val : (𝓕.c : ℝ) = 1 / √(𝓕.ε₀ * 𝓕.μ₀) := rfl

lemma c_sq : (𝓕.c : ℝ) ^ 2 = 1 / (𝓕.ε₀ * 𝓕.μ₀) := by𝓕:FreeSpace⊢ 𝓕.c.val ^ 2 = 1 / (𝓕.ε₀ * 𝓕.μ₀)
  rw [c_val,𝓕:FreeSpace⊢ (1 / √(𝓕.ε₀ * 𝓕.μ₀)) ^ 2 = 1 / (𝓕.ε₀ * 𝓕.μ₀)𝓕:FreeSpace⊢ 1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹ * (1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹) = 1 / (𝓕.ε₀ * 𝓕.μ₀) sq,𝓕:FreeSpace⊢ 1 / √(𝓕.ε₀ * 𝓕.μ₀) * (1 / √(𝓕.ε₀ * 𝓕.μ₀)) = 1 / (𝓕.ε₀ * 𝓕.μ₀)𝓕:FreeSpace⊢ 1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹ * (1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹) = 1 / (𝓕.ε₀ * 𝓕.μ₀) div_eq_mul_inv𝓕:FreeSpace⊢ 1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹ * (1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹) = 1 / (𝓕.ε₀ * 𝓕.μ₀)𝓕:FreeSpace⊢ 1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹ * (1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹) = 1 / (𝓕.ε₀ * 𝓕.μ₀)]𝓕:FreeSpace⊢ 1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹ * (1 * (√(𝓕.ε₀ * 𝓕.μ₀))⁻¹) = 1 / (𝓕.ε₀ * 𝓕.μ₀)
  field_simp𝓕:FreeSpace⊢ 𝓕.ε₀ * 𝓕.μ₀ = √(𝓕.ε₀ * 𝓕.μ₀) ^ 2
  refine (Real.sqrt_eq_iff_eq_sq ?_ ?_).mp rflrefine_1𝓕:FreeSpace⊢ 0 ≤ 𝓕.ε₀ * 𝓕.μ₀refine_2𝓕:FreeSpace⊢ 0 ≤ √(𝓕.ε₀ * 𝓕.μ₀)
  ·refine_1𝓕:FreeSpace⊢ 0 ≤ 𝓕.ε₀ * 𝓕.μ₀ apply mul_nonneg 𝓕.ε₀_nonneg 𝓕.μ₀_nonnegAll goals completed! 🐙
  ·refine_2𝓕:FreeSpace⊢ 0 ≤ √(𝓕.ε₀ * 𝓕.μ₀) positivityAll goals completed! 🐙

@[simp]
lemma c_abs : abs (𝓕.c : ℝ) = 𝓕.c := by𝓕:FreeSpace⊢ |𝓕.c.val| = 𝓕.c.val
  rw [abs_of_pos (SpeedOfLight.val_pos 𝓕.c)𝓕:FreeSpace⊢ 𝓕.c.val = 𝓕.c.valAll goals completed! 🐙]All goals completed! 🐙