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

A. The definition of the free space type

structure Electromagnetism.FreeSpace : Type

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

• ε₀ : ℝ

  The permittivity.

• μ₀ : ℝ

  The permeability.

• ε₀_pos : 0 < self.ε₀
• μ₀_pos : 0 < self.μ₀

B. Positivity properties

@[simp]

theorem Electromagnetism.FreeSpace.ε₀_nonneg (𝓕 : FreeSpace) : 0 ≤ 𝓕.ε₀

@[simp]

theorem Electromagnetism.FreeSpace.μ₀_nonneg (𝓕 : FreeSpace) : 0 ≤ 𝓕.μ₀

@[simp]

theorem Electromagnetism.FreeSpace.ε₀_ne_zero (𝓕 : FreeSpace) : 𝓕.ε₀ ≠ 0

@[simp]

theorem Electromagnetism.FreeSpace.μ₀_ne_zero (𝓕 : FreeSpace) : 𝓕.μ₀ ≠ 0

C. The speed of light

noncomputable def Electromagnetism.FreeSpace.c (𝓕 : FreeSpace) : SpeedOfLight

The speed of light in free space.

Equations

• 𝓕.c = { val := 1 / √(𝓕.ε₀ * 𝓕.μ₀), pos := ⋯ }

theorem Electromagnetism.FreeSpace.c_val (𝓕 : FreeSpace) : 𝓕.c.val = 1 / √(𝓕.ε₀ * 𝓕.μ₀)

theorem Electromagnetism.FreeSpace.c_sq (𝓕 : FreeSpace) : 𝓕.c.val ^ 2 = 1 / (𝓕.ε₀ * 𝓕.μ₀)

@[simp]

theorem Electromagnetism.FreeSpace.c_abs (𝓕 : FreeSpace) : |𝓕.c.val| = 𝓕.c.val