From 78106cb32ac0b30932ee51ca5f453dd46625bec3 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 19 Feb 2026 14:31:03 +0000 Subject: [PATCH] feat: Static EM --- .../HarmonicOscillator/Basic.lean | 1 - .../Dynamics/CurrentDensity.lean | 40 ++++++++++++ .../Kinematics/EMPotential.lean | 28 ++++++++ .../Kinematics/ElectricField.lean | 5 ++ .../Kinematics/MagneticField.lean | 14 ++++ .../Kinematics/ScalarPotential.lean | 9 +++ .../Kinematics/VectorPotential.lean | 7 ++ .../PointParticle/OneDimension.lean | 55 ++++------------ .../PointParticle/ThreeDimension.lean | 65 +++++-------------- .../SpaceAndTime/Space/DistOfFunction.lean | 16 +++-- 10 files changed, 146 insertions(+), 94 deletions(-) diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean index 19275675..5d7b4a39 100644 --- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean +++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean @@ -110,7 +110,6 @@ structure HarmonicOscillator where namespace HarmonicOscillator - variable (S : HarmonicOscillator) @[simp] diff --git a/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean b/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean index c62fa484..a1a6eddc 100644 --- a/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean +++ b/PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import PhysLean.SpaceAndTime.SpaceTime.TimeSlice +import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist /-! # The Lorentz Current Density @@ -41,6 +42,7 @@ The current density is given in terms of the charge density `ρ` and the current - D. The Lorentz current density as a distribution - D.1. The underlying charge density - D.2. The underlying current density +- E. Of Static Charge density ## iv. References @@ -279,5 +281,43 @@ noncomputable def currentDensity (c : SpeedOfLight) : map_smul' r J := by simp +/-! + +## E. Of Static Charge density + +-/ + +/-- The Lorentz current density associated with a static charge density. -/ +noncomputable def ofStaticChargeDensity {d : ℕ} (c : SpeedOfLight) : + ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] DistLorentzCurrentDensity d where + toFun ρ := + let smul : ℝ →L[ℝ] Lorentz.Vector d := { + toFun := fun r => r • Lorentz.Vector.basis (Sum.inl 0), + map_add' x y := by simp [add_smul], + map_smul' r x := by simp [smul_smul] + } + smul ∘L ((SpaceTime.distTimeSlice c).symm (c.1 • Space.constantTime ρ)) + map_add' ρ1 ρ2 := by + simp [map_add, ContinuousLinearMap.comp_add] + map_smul' r ρ := by + simp [map_smul, ContinuousLinearMap.comp_smulₛₗ, RingHom.id_apply,] + rw [smul_comm] + +@[simp] +lemma ofStaticChargeDensity_currentDensity_eq_zero {d : ℕ} (c : SpeedOfLight) + (ρ : (Space d) →d[ℝ] ℝ) : + (ofStaticChargeDensity c ρ).currentDensity c = 0 := by + ext t i + simp [ofStaticChargeDensity, currentDensity, distTimeSlice, Space.constantTime] + +@[simp] +lemma ofStaticChargeDensity_chargeDensity_eq {d : ℕ} (c : SpeedOfLight) + (ρ : (Space d) →d[ℝ] ℝ) : + (ofStaticChargeDensity c ρ).chargeDensity c = Space.constantTime ρ := by + ext f + simp [ofStaticChargeDensity, chargeDensity, Lorentz.Vector.temporalCLM, distTimeSlice_apply] + rw [← distTimeSlice_apply] + simp + end DistLorentzCurrentDensity end Electromagnetism diff --git a/PhysLean/Electromagnetism/Kinematics/EMPotential.lean b/PhysLean/Electromagnetism/Kinematics/EMPotential.lean index f76046a3..11bc6489 100644 --- a/PhysLean/Electromagnetism/Kinematics/EMPotential.lean +++ b/PhysLean/Electromagnetism/Kinematics/EMPotential.lean @@ -455,6 +455,34 @@ lemma deriv_equivariant {d} {A : DistElectromagneticPotential d} (Λ : LorentzGroup d) : deriv (Λ • A) = Λ • deriv A := by rw [deriv, distTensorDeriv_equivariant] +/-! + +## D. Construction of the electromagnetic potential from a scalar and vector potential + +-/ + +/-! + +## D.1. The electromagnetic potential of a scalar potential + +-/ + +/-- The electromagnetic potential of a scalar potential. -/ +noncomputable def ofScalarPotential {d} (c : SpeedOfLight) : + ((Time × Space d) →d[ℝ] ℝ) →ₗ[ℝ] DistElectromagneticPotential d where + toFun ρ := + let smul : ℝ →L[ℝ] Lorentz.Vector d := { + toFun := fun r => r • Lorentz.Vector.basis (Sum.inl 0), + map_add' x y := by simp [add_smul], + map_smul' r x := by simp [smul_smul] + } + smul ∘L ((SpaceTime.distTimeSlice c).symm (c.1⁻¹ • ρ)) + map_add' ρ1 ρ2 := by + simp [map_add, ContinuousLinearMap.comp_add] + map_smul' r ρ := by + simp [map_smul, ContinuousLinearMap.comp_smulₛₗ] + rw [smul_comm] + end DistElectromagneticPotential end Electromagnetism diff --git a/PhysLean/Electromagnetism/Kinematics/ElectricField.lean b/PhysLean/Electromagnetism/Kinematics/ElectricField.lean index 9a9024a8..1ca43f46 100644 --- a/PhysLean/Electromagnetism/Kinematics/ElectricField.lean +++ b/PhysLean/Electromagnetism/Kinematics/ElectricField.lean @@ -401,6 +401,11 @@ lemma electricField_eq_fieldStrength {d} {c : SpeedOfLight} field_simp ring +lemma ofScalarPotential_electricField {d} (c : SpeedOfLight) + (V : (Time × Space d) →d[ℝ] ℝ) : + (ofScalarPotential c V).electricField c = - Space.distSpaceGrad V := by + simp [electricField] + end DistElectromagneticPotential end Electromagnetism diff --git a/PhysLean/Electromagnetism/Kinematics/MagneticField.lean b/PhysLean/Electromagnetism/Kinematics/MagneticField.lean index db43e67c..cff819f9 100644 --- a/PhysLean/Electromagnetism/Kinematics/MagneticField.lean +++ b/PhysLean/Electromagnetism/Kinematics/MagneticField.lean @@ -695,5 +695,19 @@ lemma magneticFieldMatrix_one_dim_eq_zero {c : SpeedOfLight} rw [magneticFieldMatrix_eq_vectorPotential] simp +/-! + +### D.4. Magnetic field matrix of scalar potentials + +-/ + +@[simp] +lemma ofScalarPotential_magneticFieldMatrix {c : SpeedOfLight} + (V : (Time × Space d) →d[ℝ] ℝ) : + (ofScalarPotential c V).magneticFieldMatrix c = 0 := by + ext ε + rw [magneticFieldMatrix_eq_vectorPotential] + simp + end DistElectromagneticPotential end Electromagnetism diff --git a/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean b/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean index 6d4a3f72..6281d5b0 100644 --- a/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean +++ b/PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean @@ -162,5 +162,14 @@ noncomputable def scalarPotential {d} (c : SpeedOfLight) : Function.comp_apply, Pi.smul_apply, smul_eq_mul, Real.ringHom_apply] ring +@[simp] +lemma ofScalarPotential_scalarPotential {d} (c : SpeedOfLight) + (V : (Time × Space d) →d[ℝ] ℝ) : + (ofScalarPotential c V).scalarPotential c = V := by + ext ε + simp [ofScalarPotential, scalarPotential, Lorentz.Vector.temporalCLM, distTimeSlice_apply] + rw [← distTimeSlice_apply] + simp + end DistElectromagneticPotential end Electromagnetism diff --git a/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean b/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean index d8cb943d..7da35f39 100644 --- a/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean +++ b/PhysLean/Electromagnetism/Kinematics/VectorPotential.lean @@ -178,6 +178,13 @@ noncomputable def vectorPotential {d} (c : SpeedOfLight) : Pi.smul_apply, Function.comp_apply, Real.ringHom_apply, PiLp.smul_apply, smul_eq_mul] +@[simp] +lemma ofScalarPotential_vectorPotential {d} (c : SpeedOfLight) + (V : (Time × Space d) →d[ℝ] ℝ) : + (ofScalarPotential c V).vectorPotential c = 0 := by + ext ε + simp [ofScalarPotential, vectorPotential, Lorentz.Vector.spatialCLM, distTimeSlice_apply] + end DistElectromagneticPotential end Electromagnetism diff --git a/PhysLean/Electromagnetism/PointParticle/OneDimension.lean b/PhysLean/Electromagnetism/PointParticle/OneDimension.lean index e8f72a74..56471899 100644 --- a/PhysLean/Electromagnetism/PointParticle/OneDimension.lean +++ b/PhysLean/Electromagnetism/PointParticle/OneDimension.lean @@ -53,38 +53,26 @@ namespace DistElectromagneticPotential /-- The current density of a point particle stationary at the origin of 1d space. -/ noncomputable def oneDimPointParticleCurrentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : - DistLorentzCurrentDensity 1 := (SpaceTime.distTimeSlice c).symm <| - constantTime ((c * q) • diracDelta' ℝ r₀ (Lorentz.Vector.basis (Sum.inl 0))) + DistLorentzCurrentDensity 1 := .ofStaticChargeDensity c (q • diracDelta ℝ r₀) lemma oneDimPointParticleCurrentDensity_eq_distTranslate (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : - oneDimPointParticleCurrentDensity c q r₀ = ((SpaceTime.distTimeSlice c).symm <| - constantTime <| - distTranslate (basis.repr r₀) <| - ((c * q) • diracDelta' ℝ 0 (Lorentz.Vector.basis (Sum.inl 0)))) := by + oneDimPointParticleCurrentDensity c q r₀ = + .ofStaticChargeDensity c (q • distTranslate (basis.repr r₀) (diracDelta ℝ 0)) := by rw [oneDimPointParticleCurrentDensity] congr ext η - simp [distTranslate_apply] + simp @[simp] lemma oneDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : (oneDimPointParticleCurrentDensity c q r₀).currentDensity c = 0 := by - ext ε i - simp [oneDimPointParticleCurrentDensity, DistLorentzCurrentDensity.currentDensity, - Lorentz.Vector.spatialCLM, constantTime_apply] + simp [oneDimPointParticleCurrentDensity] @[simp] lemma oneDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) : (oneDimPointParticleCurrentDensity c q r₀).chargeDensity c = constantTime (q • diracDelta ℝ r₀) := by - ext ε - simp only [DistLorentzCurrentDensity.chargeDensity, one_div, Lorentz.Vector.temporalCLM, - Fin.isValue, oneDimPointParticleCurrentDensity, map_smul, LinearMap.coe_mk, AddHom.coe_mk, - ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul', - ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply, - Function.comp_apply, constantTime_apply, diracDelta'_apply, Lorentz.Vector.apply_smul, - Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul, diracDelta_apply] - field_simp + simp [oneDimPointParticleCurrentDensity] /-! @@ -101,16 +89,14 @@ lemma oneDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : /-- The electromagnetic potential of a point particle stationary at `r₀` of 1d space. -/ noncomputable def oneDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : - DistElectromagneticPotential 1 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| - distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0)) - (by fun_prop) + DistElectromagneticPotential 1 := .ofScalarPotential 𝓕.c <| constantTime <| + ⸨x => ((- (q * 𝓕.μ₀ * 𝓕.c ^ 2)/ 2) * ‖x - r₀‖)⸩ᵈ lemma oneDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : - oneDimPointParticle 𝓕 q r₀ = ((SpaceTime.distTimeSlice 𝓕.c).symm <| + oneDimPointParticle 𝓕 q r₀ = (.ofScalarPotential 𝓕.c <| constantTime <| distTranslate (basis.repr r₀) <| - distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) - (by fun_prop)) := by + ⸨x => ((- (q * 𝓕.μ₀ * 𝓕.c ^ 2)/ 2) * ‖x‖)⸩ᵈ) := by rw [oneDimPointParticle] congr ext η @@ -125,9 +111,7 @@ lemma oneDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : @[simp] lemma oneDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : (oneDimPointParticle 𝓕 q r₀).vectorPotential 𝓕.c = 0 := by - ext ε i - simp [vectorPotential, Lorentz.Vector.spatialCLM, - oneDimPointParticle, constantTime_apply, distOfFunction_vector_eval] + simp [oneDimPointParticle] /-! @@ -137,20 +121,9 @@ lemma oneDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : S lemma oneDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) : (oneDimPointParticle 𝓕 q r₀).scalarPotential 𝓕.c = - Space.constantTime (distOfFunction (fun x => - - ((q * 𝓕.μ₀ * 𝓕.c ^ 2)/(2)) • ‖x-r₀‖) (by fun_prop)) := by - ext ε - simp only [scalarPotential, Lorentz.Vector.temporalCLM, Fin.isValue, map_smul, - ContinuousLinearMap.comp_smulₛₗ, Real.ringHom_apply, oneDimPointParticle, LinearMap.coe_mk, - AddHom.coe_mk, ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul', - ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply, - Function.comp_apply, constantTime_apply, distOfFunction_vector_eval, Lorentz.Vector.apply_smul, - Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul, neg_mul] - rw [distOfFunction_mul_fun _ (by fun_prop), distOfFunction_neg, - distOfFunction_mul_fun _ (by fun_prop)] - simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, - ContinuousLinearMap.neg_apply] - ring + Space.constantTime ⸨x => - ((q * 𝓕.μ₀ * 𝓕.c ^ 2)/2) • ‖x-r₀‖⸩ᵈ := by + simp [oneDimPointParticle] + ring_nf /-! diff --git a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean index 85f8105e..809f394b 100644 --- a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean +++ b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean @@ -62,19 +62,16 @@ particle in 3d space. /-- The current density of a point particle stationary at a point `r₀` of 3d space. -/ noncomputable def threeDimPointParticleCurrentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) : - DistLorentzCurrentDensity 3 := (SpaceTime.distTimeSlice c).symm <| - constantTime ((c * q) • diracDelta' ℝ r₀ (Lorentz.Vector.basis (Sum.inl 0))) + DistLorentzCurrentDensity 3 := .ofStaticChargeDensity c (q • diracDelta ℝ r₀) lemma threeDimPointParticleCurrentDensity_eq_distTranslate (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) : - threeDimPointParticleCurrentDensity c q r₀ = ((SpaceTime.distTimeSlice c).symm <| - constantTime <| - distTranslate (basis.repr r₀) <| - ((c * q) • diracDelta' ℝ 0 (Lorentz.Vector.basis (Sum.inl 0)))) := by + threeDimPointParticleCurrentDensity c q r₀ = + .ofStaticChargeDensity c (q • distTranslate (basis.repr r₀) (diracDelta ℝ 0)) := by rw [threeDimPointParticleCurrentDensity] congr ext η - simp [distTranslate_apply] + simp /-! @@ -91,14 +88,7 @@ where $q$ is the charge of the particle and $r₀$ is the position of the partic lemma threeDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) : (threeDimPointParticleCurrentDensity c q r₀).chargeDensity c = constantTime (q • diracDelta ℝ r₀) := by - ext ε - simp only [DistLorentzCurrentDensity.chargeDensity, one_div, Lorentz.Vector.temporalCLM, - Fin.isValue, threeDimPointParticleCurrentDensity, map_smul, LinearMap.coe_mk, AddHom.coe_mk, - ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul', - ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply, - Function.comp_apply, constantTime_apply, diracDelta'_apply, Lorentz.Vector.apply_smul, - Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul, diracDelta_apply] - field_simp + simp [threeDimPointParticleCurrentDensity] /-! @@ -114,9 +104,7 @@ In other words, there is no current flow for a point particle at rest. @[simp] lemma threeDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) : (threeDimPointParticleCurrentDensity c q r₀).currentDensity c = 0 := by - ext ε i - simp [threeDimPointParticleCurrentDensity, DistLorentzCurrentDensity.currentDensity, - Lorentz.Vector.spatialCLM, constantTime_apply] + simp [threeDimPointParticleCurrentDensity] /-! @@ -141,18 +129,15 @@ open Real /-- The electromagnetic potential of a point particle stationary at `r₀` of 3d space. -/ noncomputable def threeDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) : - DistElectromagneticPotential 3 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <| - distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π)) * ‖x - r₀‖⁻¹) • - Lorentz.Vector.basis (Sum.inl 0)) - (((IsDistBounded.inv_shift _).const_mul_fun _).smul_const _) + DistElectromagneticPotential 3 := .ofScalarPotential 𝓕.c <| Space.constantTime <| + ⸨x => ((q * 𝓕.μ₀ * 𝓕.c ^ 2)/ (4 * π)) * ‖x - r₀‖⁻¹⸩ᵈ lemma threeDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) : - threeDimPointParticle 𝓕 q r₀ = ((SpaceTime.distTimeSlice 𝓕.c).symm <| + threeDimPointParticle 𝓕 q r₀ = (.ofScalarPotential 𝓕.c <| constantTime <| distTranslate (basis.repr r₀) <| - distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π))* ‖x‖⁻¹) • - Lorentz.Vector.basis (Sum.inl 0)) - ((IsDistBounded.inv.const_mul_fun _).smul_const _)) := by + distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c ^ 2)/ (4 * π))* ‖x‖⁻¹)) + (IsDistBounded.inv.const_mul_fun _)) := by rw [threeDimPointParticle] congr ext η @@ -171,22 +156,10 @@ $$V(r) = \frac{q}{4 π \epsilon_0 |r - r_0|}.$$ lemma threeDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) : (threeDimPointParticle 𝓕 q r₀).scalarPotential 𝓕.c = - Space.constantTime (distOfFunction (fun x => (q/ (4 * π * 𝓕.ε₀))• ‖x - r₀‖⁻¹) - (((IsDistBounded.inv_shift _).const_mul_fun _))) := by - ext ε - simp only [scalarPotential, Lorentz.Vector.temporalCLM, Fin.isValue, map_smul, - ContinuousLinearMap.comp_smulₛₗ, ringHom_apply, threeDimPointParticle, LinearMap.coe_mk, - AddHom.coe_mk, ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul', - ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply, - Function.comp_apply, constantTime_apply, distOfFunction_vector_eval, Lorentz.Vector.apply_smul, - Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul] - rw [distOfFunction_mul_fun _ (IsDistBounded.inv_shift _), - distOfFunction_mul_fun _ (IsDistBounded.inv_shift _)] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ContinuousLinearMap.coe_smul', Pi.smul_apply, - smul_eq_mul] - ring_nf - simp only [𝓕.c_sq, one_div, mul_inv_rev, mul_eq_mul_right_iff, inv_eq_zero, OfNat.ofNat_ne_zero, - or_false] + Space.constantTime ⸨x => (q/ (4 * π * 𝓕.ε₀))• ‖x - r₀‖⁻¹⸩ᵈ := by + simp [threeDimPointParticle, 𝓕.c_sq] + congr + funext x field_simp /-! @@ -203,9 +176,7 @@ $$\vec A(r) = 0.$$ @[simp] lemma threeDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) : (threeDimPointParticle 𝓕 q r₀).vectorPotential 𝓕.c = 0 := by - ext ε i - simp [vectorPotential, Lorentz.Vector.spatialCLM, - threeDimPointParticle, constantTime_apply, distOfFunction_vector_eval] + simp [threeDimPointParticle] /-! @@ -255,9 +226,7 @@ Given that the vector potential is zero, the magnetic field is also zero. @[simp] lemma threeDimPointParticle_magneticFieldMatrix (q : ℝ) (r₀ : Space 3) : - (threeDimPointParticle 𝓕 q r₀).magneticFieldMatrix 𝓕.c = 0 := by - ext η - simp [magneticFieldMatrix_eq_vectorPotential] + (threeDimPointParticle 𝓕 q r₀).magneticFieldMatrix 𝓕.c = 0 := by simp [threeDimPointParticle] /-! diff --git a/PhysLean/SpaceAndTime/Space/DistOfFunction.lean b/PhysLean/SpaceAndTime/Space/DistOfFunction.lean index 5e86d651..e68a403b 100644 --- a/PhysLean/SpaceAndTime/Space/DistOfFunction.lean +++ b/PhysLean/SpaceAndTime/Space/DistOfFunction.lean @@ -49,7 +49,9 @@ open MeasureTheory -/ /-- A distribution `Space d →d[ℝ] F` from a function - `f : Space d → F` which satisfies the `IsDistBounded f` condition. -/ + `f : Space d → F` which satisfies the `IsDistBounded f` condition. + The notation `⸨x => f x⸩ᵈ` or `⸨f⸩ᵈ` can be used if the proof that + `f` satisfies `IsDistBounded f` follows via `by fun_prop`. -/ def distOfFunction {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) : (Space d) →d[ℝ] F := by refine mkCLMtoNormedSpace (fun η => ∫ x, η x • f x) ?_ ?_ hf.integral_mul_schwartzMap_bounded @@ -72,6 +74,13 @@ lemma distOfFunction_apply {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) : distOfFunction f hf η = ∫ x, η x • f x := rfl +@[inherit_doc distOfFunction] +macro "⸨" u:term " => " x:term "⸩ᵈ" : term => + `(distOfFunction (fun $u => $x) (by fun_prop)) + +@[inherit_doc distOfFunction] +macro "⸨"f:term "⸩ᵈ" : term => + `(distOfFunction ($f) (by fun_prop)) /-! ## B. Linarity properties of getting distributions from functions @@ -79,13 +88,12 @@ lemma distOfFunction_apply {d : ℕ} (f : Space d → F) -/ @[simp] lemma distOfFunction_zero_eq_zero {d : ℕ} : - distOfFunction (fun _ : Space d => (0 : F)) (by fun_prop) = 0 := by + ⸨(_ : Space d) => (0 : F)⸩ᵈ = 0 := by ext η simp [distOfFunction_apply] lemma distOfFunction_smul {d : ℕ} (f : Space d → F) - (hf : IsDistBounded f) (c : ℝ) : - distOfFunction (c • f) (by fun_prop) = c • distOfFunction f hf := by + (hf : IsDistBounded f) (c : ℝ) : ⸨c • f⸩ᵈ = c • ⸨f⸩ᵈ := by ext η change _ = c • ∫ x, η x • f x rw [distOfFunction_apply]