OneDimension

📁 Source: PhysLean/Electromagnetism/PointParticle/OneDimension.lean

Statistics

Metric	Count
Definitions oneDimPointParticle, oneDimPointParticleCurrentDensity	2
Theorems oneDimPointParticleCurrentDensity_chargeDensity, oneDimPointParticleCurrentDensity_currentDensity, oneDimPointParticleCurrentDensity_eq_distTranslate, oneDimPointParticle_div_electricField, oneDimPointParticle_electricField, oneDimPointParticle_electricField_timeDeriv, oneDimPointParticle_eq_distTranslate, oneDimPointParticle_isExterma, oneDimPointParticle_magneticFieldMatrix, oneDimPointParticle_scalarPotential, oneDimPointParticle_vectorPotential	11
Total	13

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
oneDimPointParticle 📖	CompOp	8 math math: oneDimPointParticle_scalarPotential, oneDimPointParticle_div_electricField, oneDimPointParticle_eq_distTranslate, oneDimPointParticle_vectorPotential, oneDimPointParticle_electricField_timeDeriv, oneDimPointParticle_electricField, oneDimPointParticle_isExterma, oneDimPointParticle_magneticFieldMatrix
oneDimPointParticleCurrentDensity 📖	CompOp	4 math math: oneDimPointParticleCurrentDensity_currentDensity, oneDimPointParticleCurrentDensity_eq_distTranslate, oneDimPointParticle_isExterma, oneDimPointParticleCurrentDensity_chargeDensity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oneDimPointParticleCurrentDensity_chargeDensity 📖	mathematical	—	Electromagnetism.DistLorentzCurrentDensity Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup Electromagnetism.DistLorentzCurrentDensity.chargeDensity oneDimPointParticleCurrentDensity Space.constantTime Distribution.diracDelta	—	Lorentz.Vector.instFiniteDimensionalReal Space.constantTime_apply Lorentz.Vector.basis_apply
oneDimPointParticleCurrentDensity_currentDensity 📖	mathematical	—	Electromagnetism.DistLorentzCurrentDensity Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup Electromagnetism.DistLorentzCurrentDensity.currentDensity oneDimPointParticleCurrentDensity	—	Space.constantTime_apply Lorentz.Vector.basis_apply
oneDimPointParticleCurrentDensity_eq_distTranslate 📖	mathematical	—	oneDimPointParticleCurrentDensity Distribution Time Space Lorentz.Vector Time.instNormedAddCommGroup Space.instNormedAddCommGroup Lorentz.Vector.isNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Lorentz.Vector.isNormedSpace SpaceTime SpaceTime.distTimeSlice Space.constantTime Space.distTranslate Space.basis Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommGroup SpeedOfLight.val Distribution.diracDelta' Space.instZero Lorentz.Vector.basis	—	oneDimPointParticleCurrentDensity.eq_1
oneDimPointParticle_div_electricField 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Space.distSpaceDiv Electromagnetism.DistElectromagneticPotential SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup electricField Electromagnetism.FreeSpace.c oneDimPointParticle Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Space.constantTime Distribution.diracDelta	—	Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self oneDimPointParticle_electricField Space.distOfFunction.congr_simp Space.instFiniteDimensionalReal Space.instBorelSpace Space.distDiv_inv_pow_eq_dim Space.IsDistBounded.comp_add_right Space.distTranslate_ofFunction Space.constantTime_distSpaceDiv Space.distDiv_distTranslate Space.finrank_eq_dim Space.constantTime_apply
oneDimPointParticle_electricField 📖	mathematical	—	Electromagnetism.DistElectromagneticPotential Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup electricField Electromagnetism.FreeSpace.c oneDimPointParticle Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Space.constantTime Space.distOfFunction Space.instNorm Space.basis Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self	—	Space.IsDistBounded.pow Space.IsDistBounded.const_fun_smul Space.IsDistBounded.zpow_smul_repr_self Space.distGrad_distOfFunction_norm_zpow Space.IsDistBounded.comp_sub_right Space.IsDistBounded.norm_sub oneDimPointParticle_scalarPotential Space.distOfFunction.congr_simp oneDimPointParticle_vectorPotential Space.constantTime_distSpaceGrad Space.IsDistBounded.neg Space.distOfFunction_neg Space.IsDistBounded.const_mul_fun Space.distOfFunction_mul_fun Space.IsDistBounded.norm Space.IsDistBounded.comp_add_right Space.distTranslate_ofFunction Space.distTranslate_distGrad
oneDimPointParticle_electricField_timeDeriv 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Space.distTimeDeriv Electromagnetism.DistElectromagneticPotential SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup electricField Electromagnetism.FreeSpace.c oneDimPointParticle	—	Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self oneDimPointParticle_electricField Space.distOfFunction.congr_simp Space.constantTime_distTimeDeriv
oneDimPointParticle_eq_distTranslate 📖	mathematical	—	oneDimPointParticle Distribution Time Space Lorentz.Vector Time.instNormedAddCommGroup Space.instNormedAddCommGroup Lorentz.Vector.isNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Lorentz.Vector.isNormedSpace SpaceTime SpaceTime.distTimeSlice Electromagnetism.FreeSpace.c Space.constantTime Space.distTranslate Space.basis Space.distOfFunction Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Space.instNorm Lorentz.Vector.basis Space.IsDistBounded.smul_const Space.IsDistBounded.const_mul_fun Space.IsDistBounded.norm	—	Space.IsDistBounded.smul_const Space.IsDistBounded.const_mul_fun Space.IsDistBounded.norm oneDimPointParticle.eq_1 Space.IsDistBounded.comp_add_right Space.distTranslate_ofFunction Space.distOfFunction.congr_simp
oneDimPointParticle_isExterma 📖	mathematical	—	IsExtrema oneDimPointParticle oneDimPointParticleCurrentDensity Electromagnetism.FreeSpace.c	—	isExtrema_iff_components gradLagrangian_sum_inl_0 oneDimPointParticleCurrentDensity_chargeDensity oneDimPointParticle_div_electricField gradLagrangian_sum_inr_i oneDimPointParticle_electricField_timeDeriv magneticFieldMatrix_one_dim_eq_zero oneDimPointParticleCurrentDensity_currentDensity
oneDimPointParticle_magneticFieldMatrix 📖	mathematical	—	Electromagnetism.DistElectromagneticPotential Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup magneticFieldMatrix Electromagnetism.FreeSpace.c oneDimPointParticle	—	magneticFieldMatrix_one_dim_eq_zero
oneDimPointParticle_scalarPotential 📖	mathematical	—	Electromagnetism.DistElectromagneticPotential Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup scalarPotential Electromagnetism.FreeSpace.c oneDimPointParticle Space.constantTime Space.distOfFunction Electromagnetism.FreeSpace.μ₀ SpeedOfLight.val Space.instNorm Space.IsDistBounded.const_fun_smul Space.IsDistBounded.norm_sub	—	Space.IsDistBounded.const_fun_smul Space.IsDistBounded.norm_sub Space.IsDistBounded.vector_component Lorentz.Vector.basis_apply Lorentz.Vector.instFiniteDimensionalReal Space.constantTime_apply Space.distOfFunction_vector_eval Space.distOfFunction.congr_simp Space.IsDistBounded.const_mul_fun Space.distOfFunction_mul_fun Space.IsDistBounded.neg Space.distOfFunction_neg
oneDimPointParticle_vectorPotential 📖	mathematical	—	Electromagnetism.DistElectromagneticPotential Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup vectorPotential Electromagnetism.FreeSpace.c oneDimPointParticle	—	Space.constantTime_apply Space.IsDistBounded.vector_component Space.distOfFunction_vector_eval Lorentz.Vector.basis_apply Space.distOfFunction.congr_simp Space.distOfFunction_zero_eq_zero

---

← Back to Index