InfiniteWire

📁 Source: PhysLean/Electromagnetism/Current/InfiniteWire.lean

Statistics

Metric	Count
Definitions infiniteWire, wireCurrentDensity	2
Theorems infiniteWire_electricField, infiniteWire_isExterma, infiniteWire_scalarPotential, infiniteWire_vectorPotential, infiniteWire_vectorPotential_distSpaceDeriv_0, infiniteWire_vectorPotential_distTimeDeriv, infiniteWire_vectorPotential_fst, infiniteWire_vectorPotential_snd, infiniteWire_vectorPotential_thrd, wireCurrentDensity_chargeDesnity, wireCurrentDensity_currentDensity_fst, wireCurrentDensity_currentDensity_snd, wireCurrentDensity_currentDensity_thrd	13
Total	15

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
infiniteWire 📖	CompOp	9 math math: infiniteWire_vectorPotential_thrd, infiniteWire_electricField, infiniteWire_vectorPotential_fst, infiniteWire_vectorPotential, infiniteWire_vectorPotential_distTimeDeriv, infiniteWire_vectorPotential_snd, infiniteWire_isExterma, infiniteWire_scalarPotential, infiniteWire_vectorPotential_distSpaceDeriv_0
wireCurrentDensity 📖	CompOp	5 math math: wireCurrentDensity_currentDensity_fst, wireCurrentDensity_chargeDesnity, infiniteWire_isExterma, wireCurrentDensity_currentDensity_snd, wireCurrentDensity_currentDensity_thrd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infiniteWire_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 infiniteWire	—	infiniteWire_scalarPotential infiniteWire_vectorPotential_distTimeDeriv
infiniteWire_isExterma 📖	mathematical	—	IsExtrema infiniteWire Electromagnetism.DistLorentzCurrentDensity SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup wireCurrentDensity Electromagnetism.FreeSpace.c	—	infiniteWire_electricField wireCurrentDensity_chargeDesnity infiniteWire_vectorPotential_distSpaceDeriv_0 Space.IsDistBounded.log_norm Space.distSpaceDeriv_apply' infiniteWire_vectorPotential_fst Space.apply_fderiv_eq_distSpaceDeriv wireCurrentDensity_currentDensity_fst Space.constantTime_distSpaceDeriv Space.distDeriv_constantSliceDist_succAbove Space.distDiv_apply_eq_sum_distDeriv Space.instFiniteDimensionalReal Space.distDeriv_apply Distribution.fderivD_apply Space.distGrad_apply Space.IsDistBounded.zpow_smul_repr_self Space.distGrad_distOfFunction_log_norm Space.instBorelSpace Space.distDiv_inv_pow_eq_dim Space.distOfFunction.congr_simp Space.volume_metricBall_two_real wireCurrentDensity_currentDensity_snd Space.distSpaceDeriv_commute infiniteWire_vectorPotential_thrd infiniteWire_vectorPotential_snd wireCurrentDensity_currentDensity_thrd
infiniteWire_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 infiniteWire	—	Lorentz.Vector.instFiniteDimensionalReal Space.constantTime_apply Space.constantSliceDist_apply Space.IsDistBounded.vector_component Space.distOfFunction_vector_eval Lorentz.Vector.basis_apply Space.distOfFunction.congr_simp Space.distOfFunction_zero_eq_zero
infiniteWire_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 infiniteWire Space.constantTime Space.constantSliceDist Electromagnetism.FreeSpace.μ₀ Space.distOfFunction Space.instNorm Space.IsDistBounded.smul_const Space.IsDistBounded.log_norm	—	Space.IsDistBounded.smul_const Space.IsDistBounded.log_norm Space.IsDistBounded.vector_component Lorentz.Vector.basis_apply Space.IsDistBounded.pi_comp Space.constantTime_apply Space.constantSliceDist_apply Space.distOfFunction_vector_eval Space.distOfFunction.congr_simp Space.distOfFunction_eculid_eval
infiniteWire_vectorPotential_distSpaceDeriv_0 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Space.distSpaceDeriv Electromagnetism.DistElectromagneticPotential SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup vectorPotential Electromagnetism.FreeSpace.c infiniteWire	—	Space.IsDistBounded.smul_const Space.IsDistBounded.log_norm infiniteWire_vectorPotential Space.constantTime_distSpaceDeriv Space.distDeriv_constantSliceDist_same
infiniteWire_vectorPotential_distTimeDeriv 📖	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 vectorPotential Electromagnetism.FreeSpace.c infiniteWire	—	Space.IsDistBounded.smul_const Space.IsDistBounded.log_norm infiniteWire_vectorPotential Space.constantTime_distTimeDeriv
infiniteWire_vectorPotential_fst 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Electromagnetism.DistElectromagneticPotential SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup vectorPotential Electromagnetism.FreeSpace.c infiniteWire Space.constantTime Space.constantSliceDist Electromagnetism.FreeSpace.μ₀ Space.distOfFunction Space.instNorm Space.IsDistBounded.log_norm	—	Space.IsDistBounded.log_norm Space.IsDistBounded.pi_comp Space.IsDistBounded.smul_const infiniteWire_vectorPotential Space.constantTime_apply Space.constantSliceDist_apply Space.distOfFunction_eculid_eval Space.distOfFunction.congr_simp
infiniteWire_vectorPotential_snd 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Electromagnetism.DistElectromagneticPotential SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup vectorPotential Electromagnetism.FreeSpace.c infiniteWire	—	Space.IsDistBounded.smul_const Space.IsDistBounded.log_norm infiniteWire_vectorPotential Space.constantTime_apply Space.constantSliceDist_apply Space.IsDistBounded.pi_comp Space.distOfFunction_eculid_eval Space.distOfFunction.congr_simp Space.distOfFunction_zero_eq_zero
infiniteWire_vectorPotential_thrd 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Electromagnetism.DistElectromagneticPotential SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup vectorPotential Electromagnetism.FreeSpace.c infiniteWire	—	Space.IsDistBounded.smul_const Space.IsDistBounded.log_norm infiniteWire_vectorPotential Space.constantTime_apply Space.constantSliceDist_apply Space.IsDistBounded.pi_comp Space.distOfFunction_eculid_eval Space.distOfFunction.congr_simp Space.distOfFunction_zero_eq_zero
wireCurrentDensity_chargeDesnity 📖	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 wireCurrentDensity	—	Space.constantTime_apply Space.constantSliceDist_apply Lorentz.Vector.temporalCLM_basis_sum_inr
wireCurrentDensity_currentDensity_fst 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Electromagnetism.DistLorentzCurrentDensity SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup Electromagnetism.DistLorentzCurrentDensity.currentDensity wireCurrentDensity Space.constantTime Space.constantSliceDist Distribution.diracDelta Space.instZero	—	Space.constantTime_apply Space.constantSliceDist_apply Lorentz.Vector.spatialCLM_basis_sum_inr
wireCurrentDensity_currentDensity_snd 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Electromagnetism.DistLorentzCurrentDensity SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup Electromagnetism.DistLorentzCurrentDensity.currentDensity wireCurrentDensity	—	Space.constantTime_apply Space.constantSliceDist_apply Lorentz.Vector.spatialCLM_basis_sum_inr
wireCurrentDensity_currentDensity_thrd 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup Space.instNormedAddCommGroup Time.instNormedSpaceReal Space.instInnerProductSpaceReal Electromagnetism.DistLorentzCurrentDensity SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace Lorentz.Vector Lorentz.Vector.instModuleReal Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instAddCommGroup Electromagnetism.DistLorentzCurrentDensity.currentDensity wireCurrentDensity	—	Space.constantTime_apply Space.constantSliceDist_apply Lorentz.Vector.spatialCLM_basis_sum_inr

---

← Back to Index