Space 📖 | CompData | 621 mathmath: Space.distOfFunction_neg, Space.IsDistBounded.integrable_space_fderiv, Space.vsub_apply, QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrl, Space.constantTime_spaceCurlD, Space.fderiv_space_components, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Space.continuous_time_integral, Space.deriv_eq_fderiv_fun, Space.IsDistBounded.isDistBounded_smul_inner_of_smul_norm, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', SpaceTime.distTimeSlice_distDeriv_inl, Space.contDiffOn_vsub, Space.div_smul, 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.instSFiniteRadialAngularMeasure, Space.IsDistBounded.inv_shift, QuantumMechanics.SpaceDHilbertSpace.memHS_iff, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Space.slice_symm_apply_succAbove, QuantumMechanics.angularMomentum_commutation_radiusRegPow, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Space.time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Space.integral_volume_eq_spherical, Space.schwartzMap_slice_integral_differentiable, Space.gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, Space.norm_sq_eq, Space.volume_eq_addHaar, QuantumMechanics.radiusRegPow_commutation_momentumSqr, QuantumMechanics.radiusRegPowOperator_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Space.differentiable_normPowerSeries_inv, QuantumMechanics.radiusRegPowOperatorSchwartz_isSymmetric, 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, QuantumMechanics.SpaceDHilbertSpace.zero_memHS, Space.differentiable_vadd, Space.apply_eq_basis_repr_apply, ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv, QuantumMechanics.SpaceDHilbertSpace.toBra_surjective, 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, QuantumMechanics.position_comp_radiusRegPow_commute, 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.SpaceDHilbertSpace.toBra_injective, 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.lintegral_radialMeasure_eq_spherical_mul, QuantumMechanics.position_commutation_momentum_momentum, Space.IsDistBounded.isDistBounded_mul_inner', Space.fderiv_fun_slice_symm_left_apply, SpaceTime.space_toTimeAndSpace_symm, Space.schwartMap_fderiv_comm, Space.distCurl_distConst, QuantumMechanics.comp_eq_comp_sub_commute, Space.distCurl_apply_two, Space.distSpaceDeriv_apply', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Space.normPowerSeries_tendsto, QuantumMechanics.lie_leibniz, Space.curl_zero, Space.manifoldStructure_comp_manifoldStructure_symm_apply, Space.pow_mul_iteratedFDeriv_norm_le, Space.integrable_isDistBounded_inner_grad_schwartzMap_spherical, Space.time_integral_iteratedFDeriv_eq, QuantumMechanics.radiusPowOperator_apply_stronglyMeasurable, Space.time_integral_hasFDerivAt, Space.translateSchwartz_apply, Space.inner_apply_differentiable, HasVarAdjoint.grad, Space.basis_self_eq_slice, Space.curl_of_grad_eq_zero, 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, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_of_smooth, Space.distCurl_apply, Space.integral_one_dim_eq_integral_real, Space.range_manifoldStructure, Space.basis_apply, QuantumMechanics.position_commutation_radiusRegPow, Space.IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, Space.oneEquiv_symm_coe, QuantumMechanics.SpaceDHilbertSpace.coe_hilbertSpace_memHS, Space.gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, Space.IsDistBounded.nat_pow_shift, Space.distDeriv_distConst, Space.contDiffOn_vadd, Space.schwartzMap_slice_bound, Space.fderiv_val, Space.IsDistBounded.zpow_smul_repr_self, HasVarAdjDerivAt.gradient, 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, SpaceTime.spaceTime_integral_eq_time_space_integral, Space.mk_contDiff, QuantumMechanics.momentum_comp_angularMomentum_eq, Space.normPowerSeries_inv_le, QuantumMechanics.comp_eq_comp_add_commute, Space.grad_norm_sq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.SpaceDHilbertSpace.inner_mk_mk, Space.add_apply, ClassicalMechanics.wave_differentiable, QuantumMechanics.SpaceDHilbertSpace.memHS_const_smul, Space.basis_eq_mfderiv_modelDiffeo_single, Space.curl_smul, Space.normPowerSeries_eq_rpow, Space.zero_val, Space.instNonempty, Space.basis_repr_apply, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space, SpaceTime.deriv_sum_inl, Space.deriv_inner_right, QuantumMechanics.radiusRegPowOperator_apply_fun, Space.fderiv_vadd, Space.finrank_eq_dim, Space.vadd_zero_sub_vadd_zero, ClassicalMechanics.planeWave_differentiable, QuantumMechanics.positionOperatorSqr_eq, Space.fderiv_time_commute_fderiv_space, QuantumMechanics.angularMomentum_commutation_position, IsTestFunction.gradient, Space.IsDistBounded.norm_smul_nat_pow, Space.vadd_hasTemperateGrowth, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Space.deriv_eq_fderiv_basis, Space.nsmul_apply, Space.time_deriv_differentiable_space, Space.lintegral_radialMeasure, 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, QuantumMechanics.positionOperatorSchwartz_isSymmetric, 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, QuantumMechanics.radiusRegPow_commutation_momentum, 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, Space.deriv_coord_2nd_add, Electromagnetism.ElectromagneticPotential.electricField_differentiable, Space.contMDiff_vaddConst, Space.manifoldStructure_comp_manifoldStructure_symm, 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, QuantumMechanics.angularMomentumSqr_commutation_radiusRegPow, Space.norm_slice_symm_eq, Space.deriv_coord_add, 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.div_of_curl_eq_zero, Space.fderiv_time_eq_fderiv_curry, Space.distGrad_apply, QuantumMechanics.SpaceDHilbertSpace.mk_add, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Space.norm_lt_normPowerSeries, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, Space.deriv_add, Electromagnetism.LorentzCurrentDensity.chargeDensity_zero, SpaceTime.timeSliceLinearEquiv_apply, Space.radialAngularMeasure_real_closedBall, Space.curl_const, SpaceTime.toTimeAndSpace_basis_inr, Space.schwartzMap_slice_integral_contDiff, Space.gradient_dist_normPowerSeries_zpow, Space.integrableOn_norm_rpow_iff_of_isBounded_nhds, SpaceTime.boost_zero_apply_time_space, QuantumMechanics.HydrogenAtom.lrlOperator_eq'', Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, QuantumMechanics.SpaceDHilbertSpace.memHS_add, Space.basis_inner, Space.normPowerSeries_eq, Space.distDeriv_constantSliceDist_same, Space.IsDistBounded.add, Space.inner_contDiff, QuantumMechanics.radiusPowOperator_apply, QuantumMechanics.momentumSqr_comp_momentum_commute, 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, QuantumMechanics.radiusPowOperator_apply_fun, 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.IsDistBounded.isDistBounded_mul_inner_of_smul_norm, Space.fderiv_basis_repr, Space.distTimeDeriv_apply_CLM, Space.integrableOn_norm_rpow_ball_iff, Space.schwartzMap_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperatorSqr_apply, QuantumMechanics.momentum_comp_position_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Space.distDeriv_constantSliceDist_succAbove, Space.vsub_differentiable, QuantumMechanics.position_commutation_momentumSqr, Space.grad_add, 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.integrableOn_norm_rpow_shell, 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, QuantumMechanics.HydrogenAtom.hamiltonianReg_commutation_lrl, Space.gradient_eq_grad, QuantumMechanics.HydrogenAtom.lrl_commutation_lrl, QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrlSqr, 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, Space.distDiv_apply_eq_sum_fderivD, SpaceTime.toTimeAndSpace_symm_apply_inr, Space.deriv_eq, Space.distDiv_ofFunction, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Space.integrableOn_norm_rpow_of_isBounded_compl_nhds, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, Space.grad_inner_space_unit_vector, Space.distGrad_distOfFunction_log_norm, ClassicalMechanics.planeWave_eq, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_inner, Space.constantTime_distSpaceDiv, Space.IsDistBounded.norm_add_pos_nat_zpow, Space.IsDistBounded.isDistBounded_mul_inner, Space.schwartzMap_slice_integral_hasFDerivAt, Space.curl_linear_map, QuantumMechanics.HydrogenAtom.lrlOperator_eq', QuantumMechanics.HydrogenAtom.lrlOperatorSqr_eq, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space, Space.grad_eq_gradiant, Space.integrable_time_integral, Space.inner_apply_contDiff, Space.slice_symm_apply, Space.contDiff_grad, Space.basis_repr_inner_eq, Space.radialAngularMeasure_integrable_pow_neg_two, QuantumMechanics.SpaceDHilbertSpace.eLpNorm_mk, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, Space.eval_contDiff, QuantumMechanics.position_position_commutation_momentum, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Space.div_linear_map, 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, Space.lintegral_volume_eq_spherical, Electromagnetism.ElectromagneticPotential.electricField_contDiff, Space.grad_inner_repr_eq, Space.distOfFunction_inner, Space.schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, QuantumMechanics.SpaceDHilbertSpace.mem_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Space.IsDistBounded.mul_inner_pow_neg_two, Space.inner_vadd_zero, Space.distDiv_distConst, QuantumMechanics.momentumOperatorSchwartz_isSymmetric, 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.deriv_eq_mfderiv, Space.distDeriv_apply, QuantumMechanics.radiusPowOperator_apply_memHS, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_coe_ae, 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, Space.deriv_differentiable, Space.curl_sub, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Space.distGrad_eq_sum_basis, Space.distDiv_apply_eq_sum_distDeriv, QuantumMechanics.angularMomentumSqr_commutation_momentumSqr, Space.gradSchwartz_apply_eq_grad, QuantumMechanics.normRegularizedPow_hasTemperateGrowth, 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.curl_neg, QuantumMechanics.momentumSqr_comp_angularMomentum_commute, Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.aeEqFun_mk_mem_iff, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, Space.vadd_differentiable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, SpaceTime.toTimeAndSpace_symm_fderiv, Space.integrable_isDistBounded_inner_grad_schwartzMap, QuantumMechanics.HydrogenAtom.lrlOperator_eq, 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, Space.deriv_smul, Space.dist_eq_norm, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Space.gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, Space.modelDiffeo_apply, 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.deriv_const_smul, Space.IsDistBounded.aestronglyMeasurable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.leibniz_lie, Space.differentiable_normPowerSeries_zpow, QuantumMechanics.angularMomentumOperator_apply, Space.IsDistBounded.normPowerSeries_fderiv, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, Space.constantTime_distSpaceDeriv, QuantumMechanics.radiusRegPowOperator_comp_eq, Space.oneEquiv_symm_continuous, Space.instNontrivialSucc, Space.norm_vadd_le_add, Space.deriv_contDiff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, Space.sub_apply, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, Space.integrableOn_norm_rpow_ball_compl_iff, Space.smul_vadd_zero, Space.IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, Space.fderiv_normPowerSeries, QuantumMechanics.SpaceDHilbertSpace.val_eq_coe, Space.curl_add, Space.schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, Space.grad_inner_right, IsTestFunction.of_div, Space.IsDistBounded.isDistBounded_smul_self, Space.inner_basis, Space.integrableOn_norm_rpow_of_compl_nhds, Space.fderiv_slice_symm_left_apply, Space.schwartzMap_slice_integral_iteratedFDeriv, Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.position_comp_commute, Space.constantSliceDist_apply, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, QuantumMechanics.SpaceDHilbertSpace.aeStronglyMeasurable_of_memHS, Space.oneEquiv_symm_measurableEmbedding, Space.vadd_apply, Space.deriv_eq_mfderiv_manifoldStructure, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Space.IsDistBounded.inv_pow_smul_self, QuantumMechanics.angularMomentum_commutation_momentumSqr, 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, QuantumMechanics.radiusRegPowOperator_zero, IsLocalizedFunctionTransform.gradient, ClassicalMechanics.planeWave_apply_space_deriv_space_deriv, Space.IsDistBounded.comp_add_right, divergence_eq_space_div, Space.Direction.norm, Space.IsDistBounded.inv_pow_smul_repr_self, Space.IsDistBounded.nat_pow, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, Space.distSpaceDeriv_commute, QuantumMechanics.momentum_comp_radiusRegPow_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, QuantumMechanics.momentum_comp_commute, Space.fderiv_fun_slice_symm_right_apply, Space.normPowerSeries_zpow_le_norm_sq_add_one, QuantumMechanics.SpaceDHilbertSpace.ext_iff, Space.instFiniteDimensionalReal, QuantumMechanics.momentumOperatorSqr_eq, QuantumMechanics.angularMomentum_commutation_momentum, Space.distDiv_distTranslate, ClassicalMechanics.planeWave_differentiable_space, QuantumMechanics.SpaceDHilbertSpace.schwartzSubmodule_dense, QuantumMechanics.norm_sq_add_unit_sq_pos, QuantumMechanics.SpaceDHilbertSpace.toBra_apply, Space.mdifferentiable_manifoldStructure_iff_differentiable, Space.abs_eval_le_norm, Space.eq_vadd_zero, Time.deriv_contDiff_of_space, Space.distDeriv_commute, Space.distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, Space.add_vadd_zero, Electromagnetism.ElectromagneticPotential.magneticField_div_eq_zero, Space.grad_smul, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, Space.apply_fderiv_eq_distTimeDeriv, Space.distGrad_eq_of_inner, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, Space.distGrad_toFun_eq_distDeriv, Space.fderiv_space_eq_fderiv_curry, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Space.integrable_radialAngularMeasure_of_spherical, HasVarAdjDerivAt.grad, Space.eval_differentiable, Space.IsDistBounded.inv, SpaceTime.distDeriv_inl_distTimeSlice_symm, Space.timeIntegralSchwartz_apply, Space.div_add, 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, Space.volume_metricBall_three_real, QuantumMechanics.SpaceDHilbertSpace.coe_mk_ae, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Space.grad_inner, Space.instSubsingletonOfNatNat, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, Space.curl_of_curl, Space.instHasTemperateGrowthRadialAngularMeasure, Space.radialAngularMeasure_closedBall, QuantumMechanics.radiusRegPow_commutation_radiusRegPow, Space.iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, QuantumMechanics.radiusPowOperator_apply_contDiffAt, Space.oneEquiv_measurePreserving, Space.IsDistBounded.norm_add, Space.IsDistBounded.aeStronglyMeasurable_inv_pow, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Space.add_val, Space.grad_inner_space, Space.deriv_coord_2nd_sub, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, Space.iteratedFDeriv_norm_integrable, Space.abs_right_le_norm_slice_symm, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, QuantumMechanics.SpaceDHilbertSpace.mk_const_smul, 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, QuantumMechanics.HydrogenAtom.angularMomentumSqr_commutation_lrlSqr, SpaceTime.toTimeAndSpace_symm_apply_time_space, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, QuantumMechanics.SpaceDHilbertSpace.mk_eq_iff, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, HasVarAdjDerivAt.div, Space.inner_apply_differentiableAt, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_space_of_smooth, Space.grad_inner_left, Space.sub_val, Space.constantTime_distSpaceGrad, Space.apply_fderiv_eq_distSpaceDeriv, Space.inner_differentiableAt, Space.distCurl_distGrad_eq_zero, Space.lintegral_volume_eq_spherical_mul, 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
|