ThreeDimension

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

Statistics

Metric	Count
Definitions threeDimPointParticle, threeDimPointParticleCurrentDensity	2
Theorems threeDimPointParticleCurrentDensity_chargeDensity, threeDimPointParticleCurrentDensity_currentDensity, threeDimPointParticleCurrentDensity_eq_distTranslate, threeDimPointParticle_div_electricField, threeDimPointParticle_electricField, threeDimPointParticle_electricField_timeDeriv, threeDimPointParticle_eq_distTranslate, threeDimPointParticle_isExterma, threeDimPointParticle_magneticFieldMatrix, threeDimPointParticle_scalarPotential, threeDimPointParticle_vectorPotential	11
Total	13

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
threeDimPointParticle 📖	CompOp	8 math math: threeDimPointParticle_eq_distTranslate, threeDimPointParticle_vectorPotential, threeDimPointParticle_electricField, threeDimPointParticle_magneticFieldMatrix, threeDimPointParticle_scalarPotential, threeDimPointParticle_div_electricField, threeDimPointParticle_electricField_timeDeriv, threeDimPointParticle_isExterma
threeDimPointParticleCurrentDensity 📖	CompOp	4 math math: threeDimPointParticleCurrentDensity_currentDensity, threeDimPointParticleCurrentDensity_chargeDensity, threeDimPointParticleCurrentDensity_eq_distTranslate, threeDimPointParticle_isExterma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
threeDimPointParticleCurrentDensity_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 threeDimPointParticleCurrentDensity Space.constantTime Distribution.diracDelta	—	Lorentz.Vector.instFiniteDimensionalReal Space.constantTime_apply Lorentz.Vector.basis_apply
threeDimPointParticleCurrentDensity_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 threeDimPointParticleCurrentDensity	—	Space.constantTime_apply Lorentz.Vector.basis_apply
threeDimPointParticleCurrentDensity_eq_distTranslate 📖	mathematical	—	threeDimPointParticleCurrentDensity 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	—	threeDimPointParticleCurrentDensity.eq_1
threeDimPointParticle_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 threeDimPointParticle Electromagnetism.FreeSpace.ε₀ Space.constantTime Distribution.diracDelta	—	Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self threeDimPointParticle_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.volume_metricBall_three Space.constantTime_apply
threeDimPointParticle_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 threeDimPointParticle Electromagnetism.FreeSpace.ε₀ Space.constantTime Space.distOfFunction Space.instNorm Space.basis Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self	—	Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self Space.IsDistBounded.const_mul_fun Space.IsDistBounded.inv_shift threeDimPointParticle_scalarPotential threeDimPointParticle_vectorPotential Space.distOfFunction.congr_simp Space.constantTime_distSpaceGrad Space.distOfFunction_mul_fun Space.IsDistBounded.inv Space.IsDistBounded.comp_add_right Space.distTranslate_ofFunction Space.distTranslate_distGrad Space.IsDistBounded.pow Space.IsDistBounded.const_fun_smul Space.distGrad_distOfFunction_norm_zpow Space.IsDistBounded.neg Space.distOfFunction_neg
threeDimPointParticle_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 threeDimPointParticle	—	Space.IsDistBounded.comp_sub_right Space.IsDistBounded.zpow_smul_repr_self threeDimPointParticle_electricField Space.distOfFunction.congr_simp Space.constantTime_distTimeDeriv
threeDimPointParticle_eq_distTranslate 📖	mathematical	—	threeDimPointParticle 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.inv	—	Space.IsDistBounded.smul_const Space.IsDistBounded.const_mul_fun Space.IsDistBounded.inv threeDimPointParticle.eq_1 Space.IsDistBounded.comp_add_right Space.distTranslate_ofFunction Space.distOfFunction.congr_simp
threeDimPointParticle_isExterma 📖	mathematical	—	IsExtrema threeDimPointParticle threeDimPointParticleCurrentDensity Electromagnetism.FreeSpace.c	—	isExtrema_iff_components gradLagrangian_sum_inl_0 threeDimPointParticleCurrentDensity_chargeDensity threeDimPointParticle_div_electricField Electromagnetism.FreeSpace.c_sq gradLagrangian_sum_inr_i threeDimPointParticle_electricField_timeDeriv threeDimPointParticle_magneticFieldMatrix threeDimPointParticleCurrentDensity_currentDensity
threeDimPointParticle_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 threeDimPointParticle	—	magneticFieldMatrix_eq_vectorPotential threeDimPointParticle_vectorPotential
threeDimPointParticle_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 threeDimPointParticle Space.constantTime Space.distOfFunction Electromagnetism.FreeSpace.ε₀ Space.instNorm Space.IsDistBounded.const_mul_fun Space.IsDistBounded.inv_shift	—	Space.IsDistBounded.const_mul_fun Space.IsDistBounded.inv_shift Space.IsDistBounded.vector_component Lorentz.Vector.basis_apply Lorentz.Vector.instFiniteDimensionalReal Space.constantTime_apply Space.distOfFunction_vector_eval Space.distOfFunction.congr_simp Space.distOfFunction_mul_fun Electromagnetism.FreeSpace.c_sq
threeDimPointParticle_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 threeDimPointParticle	—	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