| Name | Category | Theorems |
|---|
Direction π | CompData | β |
basis π | CompOp | 69 mathmath: fderiv_basis_repr_symm, volume_eq_addHaar, apply_eq_basis_repr_apply, IsDistBounded.isDistBounded_smul_self_repr, distSpaceDeriv_apply, basis_repr_symm_apply, basis_succAbove_eq_slice, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, HasVarAdjoint.gradient, schwartMap_fderiv_comm, distCurl_apply_two, distSpaceDeriv_apply', translateSchwartz_apply, basis_self_eq_slice, distCurl_apply, basis_apply, IsDistBounded.zpow_smul_repr_self, HasVarAdjDerivAt.gradient, grad_norm_sq, basis_repr_apply, deriv_eq_fderiv_basis, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, distCurl_apply_one, distGrad_inner_eq, gradient_dist_normPowerSeries_log, gradient_dist_normPowerSeries_zpow_tendsTo, repr_grad_inner_eq, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, SpaceTime.toTimeAndSpace_basis_inr, gradient_dist_normPowerSeries_zpow, basis_inner, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, distCurl_apply_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, fderiv_basis_repr, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, gradient_eq_grad, distTranslate_ofFunction, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, distDiv_apply_eq_sum_fderivD, deriv_eq, grad_inner_space_unit_vector, distGrad_distOfFunction_log_norm, grad_eq_gradiant, basis_repr_inner_eq, translateSchwartz_coe_eq, grad_inner_repr_eq, distDeriv_apply, distGrad_distOfFunction_norm_zpow, distGrad_eq_sum_basis, IsLocalizedFunctionTransform.div_comp_repr, ClassicalMechanics.wave_dx2, gradient_eq_sum, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, grad_inner_right, inner_basis, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential, divergence_eq_space_div, IsDistBounded.inv_pow_smul_repr_self, grad_inner, grad_inner_space, gradient_dist_normPowerSeries_log_tendsTo, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, grad_inner_left, apply_fderiv_eq_distSpaceDeriv, basis_self
|
coord π | CompOp | 4 mathmath: coordCLM_apply, coord_apply, coord_contDiff, IsTestFunction.coord
|
coordCLM π | CompOp | 1 mathmath: coordCLM_apply
|
equivPi π | CompOp | 2 mathmath: fderiv_val, fderiv_mk
|
instAdd π | CompOp | 7 mathmath: add_apply, IsDistBounded.norm_smul_nat_pow, IsDistBounded.norm_smul_zpow, IsDistBounded.comp_add_right, add_vadd_zero, IsDistBounded.norm_add, add_val
|
instAddActionEuclideanSpaceRealFin π | CompOp | β |
instAddCommGroup π | CompOp | 68 mathmath: IsDistBounded.integrable_space_fderiv, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, time_integral_differentiable, schwartzMap_slice_integral_differentiable, differentiable_normPowerSeries_inv, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_space, differentiable_log_normPowerSeries, fderiv_slice_symm_right_apply, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, Electromagnetism.ElectromagneticPotential.electricField_differentiable_space, time_integral_hasFDerivAt, fderiv_val, normPowerSeries_differentiable, ClassicalMechanics.wave_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space, vadd_zero_sub_vadd_zero, ClassicalMechanics.planeWave_differentiable, fderiv_time_commute_fderiv_space, deriv_eq_fderiv_basis, time_deriv_differentiable_space, SpaceTime.timeSlice_differentiable, Electromagnetism.ElectromagneticPotential.electricField_differentiable, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, fderiv_slice_symm, repr_grad_inner_eq, fderiv_normPowerSeries_zpow, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space, fderiv_eq_sum_deriv, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, fderiv_basis_repr, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_space, mk_differentiable, deriv_eq, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, schwartzMap_slice_integral_hasFDerivAt, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space, IsDistBounded.integrable_space_fderiv_mul, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, norm_sq_differentiable, grad_inner_repr_eq, deriv_differentiable, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, iteratedFDeriv_integrable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, ClassicalMechanics.wave_dx2, differentiable_normPowerSeries_zpow, IsDistBounded.normPowerSeries_fderiv, sub_apply, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, fderiv_normPowerSeries, fderiv_slice_symm_left_apply, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, instFiniteDimensionalReal, ClassicalMechanics.planeWave_differentiable_space, eval_differentiable, integrable_fderiv_space, inner_differentiable, fderiv_mk, fderiv_normPowerSeries_tendsto, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, sub_val, inner_differentiableAt, fderiv_log_normPowerSeries, schwartzMap_iteratedFDeriv_slice_symm_integrable
|
instAddCommMonoid π | CompOp | 102 mathmath: Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, schwartzMap_fderiv_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, slice_symm_apply_succAbove, SpaceTime.spaceTime_integrable_iff_space_time_integrable, schwartzMap_slice_integral_differentiable, nsmul_val, distSpaceDeriv_apply, fderiv_slice_symm_right_apply, schwartzMap_slice_integral_iteratedFDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, basis_succAbove_eq_slice, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, sum_apply, SpaceTime.deriv_sum_inr, SpaceTime.toTimeAndSpace_symm_measurePreserving, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, integrable_isDistBounded_inner_grad_schwartzMap_spherical, time_integral_iteratedFDeriv_eq, basis_self_eq_slice, time_integral_iteratedFDeriv_norm_le, schwartzMap_slice_bound, fderiv_val, SpaceTime.spaceTime_integral_eq_time_space_integral, SpaceTime.deriv_sum_inl, finrank_eq_dim, ClassicalMechanics.planeWave_differentiable, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, nsmul_apply, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, schwartzMap_integrable_slice_symm, continuous_schwartzMap_slice_integral, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, coordCLM_apply, SpaceTime.timeSlice_differentiable, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, schwartzMap_fderiv_left_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.electricField_differentiable, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, norm_slice_symm_eq, rank_eq_dim, fderiv_slice_symm, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, SpaceTime.boost_zero_apply_time_space, SpaceTime.time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, schwartzMap_slice_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, SpaceTime.toTimeAndSpace_symm_apply_inr, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, schwartzMap_slice_integral_hasFDerivAt, slice_symm_apply, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, norm_left_le_norm_slice_symm, SpaceTime.toTimeAndSpace_symm_apply_inl, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, gradient_eq_sum, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, fderiv_slice_symm_left_apply, schwartzMap_slice_integral_iteratedFDeriv, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, distTimeDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, fderiv_mk, slice_symm_apply_self, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, abs_right_le_norm_slice_symm, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, time_integral_mul_pow_iteratedFDeriv_norm_le, sliceSchwartz_apply, SpaceTime.space_toCoord_symm, schwartzMap_iteratedFDeriv_slice_symm_integrable, slice_symm_measurableEmbedding
|
instCoeFunForallFinReal π | CompOp | β |
instInnerProductSpaceReal π | CompOp | 261 mathmath: distOfFunction_neg, IsDistBounded.integrable_space_fderiv, constantTime_spaceCurlD, continuous_time_integral, SpaceTime.distTimeSlice_distDeriv_inl, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, schwartzMap_slice_integral_differentiable, gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, volume_eq_addHaar, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, IsDistBounded.integrable_space, volume_metricBall_two, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, apply_eq_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, distOfFunction_smul, IsDistBounded.isDistBounded_smul_self_repr, volume_metricBall_two_real, distSpaceDeriv_apply, distOfFunction_smul_fun, QuantumMechanics.angularMomentumOperator1D_trivial, IsDistBounded.integral_mul_schwartzMap_bounded, basis_repr_symm_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, schwartzMap_slice_integral_iteratedFDeriv_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, basis_succAbove_eq_slice, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, IsDistBounded.integrable_time_space, radialAngularMeasure_zero_eq_volume, SpaceTime.distTimeSlice_symm_apply, QuantumMechanics.angularMomentumOperatorSqr_apply_fun, oneEquiv_symm_measurePreserving, Electromagnetism.LorentzCurrentDensity.chargeDensity_contDiff, HasVarAdjoint.gradient, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_space, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, schwartMap_fderiv_comm, distCurl_distConst, distCurl_apply_two, distSpaceDeriv_apply', pow_mul_iteratedFDeriv_norm_le, integrable_isDistBounded_inner_grad_schwartzMap_spherical, time_integral_iteratedFDeriv_eq, time_integral_hasFDerivAt, translateSchwartz_apply, HasVarAdjoint.grad, basis_self_eq_slice, distTimeDeriv_apply', IsDistBounded.integrable_space_mul, time_integral_iteratedFDeriv_norm_le, distOfFunction_apply, distTranslate_apply, distCurl_apply, basis_apply, IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, distDeriv_distConst, schwartzMap_slice_bound, IsDistBounded.zpow_smul_repr_self, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, QuantumMechanics.momentum_momentum_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, mk_contDiff, grad_norm_sq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, basis_repr_apply, QuantumMechanics.angularMomentum_commutation_position, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, deriv_eq_fderiv_basis, volume_metricBall_three, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, distCurl_apply_one, integrable_radialAngularMeasure_iff, schwartzMap_integrable_slice_symm, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, distGrad_inner_eq, continuous_schwartzMap_slice_integral, distOfFunction_zero_eq_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, distGrad_distConst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, QuantumMechanics.positionOperator_apply, QuantumMechanics.momentum_commutation_momentum, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, gradient_dist_normPowerSeries_log, schwartzMap_fderiv_left_integrable_slice_symm, gradient_dist_normPowerSeries_zpow_tendsTo, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperator_apply_fun, IsDistBounded.integrable_mul_inv_pow, QuantumMechanics.momentumSqr_commutation_momentum, SpaceTime.distTimeSlice_apply, repr_grad_inner_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, distGrad_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, gradient_dist_normPowerSeries_zpow, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, basis_inner, distDeriv_constantSliceDist_same, inner_contDiff, QuantumMechanics.position_commutation_momentum, SpaceTime.distTimeSlice_distDeriv_inr, QuantumMechanics.angularMomentumSqr_commutation_angularMomentum, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, distCurl_apply_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_contDiff, fderiv_basis_repr, distTimeDeriv_apply_CLM, schwartzMap_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, distDeriv_constantSliceDist_succAbove, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_space, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, gradient_eq_grad, distTranslate_ofFunction, distTranslate_distGrad, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, QuantumMechanics.momentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.position_commutation_position, QuantumMechanics.angularMomentumSqr_commutation_position, distDiv_apply_eq_sum_fderivD, deriv_eq, distDiv_ofFunction, grad_inner_space_unit_vector, distGrad_distOfFunction_log_norm, constantTime_distSpaceDiv, schwartzMap_slice_integral_hasFDerivAt, grad_eq_gradiant, integrable_time_integral, basis_repr_inner_eq, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, eval_contDiff, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, IsDistBounded.integrable_space_fderiv_mul, time_integral_iteratedFDeriv_apply, translateSchwartz_coe_eq, QuantumMechanics.angularMomentumOperator_antisymm, normPowerSeries_aestronglyMeasurable, Electromagnetism.ElectromagneticPotential.electricField_contDiff, grad_inner_repr_eq, distOfFunction_inner, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, distDiv_distConst, radialAngularMeasure_eq_volume_withDensity, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, distOfFunction_vector_eval, distDeriv_apply, distOfFunction_mul_fun, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, QuantumMechanics.angularMomentumOperator_eq_zero, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, distGrad_distOfFunction_norm_zpow, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.LorentzCurrentDensity.currentDensity_ContDiff, coord_contDiff, SpaceTime.timeSlice_contDiff, distGrad_eq_sum_basis, distDiv_apply_eq_sum_distDeriv, HasVarAdjoint.div, integral_radialAngularMeasure, iteratedFDeriv_integrable, QuantumMechanics.positionOperator_apply_fun, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_space, QuantumMechanics.momentumOperator_apply, IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, integrable_isDistBounded_inner_grad_schwartzMap, IsLocalizedFunctionTransform.div_comp_repr, ClassicalMechanics.wave_dx2, distSpaceGrad_apply, gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, IsDistBounded.aestronglyMeasurable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.angularMomentumOperator_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, constantTime_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, grad_inner_right, inner_basis, schwartzMap_slice_integral_iteratedFDeriv, distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, constantSliceDist_apply, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, time_integral_contDiff, Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff_space, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, IsLocalizedFunctionTransform.gradient, divergence_eq_space_div, IsDistBounded.inv_pow_smul_repr_self, distSpaceDeriv_commute, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, QuantumMechanics.angularMomentum_commutation_momentum, distDiv_distTranslate, distDeriv_commute, distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, apply_fderiv_eq_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, distGrad_toFun_eq_distDeriv, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, SpaceTime.distDeriv_inl_distTimeSlice_symm, timeIntegralSchwartz_apply, distTimeDeriv_commute_distSpaceDeriv, constantTime_apply, integrable_fderiv_space, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, grad_inner, iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, oneEquiv_measurePreserving, IsDistBounded.aeStronglyMeasurable_inv_pow, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, grad_inner_space, iteratedFDeriv_norm_integrable, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, gradient_dist_normPowerSeries_log_tendsTo, distOfFunction_eculid_eval, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, grad_inner_left, constantTime_distSpaceGrad, apply_fderiv_eq_distSpaceDeriv, distCurl_distGrad_eq_zero, distSpaceDeriv_apply_CLM, constantTime_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, basis_self, time_integral_mul_pow_iteratedFDeriv_norm_le, sliceSchwartz_apply, schwartzMap_iteratedFDeriv_slice_symm_integrable
|
instInnerReal π | CompOp | 39 mathmath: IsDistBounded.isDistBounded_smul_inner_of_smul_norm, IsDistBounded.isDistBounded_smul_inner, ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv, IsDistBounded.isDistBounded_mul_inner', inner_apply_differentiable, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv, ClassicalMechanics.wave_differentiable, deriv_inner_right, inner_apply, fderiv_normPowerSeries_zpow, basis_inner, inner_contDiff, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv, IsDistBounded.isDistBounded_mul_inner_of_smul_norm, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_magneticFunction, ClassicalMechanics.planeWave_eq, IsDistBounded.isDistBounded_mul_inner, inner_apply_contDiff, basis_repr_inner_eq, IsDistBounded.mul_inner_pow_neg_two, inner_vadd_zero, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_electricFunction, deriv_inner_left, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv, ClassicalMechanics.wave_dx2, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv, fderiv_normPowerSeries, grad_inner_right, inner_basis, inner_differentiable, fderiv_normPowerSeries_tendsto, grad_inner, inner_eq_sum, deriv_eq_inner_self, inner_apply_differentiableAt, grad_inner_left, inner_differentiableAt, fderiv_log_normPowerSeries
|
instMeasurableSpace π | CompOp | 46 mathmath: IsDistBounded.integrable_space_fderiv, SpaceTime.spaceTime_integrable_iff_space_time_integrable, volume_eq_addHaar, IsDistBounded.integrable_space, volume_metricBall_two, volume_metricBall_two_real, oneEquiv_measurableEmbedding, IsDistBounded.integral_mul_schwartzMap_bounded, IsDistBounded.integrable_time_space, radialAngularMeasure_zero_eq_volume, oneEquiv_symm_measurePreserving, HasVarAdjoint.gradient, SpaceTime.toTimeAndSpace_symm_measurePreserving, integrable_isDistBounded_inner_grad_schwartzMap_spherical, HasVarAdjoint.grad, IsDistBounded.integrable_space_mul, distOfFunction_apply, IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, HasVarAdjDerivAt.gradient, SpaceTime.spaceTime_integral_eq_time_space_integral, volume_metricBall_three, integrable_radialAngularMeasure_iff, IsDistBounded.integrable_mul_inv_pow, distDiv_inv_pow_eq_dim, distDiv_ofFunction, radialAngularMeasure_integrable_pow_neg_two, IsDistBounded.integrable_space_fderiv_mul, normPowerSeries_aestronglyMeasurable, distOfFunction_inner, radialAngularMeasure_eq_volume_withDensity, instBorelSpace, HasVarAdjoint.div, integral_radialAngularMeasure, IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, integrable_isDistBounded_inner_grad_schwartzMap, IsDistBounded.aestronglyMeasurable, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, oneEquiv_symm_measurableEmbedding, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, HasVarAdjDerivAt.grad, instHasTemperateGrowthRadialAngularMeasure, oneEquiv_measurePreserving, IsDistBounded.aeStronglyMeasurable_inv_pow, HasVarAdjDerivAt.div, slice_symm_measurableEmbedding
|
instModuleReal π | CompOp | 147 mathmath: IsDistBounded.integrable_space_fderiv, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, slice_symm_apply_succAbove, time_integral_differentiable, SpaceTime.spaceTime_integrable_iff_space_time_integrable, schwartzMap_slice_integral_differentiable, differentiable_normPowerSeries_inv, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_space, differentiable_log_normPowerSeries, oneEquiv_measurableEmbedding, fderiv_slice_symm_right_apply, schwartzMap_slice_integral_iteratedFDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, basis_succAbove_eq_slice, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, oneEquiv_symm_measurePreserving, Electromagnetism.ElectromagneticPotential.electricField_differentiable_space, SpaceTime.deriv_sum_inr, SpaceTime.toTimeAndSpace_symm_measurePreserving, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, integrable_isDistBounded_inner_grad_schwartzMap_spherical, time_integral_iteratedFDeriv_eq, time_integral_hasFDerivAt, basis_self_eq_slice, time_integral_iteratedFDeriv_norm_le, oneEquiv_symm_coe, schwartzMap_slice_bound, fderiv_val, normPowerSeries_differentiable, SpaceTime.spaceTime_integral_eq_time_space_integral, ClassicalMechanics.wave_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space, SpaceTime.deriv_sum_inl, finrank_eq_dim, ClassicalMechanics.planeWave_differentiable, fderiv_time_commute_fderiv_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, deriv_eq_fderiv_basis, time_deriv_differentiable_space, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, schwartzMap_integrable_slice_symm, continuous_schwartzMap_slice_integral, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, coordCLM_apply, SpaceTime.timeSlice_differentiable, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, schwartzMap_fderiv_left_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.electricField_differentiable, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, norm_slice_symm_eq, rank_eq_dim, fderiv_slice_symm, repr_grad_inner_eq, fderiv_normPowerSeries_zpow, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, SpaceTime.boost_zero_apply_time_space, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space, SpaceTime.time_toTimeAndSpace_symm, fderiv_eq_sum_deriv, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, fderiv_basis_repr, schwartzMap_slice_integral_iteratedFDeriv_norm_le, oneEquiv_coe, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_space, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, mk_differentiable, SpaceTime.toTimeAndSpace_symm_apply_inr, deriv_eq, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, schwartzMap_slice_integral_hasFDerivAt, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space, slice_symm_apply, IsDistBounded.integrable_space_fderiv_mul, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, norm_sq_differentiable, grad_inner_repr_eq, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, norm_left_le_norm_slice_symm, SpaceTime.toTimeAndSpace_symm_apply_inl, deriv_differentiable, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, oneEquiv_symm_apply, ClassicalMechanics.wave_dx2, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, differentiable_normPowerSeries_zpow, IsDistBounded.normPowerSeries_fderiv, oneEquiv_symm_continuous, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, fderiv_normPowerSeries, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, fderiv_slice_symm_left_apply, schwartzMap_slice_integral_iteratedFDeriv, oneEquiv_symm_measurableEmbedding, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, instFiniteDimensionalReal, ClassicalMechanics.planeWave_differentiable_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, eval_differentiable, integrable_fderiv_space, inner_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, fderiv_mk, slice_symm_apply_self, fderiv_normPowerSeries_tendsto, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, oneEquiv_measurePreserving, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, abs_right_le_norm_slice_symm, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, inner_differentiableAt, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, time_integral_mul_pow_iteratedFDeriv_norm_le, fderiv_log_normPowerSeries, sliceSchwartz_apply, SpaceTime.space_toCoord_symm, schwartzMap_iteratedFDeriv_slice_symm_integrable, slice_symm_measurableEmbedding, oneEquiv_continuous
|
instNeg π | CompOp | 3 mathmath: distTranslate_ofFunction, neg_val, neg_apply
|
instNorm π | CompOp | 75 mathmath: norm_le_normPowerSeries, IsDistBounded.inv_shift, gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, norm_sq_eq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, IsDistBounded.zpow_smul_self, IsDistBounded.norm_mul_isDistBounded, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, normPowerSeries_tendsto, pow_mul_iteratedFDeriv_norm_le, gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, IsDistBounded.nat_pow_shift, schwartzMap_slice_bound, IsDistBounded.zpow_smul_repr_self, normPowerSeries_log_le, deriv_normPowerSeries_tendsto, dist_eq, normPowerSeries_inv_le, grad_norm_sq, normPowerSeries_eq_rpow, IsDistBounded.norm_smul_nat_pow, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, IsDistBounded.pow, integrable_radialAngularMeasure_iff, IsDistBounded.norm_sub, gradient_dist_normPowerSeries_zpow_tendsTo, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, IsDistBounded.integrable_mul_inv_pow, norm_slice_symm_eq, norm_lt_normPowerSeries, normPowerSeries_eq, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, IsDistBounded.pow_shift, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, grad_inner_space_unit_vector, distGrad_distOfFunction_log_norm, IsDistBounded.norm_add_pos_nat_zpow, radialAngularMeasure_integrable_pow_neg_two, norm_sq_differentiable, IsDistBounded.norm_add_nat_pow, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, IsDistBounded.mul_inner_pow_neg_two, radialAngularMeasure_eq_volume_withDensity, norm_eq, IsDistBounded.log_norm, norm_left_le_norm_slice_symm, IsDistBounded.norm_smul_isDistBounded, distGrad_distOfFunction_norm_zpow, IsDistBounded.norm_smul_zpow, integral_radialAngularMeasure, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, IsDistBounded.norm, normPowerSeries_le_norm_sq_add_one, IsDistBounded.inv_pow_smul_self, normPowerSeries_inv_tendsto, Direction.norm, IsDistBounded.inv_pow_smul_repr_self, IsDistBounded.nat_pow, normPowerSeries_zpow_le_norm_sq_add_one, abs_eval_le_norm, IsDistBounded.inv, norm_vadd_zero, fderiv_normPowerSeries_tendsto, iteratedFDeriv_norm_mul_pow_integrable, IsDistBounded.norm_add, IsDistBounded.aeStronglyMeasurable_inv_pow, grad_inner_space, abs_right_le_norm_slice_symm, gradient_dist_normPowerSeries_log_tendsTo, time_integral_mul_pow_iteratedFDeriv_norm_le, deriv_norm_sq
|
instNormedAddCommGroup π | CompOp | 272 mathmath: distOfFunction_neg, IsDistBounded.integrable_space_fderiv, constantTime_spaceCurlD, continuous_time_integral, SpaceTime.distTimeSlice_distDeriv_inl, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, IsDistBounded.inv_shift, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, schwartzMap_slice_integral_differentiable, gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, volume_eq_addHaar, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, IsDistBounded.integrable_space, volume_metricBall_two, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, apply_eq_basis_repr_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, IsDistBounded.zpow_smul_self, distOfFunction_smul, IsDistBounded.isDistBounded_smul_self_repr, volume_metricBall_two_real, distSpaceDeriv_apply, distOfFunction_smul_fun, QuantumMechanics.angularMomentumOperator1D_trivial, IsDistBounded.integral_mul_schwartzMap_bounded, basis_repr_symm_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, schwartzMap_slice_integral_iteratedFDeriv_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, basis_succAbove_eq_slice, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, IsDistBounded.integrable_time_space, radialAngularMeasure_zero_eq_volume, SpaceTime.distTimeSlice_symm_apply, QuantumMechanics.angularMomentumOperatorSqr_apply_fun, oneEquiv_symm_measurePreserving, Electromagnetism.LorentzCurrentDensity.chargeDensity_contDiff, HasVarAdjoint.gradient, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_space, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, schwartMap_fderiv_comm, distCurl_distConst, distCurl_apply_two, distSpaceDeriv_apply', pow_mul_iteratedFDeriv_norm_le, integrable_isDistBounded_inner_grad_schwartzMap_spherical, time_integral_iteratedFDeriv_eq, time_integral_hasFDerivAt, translateSchwartz_apply, HasVarAdjoint.grad, basis_self_eq_slice, distTimeDeriv_apply', IsDistBounded.integrable_space_mul, time_integral_iteratedFDeriv_norm_le, distOfFunction_apply, distTranslate_apply, distCurl_apply, basis_apply, IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, IsDistBounded.nat_pow_shift, distDeriv_distConst, schwartzMap_slice_bound, IsDistBounded.zpow_smul_repr_self, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, QuantumMechanics.momentum_momentum_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, mk_contDiff, grad_norm_sq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, basis_repr_apply, QuantumMechanics.angularMomentum_commutation_position, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, deriv_eq_fderiv_basis, volume_metricBall_three, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, distCurl_apply_one, integrable_radialAngularMeasure_iff, schwartzMap_integrable_slice_symm, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, distGrad_inner_eq, continuous_schwartzMap_slice_integral, distOfFunction_zero_eq_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, distGrad_distConst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, IsDistBounded.norm_sub, QuantumMechanics.positionOperator_apply, IsDistBounded.comp_sub_right, QuantumMechanics.momentum_commutation_momentum, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, gradient_dist_normPowerSeries_log, schwartzMap_fderiv_left_integrable_slice_symm, gradient_dist_normPowerSeries_zpow_tendsTo, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperator_apply_fun, IsDistBounded.integrable_mul_inv_pow, QuantumMechanics.momentumSqr_commutation_momentum, SpaceTime.distTimeSlice_apply, repr_grad_inner_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, distGrad_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, gradient_dist_normPowerSeries_zpow, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, basis_inner, distDeriv_constantSliceDist_same, inner_contDiff, QuantumMechanics.position_commutation_momentum, SpaceTime.distTimeSlice_distDeriv_inr, QuantumMechanics.angularMomentumSqr_commutation_angularMomentum, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, distCurl_apply_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_contDiff, fderiv_basis_repr, distTimeDeriv_apply_CLM, schwartzMap_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, distDeriv_constantSliceDist_succAbove, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, IsDistBounded.pow_shift, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_space, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, gradient_eq_grad, distTranslate_ofFunction, distTranslate_distGrad, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, QuantumMechanics.momentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.position_commutation_position, QuantumMechanics.angularMomentumSqr_commutation_position, distDiv_apply_eq_sum_fderivD, deriv_eq, distDiv_ofFunction, grad_inner_space_unit_vector, distGrad_distOfFunction_log_norm, constantTime_distSpaceDiv, schwartzMap_slice_integral_hasFDerivAt, grad_eq_gradiant, integrable_time_integral, basis_repr_inner_eq, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, eval_contDiff, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, IsDistBounded.integrable_space_fderiv_mul, time_integral_iteratedFDeriv_apply, translateSchwartz_coe_eq, QuantumMechanics.angularMomentumOperator_antisymm, normPowerSeries_aestronglyMeasurable, Electromagnetism.ElectromagneticPotential.electricField_contDiff, grad_inner_repr_eq, distOfFunction_inner, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, distDiv_distConst, radialAngularMeasure_eq_volume_withDensity, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, distOfFunction_vector_eval, distDeriv_apply, distOfFunction_mul_fun, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, QuantumMechanics.angularMomentumOperator_eq_zero, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, distGrad_distOfFunction_norm_zpow, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.LorentzCurrentDensity.currentDensity_ContDiff, coord_contDiff, SpaceTime.timeSlice_contDiff, distGrad_eq_sum_basis, distDiv_apply_eq_sum_distDeriv, HasVarAdjoint.div, integral_radialAngularMeasure, iteratedFDeriv_integrable, QuantumMechanics.positionOperator_apply_fun, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_space, QuantumMechanics.momentumOperator_apply, IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, integrable_isDistBounded_inner_grad_schwartzMap, IsLocalizedFunctionTransform.div_comp_repr, ClassicalMechanics.wave_dx2, distSpaceGrad_apply, gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, IsDistBounded.aestronglyMeasurable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.angularMomentumOperator_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, constantTime_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, grad_inner_right, IsDistBounded.isDistBounded_smul_self, inner_basis, schwartzMap_slice_integral_iteratedFDeriv, distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, constantSliceDist_apply, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, IsDistBounded.inv_pow_smul_self, time_integral_contDiff, Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff_space, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, IsLocalizedFunctionTransform.gradient, divergence_eq_space_div, IsDistBounded.inv_pow_smul_repr_self, distSpaceDeriv_commute, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, QuantumMechanics.angularMomentum_commutation_momentum, distDiv_distTranslate, distDeriv_commute, distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, apply_fderiv_eq_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, distGrad_toFun_eq_distDeriv, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, SpaceTime.distDeriv_inl_distTimeSlice_symm, timeIntegralSchwartz_apply, distTimeDeriv_commute_distSpaceDeriv, constantTime_apply, integrable_fderiv_space, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, IsLocalizedFunctionTransform.div, IsLocalizedFunctionTransform.grad, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, grad_inner, instHasTemperateGrowthRadialAngularMeasure, iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, oneEquiv_measurePreserving, IsDistBounded.aeStronglyMeasurable_inv_pow, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, grad_inner_space, iteratedFDeriv_norm_integrable, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, gradient_dist_normPowerSeries_log_tendsTo, distOfFunction_eculid_eval, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, grad_inner_left, constantTime_distSpaceGrad, apply_fderiv_eq_distSpaceDeriv, distCurl_distGrad_eq_zero, distSpaceDeriv_apply_CLM, constantTime_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, basis_self, time_integral_mul_pow_iteratedFDeriv_norm_le, sliceSchwartz_apply, schwartzMap_iteratedFDeriv_slice_symm_integrable
|
instSMulReal π | CompOp | 10 mathmath: IsDistBounded.zpow_smul_self, smul_val, SpaceTime.toTimeAndSpace_basis_inl', grad_inner_space_unit_vector, gradient_eq_sum, smul_vadd_zero, IsDistBounded.isDistBounded_smul_self, IsDistBounded.inv_pow_smul_self, smul_apply, grad_inner_space
|
instSeminormedAddCommGroup π | CompOp | 163 mathmath: IsDistBounded.integrable_space_fderiv, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, continuous_time_integral, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, slice_symm_apply_succAbove, time_integral_differentiable, SpaceTime.spaceTime_integrable_iff_space_time_integrable, schwartzMap_slice_integral_differentiable, differentiable_normPowerSeries_inv, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_space, volume_metricBall_two, differentiable_log_normPowerSeries, volume_metricBall_two_real, oneEquiv_measurableEmbedding, fderiv_slice_symm_right_apply, schwartzMap_slice_integral_iteratedFDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, basis_succAbove_eq_slice, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, oneEquiv_symm_measurePreserving, Electromagnetism.ElectromagneticPotential.electricField_differentiable_space, HasVarAdjoint.gradient, SpaceTime.deriv_sum_inr, SpaceTime.toTimeAndSpace_symm_measurePreserving, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, pow_mul_iteratedFDeriv_norm_le, time_integral_iteratedFDeriv_eq, time_integral_hasFDerivAt, basis_self_eq_slice, time_integral_iteratedFDeriv_norm_le, oneEquiv_symm_coe, schwartzMap_slice_bound, fderiv_val, HasVarAdjDerivAt.gradient, normPowerSeries_differentiable, dist_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, ClassicalMechanics.wave_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space, SpaceTime.deriv_sum_inl, ClassicalMechanics.planeWave_differentiable, fderiv_time_commute_fderiv_space, IsTestFunction.gradient, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, deriv_eq_fderiv_basis, time_deriv_differentiable_space, volume_metricBall_three, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, schwartzMap_integrable_slice_symm, continuous_schwartzMap_slice_integral, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, coordCLM_apply, SpaceTime.timeSlice_differentiable, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, schwartzMap_fderiv_left_integrable_slice_symm, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.electricField_differentiable, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, norm_slice_symm_eq, fderiv_slice_symm, repr_grad_inner_eq, fderiv_normPowerSeries_zpow, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, SpaceTime.boost_zero_apply_time_space, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space, SpaceTime.time_toTimeAndSpace_symm, fderiv_eq_sum_deriv, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, fderiv_basis_repr, schwartzMap_slice_integral_iteratedFDeriv_norm_le, oneEquiv_coe, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_space, distDiv_inv_pow_eq_dim, gradient_eq_grad, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, mk_differentiable, SpaceTime.toTimeAndSpace_symm_apply_inr, deriv_eq, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, schwartzMap_slice_integral_hasFDerivAt, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space, grad_eq_gradiant, slice_symm_apply, IsDistBounded.integrable_space_fderiv_mul, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, norm_sq_differentiable, grad_inner_repr_eq, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, instBorelSpace, norm_left_le_norm_slice_symm, SpaceTime.toTimeAndSpace_symm_apply_inl, deriv_differentiable, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, mk_continuous, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, iteratedFDeriv_integrable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, oneEquiv_symm_apply, ClassicalMechanics.wave_dx2, eval_continuous, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, gradient_eq_sum, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, differentiable_normPowerSeries_zpow, IsDistBounded.normPowerSeries_fderiv, oneEquiv_symm_continuous, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, fderiv_normPowerSeries, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, fderiv_slice_symm_left_apply, schwartzMap_slice_integral_iteratedFDeriv, oneEquiv_symm_measurableEmbedding, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, IsLocalizedFunctionTransform.gradient, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, ClassicalMechanics.planeWave_differentiable_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, eval_differentiable, integrable_fderiv_space, inner_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, fderiv_mk, slice_symm_apply_self, fderiv_normPowerSeries_tendsto, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, iteratedFDeriv_norm_mul_pow_integrable, oneEquiv_measurePreserving, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, iteratedFDeriv_norm_integrable, abs_right_le_norm_slice_symm, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, inner_differentiableAt, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, time_integral_mul_pow_iteratedFDeriv_norm_le, fderiv_log_normPowerSeries, sliceSchwartz_apply, SpaceTime.space_toCoord_symm, schwartzMap_iteratedFDeriv_slice_symm_integrable, slice_symm_measurableEmbedding, oneEquiv_continuous
|
instVAddEuclideanSpaceRealFin π | CompOp | 9 mathmath: vadd_zero_sub_vadd_zero, vadd_val, vadd_transitive, inner_vadd_zero, smul_vadd_zero, vadd_apply, eq_vadd_zero, add_vadd_zero, norm_vadd_zero
|
instZero π | CompOp | 30 mathmath: fderiv_basis_repr_symm, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_eq_magneticFieldMatrix, volume_metricBall_two, volume_metricBall_two_real, RigidBody.solidSphere_centerOfMass, zero_apply, fderiv_fun_slice_symm_left_apply, basis_self_eq_slice, distTimeDeriv_apply', zero_val, vadd_zero_sub_vadd_zero, volume_metricBall_three, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, SpaceTime.toTimeAndSpace_basis_inl', fderiv_time_eq_fderiv_curry, point_dim_zero_eq, fderiv_basis_repr, distDiv_inv_pow_eq_dim, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField, inner_vadd_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, smul_vadd_zero, fderiv_slice_symm_left_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, eq_vadd_zero, distTimeDeriv_apply, add_vadd_zero, apply_fderiv_eq_distTimeDeriv, norm_vadd_zero, SpaceTime.toTimeAndSpace_basis_inl
|
oneEquiv π | CompOp | 9 mathmath: oneEquiv_measurableEmbedding, oneEquiv_symm_measurePreserving, oneEquiv_symm_coe, oneEquiv_coe, oneEquiv_symm_apply, oneEquiv_symm_continuous, oneEquiv_symm_measurableEmbedding, oneEquiv_measurePreserving, oneEquiv_continuous
|
oneEquivCLE π | CompOp | β |
termπ π | CompOp | β |
toDirection π | CompOp | β |
val π | CompOp | 91 mathmath: Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField, slice_symm_apply_succAbove, norm_sq_eq, Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv, apply_eq_basis_repr_apply, ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv, nsmul_val, basis_repr_symm_apply, zero_apply, sum_apply, basis_apply, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ, fderiv_val, deriv_normPowerSeries_tendsto, add_apply, zero_val, basis_repr_apply, deriv_inner_right, nsmul_apply, vadd_val, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ', QuantumMechanics.positionOperator_apply, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ, Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ, smul_val, inner_apply, coord_apply, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv, Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix, SpaceTime.boost_zero_apply_time_space, basis_inner, Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix, fderiv_eq_sum_deriv, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv, oneEquiv_coe, eq_of_apply_iff, deriv_normPowerSeries, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_zero, ClassicalMechanics.planeWave_space_deriv_space_deriv, direction_unit_sq_sum, SpaceTime.toTimeAndSpace_symm_apply_inr, val_eq_iff, deriv_component, IsTestFunction.space_component, deriv_normPowerSeries_zpow, slice_symm_apply, eval_contDiff, neg_val, norm_eq, ClassicalMechanics.planeWave_space_deriv, deriv_inner_left, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, QuantumMechanics.positionOperator_apply_fun, neg_apply, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv, oneEquiv_symm_apply, ClassicalMechanics.wave_dx2, eval_continuous, ClassicalMechanics.planeWave_apply_space_deriv, Electromagnetism.ElectromagneticPotential.IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator, deriv_component_diff, sub_apply, inner_basis, vadd_apply, ClassicalMechanics.planeWave_apply_space_deriv_space_deriv, Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ_space_deriv_zero, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, deriv_component_same, abs_eval_le_norm, IsDistBounded.component_smul_isDistBounded, eval_differentiable, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix, smul_apply, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv, slice_symm_apply_self, Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator, IsDistBounded.component_mul_isDistBounded, deriv_log_normPowerSeries, add_val, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero, inner_eq_sum, deriv_eq_inner_self, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ, deriv_component_sq, sub_val, basis_self, SpaceTime.space_toCoord_symm, deriv_norm_sq
|
| Name | Category | Theorems |
|---|
Space π | CompData | 468 mathmath: Space.distOfFunction_neg, Space.IsDistBounded.integrable_space_fderiv, Space.constantTime_spaceCurlD, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Space.continuous_time_integral, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', SpaceTime.distTimeSlice_distDeriv_inl, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Space.fderiv_basis_repr_symm, Space.IsDistBounded.isDistBounded_smul_inner, Space.norm_le_normPowerSeries, Space.schwartzMap_fderiv_integrable_slice_symm, Space.IsDistBounded.inv_shift, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Space.slice_symm_apply_succAbove, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Space.time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Space.schwartzMap_slice_integral_differentiable, Space.gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, Space.norm_sq_eq, Space.volume_eq_addHaar, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Space.differentiable_normPowerSeries_inv, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_space, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFunction_eq_magneticFieldMatrix, Space.IsDistBounded.integrable_space, Space.volume_metricBall_two, Space.differentiable_log_normPowerSeries, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, Space.apply_eq_basis_repr_apply, ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Space.IsDistBounded.zpow_smul_self, Space.distOfFunction_smul, Space.IsDistBounded.isDistBounded_smul_self_repr, Space.volume_metricBall_two_real, RigidBody.solidSphere_centerOfMass, Space.IsDistBounded.norm_mul_isDistBounded, Space.nsmul_val, Space.oneEquiv_measurableEmbedding, Space.distSpaceDeriv_apply, Space.distOfFunction_smul_fun, QuantumMechanics.angularMomentumOperator1D_trivial, Space.IsDistBounded.integral_mul_schwartzMap_bounded, Space.fderiv_slice_symm_right_apply, Space.basis_repr_symm_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Space.schwartzMap_slice_integral_iteratedFDeriv_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, Space.basis_succAbove_eq_slice, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, Space.IsDistBounded.integrable_time_space, Space.zero_apply, Space.radialAngularMeasure_zero_eq_volume, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, Space.sum_apply, Space.IsDistBounded.sum, QuantumMechanics.angularMomentumOperatorSqr_apply_fun, Space.grad_zero, Space.oneEquiv_symm_measurePreserving, Electromagnetism.ElectromagneticPotential.electricField_differentiable_space, Electromagnetism.LorentzCurrentDensity.chargeDensity_contDiff, HasVarAdjoint.gradient, SpaceTime.deriv_sum_inr, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_space, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, Space.IsDistBounded.isDistBounded_mul_inner', SpaceTime.space_toTimeAndSpace_symm, Space.schwartMap_fderiv_comm, Space.distCurl_distConst, Space.distCurl_apply_two, Space.distSpaceDeriv_apply', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Space.normPowerSeries_tendsto, Space.curl_zero, Space.pow_mul_iteratedFDeriv_norm_le, Space.integrable_isDistBounded_inner_grad_schwartzMap_spherical, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_hasFDerivAt, Space.translateSchwartz_apply, HasVarAdjoint.grad, Space.basis_self_eq_slice, Space.distTimeDeriv_apply', Space.IsDistBounded.integrable_space_mul, Space.time_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv, Space.distOfFunction_apply, Space.distTranslate_apply, Space.distCurl_apply, Space.basis_apply, Space.IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, Space.oneEquiv_symm_coe, Space.gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, Space.IsDistBounded.nat_pow_shift, Space.distDeriv_distConst, Space.schwartzMap_slice_bound, Space.fderiv_val, Space.IsDistBounded.zpow_smul_repr_self, Space.normPowerSeries_differentiable, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, Space.normPowerSeries_log_le, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, Space.deriv_normPowerSeries_tendsto, Space.dist_eq, QuantumMechanics.momentum_momentum_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, Space.mk_contDiff, Space.normPowerSeries_inv_le, Space.grad_norm_sq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Space.add_apply, ClassicalMechanics.wave_differentiable, Space.normPowerSeries_eq_rpow, Space.zero_val, Space.basis_repr_apply, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space, SpaceTime.deriv_sum_inl, Space.deriv_inner_right, Space.finrank_eq_dim, Space.vadd_zero_sub_vadd_zero, ClassicalMechanics.planeWave_differentiable, QuantumMechanics.angularMomentum_commutation_position, Space.IsDistBounded.norm_smul_nat_pow, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Space.deriv_eq_fderiv_basis, Space.nsmul_apply, Space.vadd_val, Space.volume_metricBall_three, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Space.distCurl_apply_one, Space.IsDistBounded.pow, Space.integrable_radialAngularMeasure_iff, Space.schwartzMap_integrable_slice_symm, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Space.distGrad_inner_eq, Space.continuous_schwartzMap_slice_integral, Space.distOfFunction_zero_eq_zero, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Space.coordCLM_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Space.distGrad_distConst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, Space.IsDistBounded.norm_sub, QuantumMechanics.positionOperator_apply, Space.IsDistBounded.comp_sub_right, QuantumMechanics.momentum_commutation_momentum, SpaceTime.timeSlice_differentiable, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, Space.gradient_dist_normPowerSeries_log, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, SpaceTime.timeSliceLinearEquiv_symm_apply, Space.schwartzMap_fderiv_left_integrable_slice_symm, Space.gradient_dist_normPowerSeries_zpow_tendsTo, Space.smul_val, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, Space.schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.electricField_differentiable, QuantumMechanics.angularMomentumOperator_apply_fun, Space.IsDistBounded.integrable_mul_inv_pow, SpaceTime.toTimeAndSpace_basis_inl', Space.inner_apply, QuantumMechanics.momentumSqr_commutation_momentum, Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, Space.norm_slice_symm_eq, Space.rank_eq_dim, Space.fderiv_slice_symm, SpaceTime.distTimeSlice_apply, Space.repr_grad_inner_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, Space.fderiv_normPowerSeries_zpow, Space.distGrad_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Space.norm_lt_normPowerSeries, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, Electromagnetism.LorentzCurrentDensity.chargeDensity_zero, SpaceTime.timeSliceLinearEquiv_apply, Space.curl_const, SpaceTime.toTimeAndSpace_basis_inr, Space.schwartzMap_slice_integral_contDiff, Space.gradient_dist_normPowerSeries_zpow, SpaceTime.boost_zero_apply_time_space, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, Space.basis_inner, Space.normPowerSeries_eq, Space.distDeriv_constantSliceDist_same, Space.IsDistBounded.add, Space.inner_contDiff, QuantumMechanics.position_commutation_momentum, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space, SpaceTime.time_toTimeAndSpace_symm, Space.fderiv_eq_sum_deriv, Space.point_dim_zero_eq, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, SpaceTime.distTimeSlice_distDeriv_inr, QuantumMechanics.angularMomentumSqr_commutation_angularMomentum, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff, Space.vadd_transitive, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, Space.distCurl_apply_zero, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_contDiff, Space.fderiv_basis_repr, Space.distTimeDeriv_apply_CLM, Space.schwartzMap_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Space.distDeriv_constantSliceDist_succAbove, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Space.IsDistBounded.pow_shift, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_magneticFunction, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_space, Space.oneEquiv_coe, Space.IsDistBounded.zpow_smul_repr_self_sub, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_space, Space.distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, Space.gradient_eq_grad, Space.distTranslate_ofFunction, Space.distTranslate_distGrad, Electromagnetism.LorentzCurrentDensity.currentDensity_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, QuantumMechanics.momentumOperatorSqr_apply, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, ClassicalMechanics.planeWave_space_deriv_space_deriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, Space.mk_differentiable, QuantumMechanics.position_commutation_position, QuantumMechanics.angularMomentumSqr_commutation_position, Space.distDiv_apply_eq_sum_fderivD, SpaceTime.toTimeAndSpace_symm_apply_inr, Space.deriv_eq, Space.distDiv_ofFunction, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, Space.distGrad_distOfFunction_log_norm, ClassicalMechanics.planeWave_eq, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField, Space.constantTime_distSpaceDiv, Space.IsDistBounded.norm_add_pos_nat_zpow, Space.IsDistBounded.isDistBounded_mul_inner, Space.schwartzMap_slice_integral_hasFDerivAt, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space, Space.grad_eq_gradiant, Space.integrable_time_integral, Space.slice_symm_apply, Space.basis_repr_inner_eq, Space.radialAngularMeasure_integrable_pow_neg_two, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, Space.eval_contDiff, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Space.IsDistBounded.integrable_space_fderiv_mul, Space.neg_val, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, Space.norm_sq_differentiable, Space.time_integral_iteratedFDeriv_apply, Space.IsDistBounded.norm_add_nat_pow, Space.translateSchwartz_coe_eq, QuantumMechanics.angularMomentumOperator_antisymm, Space.normPowerSeries_aestronglyMeasurable, Electromagnetism.ElectromagneticPotential.electricField_contDiff, Space.grad_inner_repr_eq, Space.distOfFunction_inner, Space.schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Space.IsDistBounded.mul_inner_pow_neg_two, Space.inner_vadd_zero, Space.distDiv_distConst, Space.radialAngularMeasure_eq_volume_withDensity, Space.norm_eq, Space.instBorelSpace, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_electricFunction, Space.distOfFunction_vector_eval, Space.IsDistBounded.log_norm, Space.distDeriv_apply, Space.norm_left_le_norm_slice_symm, Space.IsDistBounded.norm_smul_isDistBounded, Space.distOfFunction_mul_fun, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, QuantumMechanics.angularMomentumOperator_eq_zero, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, SpaceTime.toTimeAndSpace_symm_apply_inl, Space.distGrad_distOfFunction_norm_zpow, Space.IsDistBounded.norm_smul_zpow, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.LorentzCurrentDensity.currentDensity_ContDiff, Space.coord_contDiff, SpaceTime.timeSlice_contDiff, Electromagnetism.ElectromagneticPotential.harmonicWaveX_scalarPotential_eq_zero, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Space.distGrad_eq_sum_basis, Space.distDiv_apply_eq_sum_distDeriv, ClassicalMechanics.planeWave_space_deriv, Space.deriv_inner_left, HasVarAdjoint.div, Space.mk_continuous, Space.grad_neg, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Space.integral_radialAngularMeasure, Space.iteratedFDeriv_integrable, QuantumMechanics.positionOperator_apply_fun, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_space, Space.neg_apply, QuantumMechanics.momentumOperator_apply, Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, SpaceTime.toTimeAndSpace_symm_fderiv, Space.integrable_isDistBounded_inner_grad_schwartzMap, Space.IsDistBounded.norm, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv, SpaceTime.toTimeAndSpace_fderiv, IsLocalizedFunctionTransform.div_comp_repr, Space.oneEquiv_symm_apply, ClassicalMechanics.wave_dx2, Space.eval_continuous, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, ClassicalMechanics.planeWave_apply_space_deriv, Space.grad_const, Space.distSpaceGrad_apply, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Space.gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv, Space.normPowerSeries_le_norm_sq_add_one, Space.IsDistBounded.aestronglyMeasurable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, Space.differentiable_normPowerSeries_zpow, QuantumMechanics.angularMomentumOperator_apply, Space.IsDistBounded.normPowerSeries_fderiv, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, Space.constantTime_distSpaceDeriv, Space.oneEquiv_symm_continuous, Space.instNontrivialSucc, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, Space.sub_apply, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, Space.smul_vadd_zero, Space.IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, Space.fderiv_normPowerSeries, Space.schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, Space.grad_inner_right, Space.IsDistBounded.isDistBounded_smul_self, Space.inner_basis, Space.fderiv_slice_symm_left_apply, Space.schwartzMap_slice_integral_iteratedFDeriv, Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Space.constantSliceDist_apply, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, Space.oneEquiv_symm_measurableEmbedding, Space.vadd_apply, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Space.IsDistBounded.inv_pow_smul_self, Space.time_integral_contDiff, Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff_space, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Space.normPowerSeries_inv_tendsto, IsLocalizedFunctionTransform.gradient, ClassicalMechanics.planeWave_apply_space_deriv_space_deriv, Space.IsDistBounded.comp_add_right, Space.Direction.norm, Space.IsDistBounded.inv_pow_smul_repr_self, Space.IsDistBounded.nat_pow, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, Space.distSpaceDeriv_commute, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, Space.normPowerSeries_zpow_le_norm_sq_add_one, Space.instFiniteDimensionalReal, QuantumMechanics.angularMomentum_commutation_momentum, Space.distDiv_distTranslate, ClassicalMechanics.planeWave_differentiable_space, Space.abs_eval_le_norm, Space.eq_vadd_zero, Space.distDeriv_commute, Space.distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, Space.add_vadd_zero, Electromagnetism.ElectromagneticPotential.magneticField_div_eq_zero, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, Space.apply_fderiv_eq_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, Space.distGrad_toFun_eq_distDeriv, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Space.eval_differentiable, Space.IsDistBounded.inv, SpaceTime.distDeriv_inl_distTimeSlice_symm, Space.timeIntegralSchwartz_apply, Space.distTimeDeriv_commute_distSpaceDeriv, Space.constantTime_apply, Space.integrable_fderiv_space, Space.inner_differentiable, Space.IsDistBounded.zero, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Space.norm_vadd_zero, IsLocalizedFunctionTransform.div, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, Space.fderiv_mk, Space.smul_apply, IsLocalizedFunctionTransform.grad, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, Space.slice_symm_apply_self, Space.fderiv_normPowerSeries_tendsto, Space.div_const, SpaceTime.toTimeAndSpace_basis_inl, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Space.grad_inner, Space.instSubsingletonOfNatNat, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, Space.instHasTemperateGrowthRadialAngularMeasure, Space.iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, Space.oneEquiv_measurePreserving, Space.IsDistBounded.norm_add, Space.IsDistBounded.aeStronglyMeasurable_inv_pow, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Space.add_val, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, Space.iteratedFDeriv_norm_integrable, Space.abs_right_le_norm_slice_symm, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, Space.inner_eq_sum, Space.deriv_eq_inner_self, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, Space.gradient_dist_normPowerSeries_log_tendsTo, Space.IsDistBounded.const_smul, Space.distOfFunction_eculid_eval, SpaceTime.toTimeAndSpace_symm_apply_time_space, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, Space.grad_inner_left, Space.sub_val, Space.constantTime_distSpaceGrad, Space.apply_fderiv_eq_distSpaceDeriv, Space.inner_differentiableAt, Space.distCurl_distGrad_eq_zero, Space.distSpaceDeriv_apply_CLM, Space.constantTime_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, Space.div_zero, Space.basis_self, Space.time_integral_mul_pow_iteratedFDeriv_norm_le, Space.fderiv_log_normPowerSeries, Space.sliceSchwartz_apply, SpaceTime.space_toCoord_symm, Space.schwartzMap_iteratedFDeriv_slice_symm_integrable, Space.slice_symm_measurableEmbedding, Space.deriv_norm_sq, Space.oneEquiv_continuous
|