Basic

📁 Source: PhysLean/SpaceAndTime/SpaceTime/Basic.lean

Statistics

Metric	Count
Definitions SpaceTime, coord, coordCLM, instMeasurableSpace, instMeasureSpace, space, space_equivariant, term𝔁, time, timeSpaceBasis, timeSpaceBasisEquiv, toTimeAndSpace	12
Theorems coord_apply, det_timeSpaceBasisEquiv, instBorelSpace, instIsAddHaarMeasureVolume, instIsFiniteMeasureOnCompactsVolume, instIsOpenPosMeasureVolume, spaceTime_integrable_iff_space_time_integrable, spaceTime_integral_eq_space_integral_time_integral, spaceTime_integral_eq_time_integral_space_integral, spaceTime_integral_eq_time_space_integral, space_toCoord_symm, space_toTimeAndSpace_symm, timeSpaceBasis_addHaar, timeSpaceBasis_apply_inl, timeSpaceBasis_apply_inr, timeSpaceBasis_eq_map_basis, time_toTimeAndSpace_symm, time_val_toCoord_symm, toTimeAndSpace_basis_inl, toTimeAndSpace_basis_inl', toTimeAndSpace_basis_inr, toTimeAndSpace_fderiv, toTimeAndSpace_symm_apply_inl, toTimeAndSpace_symm_apply_inr, toTimeAndSpace_symm_apply_time_space, toTimeAndSpace_symm_fderiv, toTimeAndSpace_symm_measurePreserving	27
Total	39

SpaceTime

Definitions

Name	Category	Theorems
coord 📖	CompOp	1 math math: coord_apply
coordCLM 📖	CompOp	—
instMeasurableSpace 📖	CompOp	2 math math: instBorelSpace, timeSpaceBasis_addHaar
instMeasureSpace 📖	CompOp	13 math math: spaceTime_integrable_iff_space_time_integrable, toTimeAndSpace_symm_measurePreserving, instIsAddHaarMeasureVolume, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt, spaceTime_integral_eq_time_space_integral, Electromagnetism.ElectromagneticPotential.kineticTerm_hasVarGradientAt, instIsOpenPosMeasureVolume, Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt, timeSpaceBasis_addHaar, instIsFiniteMeasureOnCompactsVolume, Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_eq_add_gradKineticTerm, Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_gradLagrangian, Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component
space 📖	CompOp	18 math math: Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, space_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, space_toCoord_symm
space_equivariant 📖	CompOp	—
term𝔁 📖	CompOp	—
time 📖	CompOp	18 math math: Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, time_val_toCoord_symm, time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix
timeSpaceBasis 📖	CompOp	4 math math: timeSpaceBasis_eq_map_basis, timeSpaceBasis_addHaar, timeSpaceBasis_apply_inr, timeSpaceBasis_apply_inl
timeSpaceBasisEquiv 📖	CompOp	2 math math: timeSpaceBasis_eq_map_basis, det_timeSpaceBasisEquiv
toTimeAndSpace 📖	CompOp	34 math math: spaceTime_integrable_iff_space_time_integrable, distTimeSlice_symm_apply, deriv_sum_inr, toTimeAndSpace_symm_measurePreserving, space_toTimeAndSpace_symm, spaceTime_integral_eq_time_space_integral, deriv_sum_inl, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, distTimeSlice_apply, toTimeAndSpace_basis_inr, boost_zero_apply_time_space, time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, toTimeAndSpace_symm_apply_inr, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, toTimeAndSpace_symm_apply_inl, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, toTimeAndSpace_symm_fderiv, toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, spaceTime_integral_eq_space_integral_time_integral, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, toTimeAndSpace_basis_inl, toTimeAndSpace_symm_apply_time_space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coord_apply 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal coord	—	—
det_timeSpaceBasisEquiv 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid timeSpaceBasisEquiv SpeedOfLight.val	—	Lorentz.Vector.instFiniteDimensionalReal Time.ext time_val_toCoord_symm Space.eq_of_apply Time.instFiniteDimensionalReal Space.instFiniteDimensionalReal Time.finRank_eq_one
instBorelSpace 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup instMeasurableSpace	—	—
instIsAddHaarMeasureVolume 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup instMeasureSpace	—	instBorelSpace
instIsFiniteMeasureOnCompactsVolume 📖	mathematical	—	SpaceTime instMeasureSpace Lorentz.Vector.isNormedAddCommGroup	—	instBorelSpace
instIsOpenPosMeasureVolume 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup instMeasureSpace	—	instBorelSpace
spaceTime_integrable_iff_space_time_integrable 📖	mathematical	—	SpaceTime instMeasureSpace Time Space Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace	—	Time.instFiniteDimensionalReal Time.instBorelSpace Space.instFiniteDimensionalReal Space.instBorelSpace toTimeAndSpace_symm_measurePreserving instBorelSpace Lorentz.Vector.instFiniteDimensionalReal
spaceTime_integral_eq_space_integral_time_integral 📖	mathematical	SpaceTime instMeasureSpace	SpeedOfLight.val Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace	—	Space.instFiniteDimensionalReal Space.instBorelSpace Time.instFiniteDimensionalReal Time.instBorelSpace spaceTime_integral_eq_time_space_integral spaceTime_integrable_iff_space_time_integrable
spaceTime_integral_eq_time_integral_space_integral 📖	mathematical	SpaceTime instMeasureSpace	SpeedOfLight.val Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace	—	Time.instFiniteDimensionalReal Time.instBorelSpace Space.instFiniteDimensionalReal Space.instBorelSpace spaceTime_integral_eq_time_space_integral spaceTime_integrable_iff_space_time_integrable
spaceTime_integral_eq_time_space_integral 📖	mathematical	—	SpaceTime instMeasureSpace SpeedOfLight.val Time Space Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace	—	Time.instFiniteDimensionalReal Time.instBorelSpace Space.instFiniteDimensionalReal Space.instBorelSpace instBorelSpace Space.volume_eq_addHaar Time.volume_eq_basis_addHaar Lorentz.Vector.instFiniteDimensionalReal timeSpaceBasis_addHaar
space_toCoord_symm 📖	mathematical	—	Space.val SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instModuleReal Space.instModuleReal space	—	—
space_toTimeAndSpace_symm 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instModuleReal Space.instModuleReal space Time Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Time.instModuleReal toTimeAndSpace	—	Space.eq_of_apply Lorentz.Vector.instFiniteDimensionalReal
timeSpaceBasis_addHaar 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.isNormedSpace instMeasurableSpace instBorelSpace timeSpaceBasis instMeasureSpace SpeedOfLight.val	—	instBorelSpace timeSpaceBasis_eq_map_basis Lorentz.Vector.instFiniteDimensionalReal det_timeSpaceBasisEquiv
timeSpaceBasis_apply_inl 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal timeSpaceBasis Lorentz.Vector Lorentz.Vector.isNormedAddCommGroup SpeedOfLight.val Lorentz.Vector.basis	—	Time.basis_apply_eq_one toTimeAndSpace_basis_inl Time.ext Time.one_val
timeSpaceBasis_apply_inr 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal timeSpaceBasis Lorentz.Vector Lorentz.Vector.basis	—	toTimeAndSpace_basis_inr
timeSpaceBasis_eq_map_basis 📖	mathematical	—	timeSpaceBasis Lorentz.Vector SpaceTime Lorentz.Vector.instAddCommMonoid Lorentz.Vector.instModuleReal Lorentz.Vector.basis Lorentz.Vector.isNormedAddCommGroup timeSpaceBasisEquiv	—	timeSpaceBasis_apply_inl Lorentz.Vector.basis_apply timeSpaceBasis_apply_inr
time_toTimeAndSpace_symm 📖	mathematical	—	SpaceTime Time Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Lorentz.Vector.instModuleReal Time.instModuleReal time Space Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Space.instModuleReal toTimeAndSpace	—	Time.ext Lorentz.Vector.instFiniteDimensionalReal
time_val_toCoord_symm 📖	mathematical	—	Time.val SpaceTime Time Lorentz.Vector.instAddCommMonoid Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Lorentz.Vector.instModuleReal Time.instModuleReal time SpeedOfLight.val	—	—
toTimeAndSpace_basis_inl 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instModuleReal Time.instModuleReal Space.instModuleReal toTimeAndSpace Lorentz.Vector Lorentz.Vector.basis SpeedOfLight.val Space.instZero	—	Lorentz.Vector.timeComponent_basis_sum_inl Space.eq_of_apply Lorentz.Vector.basis_apply Space.zero_apply
toTimeAndSpace_basis_inl' 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instModuleReal Time.instModuleReal Space.instModuleReal toTimeAndSpace Lorentz.Vector Lorentz.Vector.basis Time.instSMulReal Space.instSMulReal SpeedOfLight.val Time.instOfNat Space.instZero	—	toTimeAndSpace_basis_inl Time.one_val
toTimeAndSpace_basis_inr 📖	mathematical	—	SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.instModuleReal Time.instModuleReal Space.instModuleReal toTimeAndSpace Lorentz.Vector Lorentz.Vector.basis Time.instOfNat Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.basis	—	Lorentz.Vector.timeComponent_basis_sum_inr Space.eq_of_apply Lorentz.Vector.basis_apply Space.basis_apply
toTimeAndSpace_fderiv 📖	mathematical	—	SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Time Space Time.instAddCommGroup Space.instAddCommGroup Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Time.instModuleReal Space.instModuleReal Space.instSeminormedAddCommGroup Lorentz.Vector.instAddCommMonoid toTimeAndSpace	—	—
toTimeAndSpace_symm_apply_inl 📖	mathematical	—	Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace SpeedOfLight.val Time.val	—	—
toTimeAndSpace_symm_apply_inr 📖	mathematical	—	Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace Space.val	—	—
toTimeAndSpace_symm_apply_time_space 📖	mathematical	—	Time Space Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace time space	—	—
toTimeAndSpace_symm_fderiv 📖	mathematical	—	Time Space Time.instAddCommGroup Space.instAddCommGroup Time.instSeminormedAddCommGroup Time.instNormedAddCommGroup Space.instAddCommMonoid Time.instModuleReal Space.instModuleReal Space.instSeminormedAddCommGroup SpaceTime Lorentz.Vector.instAddCommGroup Lorentz.Vector.instModuleReal Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid toTimeAndSpace	—	—
toTimeAndSpace_symm_measurePreserving 📖	mathematical	—	Time Space SpaceTime Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space.instNormedAddCommGroup Space.instInnerProductSpaceReal Space.instFiniteDimensionalReal Space.instMeasurableSpace Space.instBorelSpace instMeasureSpace Time.instSeminormedAddCommGroup Space.instSeminormedAddCommGroup Space.instAddCommMonoid Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.instAddCommMonoid Time.instModuleReal Space.instModuleReal Lorentz.Vector.instModuleReal toTimeAndSpace SpeedOfLight.val	—	instBorelSpace Time.instFiniteDimensionalReal Time.instBorelSpace Space.instFiniteDimensionalReal Space.instBorelSpace Space.volume_eq_addHaar Time.volume_eq_basis_addHaar Lorentz.Vector.instFiniteDimensionalReal timeSpaceBasis_addHaar

(root)

Definitions

Name	Category	Theorems
SpaceTime 📖	CompOp	176 math math: StandardModel.HiggsField.toVec_smooth, SpaceTime.distTimeSlice_distDeriv_inl, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_gradLagrangian, Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, StandardModel.HiggsField.normSq_smooth, SpaceTime.differentiable_vector, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, StandardModel.HiggsField.const_toHiggsVec_apply, StandardModel.HiggsField.inner_symm, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, SpaceTime.deriv_coord, SpaceTime.distDeriv_apply', StandardModel.HiggsField.Potential.isMinOn_iff_of_μSq_nonpos_𝓵_pos, SpaceTime.distTimeSlice_symm_apply, StandardModel.HiggsField.apply_smooth, StandardModel.HiggsField.inner_smooth, SpaceTime.deriv_zero, StandardModel.HiggsField.apply_im_smooth, SpaceTime.distTensorDeriv_toTensor_basis_repr, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum, SpaceTime.space_toTimeAndSpace_symm, SpaceTime.instIsAddHaarMeasureVolume, Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero, SpaceTime.deriv_eq, Electromagnetism.ElectromagneticPotential.harmonicWaveX_differentiable, Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distDeriv_comp_lorentz_action, StandardModel.HiggsField.const_apply, Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold, SpaceTime.spaceTime_integral_eq_time_space_integral, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv, SpaceTime.timeSpaceBasis_eq_map_basis, StandardModel.HiggsField.inner_zero_right, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonneg_𝓵_pos, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, SpaceTime.timeSliceLinearEquiv_symm_apply, StandardModel.HiggsField.Potential.toFun_smooth, SpaceTime.distDeriv_commute, SpaceTime.distTensorDeriv_equivariant, SpaceTime.contDiff_vector, SpaceTime.toTimeAndSpace_basis_inl', StandardModel.HiggsField.inner_add_left, SpaceTime.distTimeSlice_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add, Electromagnetism.LorentzCurrentDensity.chargeDensity_zero, SpaceTime.instIsOpenPosMeasureVolume, SpaceTime.timeSliceLinearEquiv_apply, SpaceTime.time_val_toCoord_symm, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single, Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply, SpaceTime.toTimeAndSpace_basis_inr, SpaceTime.boost_zero_apply_time_space, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, SpaceTime.time_toTimeAndSpace_symm, SpaceTime.distTimeSlice_distDeriv_inr, StandardModel.HiggsField.inner_neg_right, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, SpaceTime.instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution, Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, StandardModel.HiggsField.Potential.eq_zero_iff_of_μSq_nonpos_𝓵_pos, Electromagnetism.LorentzCurrentDensity.currentDensity_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, SpaceTime.coord_apply, StandardModel.HiggsField.inner_neg_left, SpaceTime.distDeriv_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, StandardModel.HiggsField.Potential.isMaxOn_iff_field_of_𝓵_neg, StandardModel.HiggsField.inner_add_right, SpaceTime.apply_fderiv_eq_distDeriv, SpaceTime.toTimeAndSpace_symm_apply_inr, StandardModel.HiggsField.normSq_expand, SpaceTime.instBorelSpace, StandardModel.HiggsField.Potential.toFun_zero, SpaceTime.det_timeSpaceBasisEquiv, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.ElectromagneticPotential.isExtrema_iff_gradLagrangian, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, StandardModel.HiggsField.apply_re_smooth, StandardModel.HiggsField.Potential.isMaxOn_iff_isMinOn_neg, Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux, SpaceTime.timeSpaceBasis_addHaar, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, SpaceTime.toTimeAndSpace_symm_apply_inl, StandardModel.HiggsField.inner_eq_expand, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux, Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply, StandardModel.HiggsField.inner_zero_left, StandardModel.HiggsField.inner_expand_conj, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, SpaceTime.boost_x_smul, StandardModel.HiggsField.toHiggsVec_smooth, SpaceTime.instIsFiniteMeasureOnCompactsVolume, Electromagnetism.DistElectromagneticPotential.infiniteWire_isExterma, Electromagnetism.ElectromagneticPotential.kineticTerm_const, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, StandardModel.HiggsField.Potential.isMinOn_iff_of_μSq_nonneg_𝓵_pos, StandardModel.HiggsField.const_normSq, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_𝓵_pos, SpaceTime.schwartzAction_surjective, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, StandardModel.HiggsField.Potential.toFun_eq_zero_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, StandardModel.HiggsField.Potential.isMinOn_iff_field_of_μSq_nonpos_𝓵_pos, Electromagnetism.ElectromagneticPotential.harmonicWaveX_contDiff, StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec, Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero, StandardModel.HiggsField.inner_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.constantEB_isExtrema, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, SpaceTime.schwartzAction_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.deriv_equivariant, SpaceTime.schwartzAction_mul_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, SpaceTime.distDeriv_inl_distTimeSlice_symm, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isExtrema, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis, SpaceTime.lorentzGroup_smul_dist_apply, Electromagnetism.ElectromagneticPotential.constantEB_smooth, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, StandardModel.HiggsField.contDiff, StandardModel.HiggsField.normSq_zero, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, SpaceTime.timeSpaceBasis_apply_inr, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_components, SpaceTime.timeSpaceBasis_apply_inl, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, SpaceTime.distTensorDeriv_apply, SpaceTime.space_toCoord_symm, Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr, SpaceTime.schwartzAction_injective

---

← Back to Index