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 Mathlib.Analysis.RCLike.BasicThe units of charge
A unit of charge corresponding to a choice of translationally-invariant
metric on the charge manifold (to be defined diffeomorphic to ℝ).
Such a choice is (non-canonically) equivalent to a
choice of positive real number. We define the type ChargeUnit to be equivalent to the
positive reals.
We assume that the charge manifold is already defined with an orientation, with the electron being in the negative direction.
On ChargeUnit there is an instance of division giving a real number, corresponding to the
ratio of the two scales of temperature unit.
To define specific charge units, we first state the existence of a a given charge unit, and then construct all other charge units from it. We choose to state the existence of the charge unit of the coulomb, and construct all other charge units from that.
@[expose] public sectionThe choices of translationally-invariant metrics on the charge-manifold. Such a choice corresponds to a choice of units for charge. This assumes that an orientation has already being picked on the charge manifold.
The underlying scale of the unit.
structure ChargeUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : ChargeUnit) : x.val ≠ 0 := x:ChargeUnit⊢ x.val ≠ 0
All goals completed! 🐙lemma val_pos (x : ChargeUnit) : 0 < x.val := x.propertyinstance : Inhabited ChargeUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩Division of ChargeUnit
lemma div_eq_val (x y : ChargeUnit) :
x / y = (⟨x.val / y.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt y.val_pos)⟩ : ℝ≥0) := rflx:ChargeUnity:ChargeUnit⊢ ¬⟨x.val / y.val, ⋯⟩ = 0
x:ChargeUnity:ChargeUnit⊢ ↑⟨x.val / y.val, ⋯⟩ ≠ 0
All goals completed! 🐙@[simp]
lemma div_pos (x y : ChargeUnit) : (0 : ℝ≥0) < x/ y := x:ChargeUnity:ChargeUnit⊢ 0 < x / y
x:ChargeUnity:ChargeUnit⊢ 0 ≤ x / yx:ChargeUnity:ChargeUnit⊢ 0 ≠ x / y
x:ChargeUnity:ChargeUnit⊢ 0 ≤ x / y All goals completed! 🐙
x:ChargeUnity:ChargeUnit⊢ 0 ≠ x / y All goals completed! 🐙@[simp]
lemma div_self (x : ChargeUnit) :
x / x = (1 : ℝ≥0) := x:ChargeUnit⊢ x / x = 1
x:ChargeUnit⊢ ⟨1, ⋯⟩ = 1
All goals completed! 🐙All goals completed! 🐙@[simp]
lemma div_mul_div_coe (x y z : ChargeUnit) :
(x / y : ℝ) * (y / z : ℝ) = x / z := x:ChargeUnity:ChargeUnitz:ChargeUnit⊢ ↑(x / y) * ↑(y / z) = ↑(x / z)
x:ChargeUnity:ChargeUnitz:ChargeUnit⊢ x.val / y.val * (y.val / z.val) = x.val / z.val
All goals completed! 🐙The scaling of a charge unit
The scaling of a charge unit by a positive real.
def scale (r : ℝ) (x : ChargeUnit) (hr : 0 < r := by norm_num) : ChargeUnit :=
⟨r * x.val, mul_pos hr x.val_pos⟩@[simp]
lemma scale_div_self (x : ChargeUnit) (r : ℝ) (hr : 0 < r) :
scale r x hr / x = (⟨r, le_of_lt hr⟩ : ℝ≥0) := x:ChargeUnitr:ℝhr:0 < r⊢ scale r x hr / x = ⟨r, ⋯⟩
All goals completed! 🐙@[simp]
lemma self_div_scale (x : ChargeUnit) (r : ℝ) (hr : 0 < r) :
x / scale r x hr = (⟨1/r, _root_.div_nonneg (x:ChargeUnitr:ℝhr:0 < r⊢ 0 ≤ 1 All goals completed! 🐙) (le_of_lt hr)⟩ : ℝ≥0) := x:ChargeUnitr:ℝhr:0 < r⊢ x / scale r x hr = ⟨1 / r, ⋯⟩
x:ChargeUnitr:ℝhr:0 < r⊢ ⟨x.val / (r * x.val), ⋯⟩ = ⟨r⁻¹, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_one (x : ChargeUnit) : scale 1 x = x := x:ChargeUnit⊢ scale 1 x ⋯ = x
All goals completed! 🐙x1:ChargeUnitx2:ChargeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ ↑⟨r1 * x1.val / (r2 * x2.val), ⋯⟩ = ↑⟨r1, ⋯⟩ / ↑⟨r2, ⋯⟩ * ↑⟨x1.val / x2.val, ⋯⟩
All goals completed! 🐙@[simp]
lemma scale_scale (x : ChargeUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) :
scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x (mul_pos hr1 hr2) := x:ChargeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x ⋯
x:ChargeUnitr1:ℝr2:ℝhr1:0 < r1hr2:0 < r2⊢ r1 * (r2 * x.val) = r1 * r2 * x.val
All goals completed! 🐙Specific choices of charge units
We define specific choices of charge units.
We first define the notion of a columb to correspond to the charge unit with underlying value
equal to 1. This is really down to a choice in the isomorphism between the set of metrics
on the charge manifold and the positive reals.
The definition of a charge unit of coulomb.
def coulombs : ChargeUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩