| Name | Category | Theorems |
|---|
Direction π | CompData | β |
basis π | CompOp | 72 mathmath: deriv_eq_fderiv_fun, 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_eq_mfderiv_modelDiffeo_single, 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, deriv_eq_mfderiv, 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
|
instAddCommGroup π | CompOp | 79 mathmath: IsDistBounded.integrable_space_fderiv, fderiv_space_components, deriv_eq_fderiv_fun, 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, differentiable_vadd, fderiv_slice_symm_right_apply, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, Electromagnetism.ElectromagneticPotential.electricField_differentiable_space, fderiv_fun_slice_symm_left_apply, time_integral_hasFDerivAt, fderiv_val, normPowerSeries_differentiable, ClassicalMechanics.wave_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space, fderiv_vadd, 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, fderiv_time_eq_fderiv_curry, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space, fderiv_eq_sum_deriv, ClassicalMechanics.wave_fderiv_inner_eq_inner_fderiv_proj, fderiv_basis_repr, vsub_differentiable, 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, vadd_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, fderiv_fun_slice_symm_right_apply, instFiniteDimensionalReal, ClassicalMechanics.planeWave_differentiable_space, mdifferentiable_manifoldStructure_iff_differentiable, fderiv_space_eq_fderiv_curry, 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 | 109 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, integral_volume_eq_spherical, 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, fderiv_fun_slice_symm_left_apply, 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, fderiv_vadd, 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, fderiv_time_eq_fderiv_curry, 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, lintegral_volume_eq_spherical, 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, fderiv_fun_slice_symm_right_apply, distTimeDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, fderiv_space_eq_fderiv_curry, 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
|
instInnerProductSpaceReal π | CompOp | 357 mathmath: distOfFunction_neg, IsDistBounded.integrable_space_fderiv, QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrl, constantTime_spaceCurlD, continuous_time_integral, deriv_eq_fderiv_fun, SpaceTime.distTimeSlice_distDeriv_inl, contDiffOn_vsub, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, QuantumMechanics.SpaceDHilbertSpace.memHS_iff, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff, QuantumMechanics.angularMomentum_commutation_radiusRegPow, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, integral_volume_eq_spherical, schwartzMap_slice_integral_differentiable, gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, volume_eq_addHaar, QuantumMechanics.radiusRegPow_commutation_momentumSqr, QuantumMechanics.radiusRegPowOperator_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, QuantumMechanics.radiusRegPowOperatorSchwartz_isSymmetric, IsDistBounded.integrable_space, volume_metricBall_two, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, apply_eq_basis_repr_apply, QuantumMechanics.SpaceDHilbertSpace.toBra_surjective, 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, QuantumMechanics.position_comp_radiusRegPow_commute, basis_succAbove_eq_slice, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, IsDistBounded.integrable_time_space, radialAngularMeasure_zero_eq_volume, SpaceTime.distTimeSlice_symm_apply, QuantumMechanics.SpaceDHilbertSpace.toBra_injective, 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, lintegral_radialMeasure_eq_spherical_mul, QuantumMechanics.position_commutation_momentum_momentum, schwartMap_fderiv_comm, distCurl_distConst, QuantumMechanics.comp_eq_comp_sub_commute, distCurl_apply_two, distSpaceDeriv_apply', QuantumMechanics.lie_leibniz, pow_mul_iteratedFDeriv_norm_le, integrable_isDistBounded_inner_grad_schwartzMap_spherical, time_integral_iteratedFDeriv_eq, QuantumMechanics.radiusPowOperator_apply_stronglyMeasurable, 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, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_of_smooth, distCurl_apply, integral_one_dim_eq_integral_real, basis_apply, QuantumMechanics.position_commutation_radiusRegPow, IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.coe_hilbertSpace_memHS, gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, distDeriv_distConst, contDiffOn_vadd, schwartzMap_slice_bound, IsDistBounded.zpow_smul_repr_self, HasVarAdjDerivAt.gradient, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, mk_contDiff, QuantumMechanics.momentum_comp_angularMomentum_eq, QuantumMechanics.comp_eq_comp_add_commute, grad_norm_sq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.SpaceDHilbertSpace.inner_mk_mk, basis_eq_mfderiv_modelDiffeo_single, basis_repr_apply, QuantumMechanics.radiusRegPowOperator_apply_fun, QuantumMechanics.positionOperatorSqr_eq, QuantumMechanics.angularMomentum_commutation_position, IsTestFunction.gradient, vadd_hasTemperateGrowth, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, deriv_eq_fderiv_basis, lintegral_radialMeasure, 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.positionOperatorSchwartz_isSymmetric, QuantumMechanics.momentum_commutation_momentum, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, gradient_dist_normPowerSeries_log, QuantumMechanics.radiusRegPow_commutation_momentum, 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, QuantumMechanics.angularMomentumSqr_commutation_radiusRegPow, SpaceTime.distTimeSlice_apply, repr_grad_inner_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, distGrad_apply, QuantumMechanics.SpaceDHilbertSpace.mk_add, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, gradient_dist_normPowerSeries_zpow, integrableOn_norm_rpow_iff_of_isBounded_nhds, QuantumMechanics.HydrogenAtom.lrlOperator_eq'', Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, basis_inner, distDeriv_constantSliceDist_same, inner_contDiff, QuantumMechanics.radiusPowOperator_apply, QuantumMechanics.momentumSqr_comp_momentum_commute, QuantumMechanics.position_commutation_momentum, QuantumMechanics.radiusPowOperator_apply_fun, 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, integrableOn_norm_rpow_ball_iff, schwartzMap_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperatorSqr_apply, QuantumMechanics.momentum_comp_position_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, distDeriv_constantSliceDist_succAbove, QuantumMechanics.position_commutation_momentumSqr, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_space, integrableOn_norm_rpow_shell, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, QuantumMechanics.HydrogenAtom.hamiltonianReg_commutation_lrl, gradient_eq_grad, QuantumMechanics.HydrogenAtom.lrl_commutation_lrl, QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrlSqr, distTranslate_ofFunction, distTranslate_distGrad, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, QuantumMechanics.momentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.position_commutation_position, distDiv_apply_eq_sum_fderivD, deriv_eq, distDiv_ofFunction, integrableOn_norm_rpow_of_isBounded_compl_nhds, grad_inner_space_unit_vector, distGrad_distOfFunction_log_norm, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_inner, constantTime_distSpaceDiv, schwartzMap_slice_integral_hasFDerivAt, QuantumMechanics.HydrogenAtom.lrlOperator_eq', QuantumMechanics.HydrogenAtom.lrlOperatorSqr_eq, grad_eq_gradiant, integrable_time_integral, contDiff_grad, basis_repr_inner_eq, QuantumMechanics.SpaceDHilbertSpace.eLpNorm_mk, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, eval_contDiff, QuantumMechanics.position_position_commutation_momentum, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, IsDistBounded.integrable_space_fderiv_mul, time_integral_iteratedFDeriv_apply, translateSchwartz_coe_eq, QuantumMechanics.angularMomentumOperator_antisymm, normPowerSeries_aestronglyMeasurable, lintegral_volume_eq_spherical, Electromagnetism.ElectromagneticPotential.electricField_contDiff, grad_inner_repr_eq, distOfFunction_inner, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, QuantumMechanics.SpaceDHilbertSpace.mem_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, distDiv_distConst, QuantumMechanics.momentumOperatorSchwartz_isSymmetric, radialAngularMeasure_eq_volume_withDensity, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, distOfFunction_vector_eval, deriv_eq_mfderiv, distDeriv_apply, QuantumMechanics.radiusPowOperator_apply_memHS, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_coe_ae, 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, QuantumMechanics.angularMomentumSqr_commutation_momentumSqr, gradSchwartz_apply_eq_grad, QuantumMechanics.normRegularizedPow_hasTemperateGrowth, HasVarAdjoint.div, integral_radialAngularMeasure, iteratedFDeriv_integrable, QuantumMechanics.positionOperator_apply_fun, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_space, QuantumMechanics.momentumOperator_apply, QuantumMechanics.momentumSqr_comp_angularMomentum_commute, IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.aeEqFun_mk_mem_iff, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, integrable_isDistBounded_inner_grad_schwartzMap, QuantumMechanics.HydrogenAtom.lrlOperator_eq, IsLocalizedFunctionTransform.div_comp_repr, ClassicalMechanics.wave_dx2, distSpaceGrad_apply, gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, modelDiffeo_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, IsDistBounded.aestronglyMeasurable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.leibniz_lie, QuantumMechanics.angularMomentumOperator_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, constantTime_distSpaceDeriv, QuantumMechanics.radiusRegPowOperator_comp_eq, deriv_contDiff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, integrableOn_norm_rpow_ball_compl_iff, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.val_eq_coe, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, grad_inner_right, IsTestFunction.of_div, inner_basis, integrableOn_norm_rpow_of_compl_nhds, schwartzMap_slice_integral_iteratedFDeriv, distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.position_comp_commute, constantSliceDist_apply, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, QuantumMechanics.SpaceDHilbertSpace.aeStronglyMeasurable_of_memHS, QuantumMechanics.angularMomentum_commutation_momentumSqr, time_integral_contDiff, Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff_space, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, QuantumMechanics.radiusRegPowOperator_zero, IsLocalizedFunctionTransform.gradient, divergence_eq_space_div, IsDistBounded.inv_pow_smul_repr_self, distSpaceDeriv_commute, QuantumMechanics.momentum_comp_radiusRegPow_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, QuantumMechanics.momentum_comp_commute, QuantumMechanics.SpaceDHilbertSpace.ext_iff, QuantumMechanics.momentumOperatorSqr_eq, QuantumMechanics.angularMomentum_commutation_momentum, distDiv_distTranslate, QuantumMechanics.SpaceDHilbertSpace.schwartzSubmodule_dense, QuantumMechanics.SpaceDHilbertSpace.toBra_apply, Time.deriv_contDiff_of_space, distDeriv_commute, distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, apply_fderiv_eq_distTimeDeriv, distGrad_eq_of_inner, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, distGrad_toFun_eq_distDeriv, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, HasVarAdjDerivAt.grad, 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, volume_metricBall_three_real, QuantumMechanics.SpaceDHilbertSpace.coe_mk_ae, grad_inner, QuantumMechanics.radiusRegPow_commutation_radiusRegPow, iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, QuantumMechanics.radiusPowOperator_apply_contDiffAt, oneEquiv_measurePreserving, IsDistBounded.aeStronglyMeasurable_inv_pow, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, grad_inner_space, iteratedFDeriv_norm_integrable, QuantumMechanics.SpaceDHilbertSpace.mk_const_smul, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, gradient_dist_normPowerSeries_log_tendsTo, distOfFunction_eculid_eval, QuantumMechanics.HydrogenAtom.angularMomentumSqr_commutation_lrlSqr, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, QuantumMechanics.SpaceDHilbertSpace.mk_eq_iff, HasVarAdjDerivAt.div, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_space_of_smooth, grad_inner_left, constantTime_distSpaceGrad, apply_fderiv_eq_distSpaceDeriv, distCurl_distGrad_eq_zero, lintegral_volume_eq_spherical_mul, 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 | 86 mathmath: IsDistBounded.integrable_space_fderiv, instSFiniteRadialAngularMeasure, QuantumMechanics.SpaceDHilbertSpace.memHS_iff, SpaceTime.spaceTime_integrable_iff_space_time_integrable, integral_volume_eq_spherical, volume_eq_addHaar, QuantumMechanics.radiusRegPowOperatorSchwartz_isSymmetric, IsDistBounded.integrable_space, volume_metricBall_two, QuantumMechanics.SpaceDHilbertSpace.toBra_surjective, volume_metricBall_two_real, oneEquiv_measurableEmbedding, IsDistBounded.integral_mul_schwartzMap_bounded, IsDistBounded.integrable_time_space, radialAngularMeasure_zero_eq_volume, QuantumMechanics.SpaceDHilbertSpace.toBra_injective, oneEquiv_symm_measurePreserving, HasVarAdjoint.gradient, SpaceTime.toTimeAndSpace_symm_measurePreserving, lintegral_radialMeasure_eq_spherical_mul, integrable_isDistBounded_inner_grad_schwartzMap_spherical, QuantumMechanics.radiusPowOperator_apply_stronglyMeasurable, HasVarAdjoint.grad, IsDistBounded.integrable_space_mul, distOfFunction_apply, integral_one_dim_eq_integral_real, IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.coe_hilbertSpace_memHS, HasVarAdjDerivAt.gradient, SpaceTime.spaceTime_integral_eq_time_space_integral, QuantumMechanics.SpaceDHilbertSpace.inner_mk_mk, lintegral_radialMeasure, volume_metricBall_three, integrable_radialAngularMeasure_iff, QuantumMechanics.positionOperatorSchwartz_isSymmetric, IsDistBounded.integrable_mul_inv_pow, QuantumMechanics.SpaceDHilbertSpace.mk_add, radialAngularMeasure_real_closedBall, integrableOn_norm_rpow_iff_of_isBounded_nhds, integrableOn_norm_rpow_ball_iff, integrableOn_norm_rpow_shell, distDiv_inv_pow_eq_dim, distDiv_ofFunction, integrableOn_norm_rpow_of_isBounded_compl_nhds, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_inner, radialAngularMeasure_integrable_pow_neg_two, QuantumMechanics.SpaceDHilbertSpace.eLpNorm_mk, IsDistBounded.integrable_space_fderiv_mul, normPowerSeries_aestronglyMeasurable, lintegral_volume_eq_spherical, distOfFunction_inner, QuantumMechanics.SpaceDHilbertSpace.mem_iff, QuantumMechanics.momentumOperatorSchwartz_isSymmetric, radialAngularMeasure_eq_volume_withDensity, instBorelSpace, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_coe_ae, HasVarAdjoint.div, integral_radialAngularMeasure, IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.aeEqFun_mk_mem_iff, integrable_isDistBounded_inner_grad_schwartzMap, IsDistBounded.aestronglyMeasurable, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, integrableOn_norm_rpow_ball_compl_iff, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.val_eq_coe, integrableOn_norm_rpow_of_compl_nhds, QuantumMechanics.SpaceDHilbertSpace.aeStronglyMeasurable_of_memHS, oneEquiv_symm_measurableEmbedding, QuantumMechanics.SpaceDHilbertSpace.ext_iff, QuantumMechanics.SpaceDHilbertSpace.schwartzSubmodule_dense, QuantumMechanics.SpaceDHilbertSpace.toBra_apply, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, integrable_radialAngularMeasure_of_spherical, HasVarAdjDerivAt.grad, volume_metricBall_three_real, QuantumMechanics.SpaceDHilbertSpace.coe_mk_ae, instHasTemperateGrowthRadialAngularMeasure, radialAngularMeasure_closedBall, oneEquiv_measurePreserving, IsDistBounded.aeStronglyMeasurable_inv_pow, QuantumMechanics.SpaceDHilbertSpace.mk_const_smul, QuantumMechanics.SpaceDHilbertSpace.mk_eq_iff, HasVarAdjDerivAt.div, lintegral_volume_eq_spherical_mul, slice_symm_measurableEmbedding
|
instModuleReal π | CompOp | 161 mathmath: IsDistBounded.integrable_space_fderiv, fderiv_space_components, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, deriv_eq_fderiv_fun, 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, integral_volume_eq_spherical, schwartzMap_slice_integral_differentiable, differentiable_normPowerSeries_inv, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_space, differentiable_log_normPowerSeries, differentiable_vadd, 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, fderiv_fun_slice_symm_left_apply, 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, integral_one_dim_eq_integral_real, 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, fderiv_vadd, 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, fderiv_time_eq_fderiv_curry, 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, vsub_differentiable, 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, lintegral_volume_eq_spherical, 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, vadd_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, fderiv_fun_slice_symm_right_apply, instFiniteDimensionalReal, ClassicalMechanics.planeWave_differentiable_space, mdifferentiable_manifoldStructure_iff_differentiable, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, fderiv_space_eq_fderiv_curry, 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 | 88 mathmath: norm_le_normPowerSeries, IsDistBounded.inv_shift, gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, norm_sq_eq, QuantumMechanics.radiusRegPowOperator_apply, 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, normPowerSeries_inv_le, grad_norm_sq, normPowerSeries_eq_rpow, QuantumMechanics.radiusRegPowOperator_apply_fun, IsDistBounded.norm_smul_nat_pow, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, lintegral_radialMeasure, 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, integrableOn_norm_rpow_iff_of_isBounded_nhds, normPowerSeries_eq, QuantumMechanics.radiusPowOperator_apply, QuantumMechanics.radiusPowOperator_apply_fun, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, integrableOn_norm_rpow_ball_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, IsDistBounded.pow_shift, integrableOn_norm_rpow_shell, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, integrableOn_norm_rpow_of_isBounded_compl_nhds, 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, dist_eq_norm, normPowerSeries_le_norm_sq_add_one, norm_vadd_le_add, integrableOn_norm_rpow_ball_compl_iff, integrableOn_norm_rpow_of_compl_nhds, 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, QuantumMechanics.norm_sq_add_unit_sq_pos, 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 | 368 mathmath: distOfFunction_neg, IsDistBounded.integrable_space_fderiv, QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrl, constantTime_spaceCurlD, continuous_time_integral, deriv_eq_fderiv_fun, SpaceTime.distTimeSlice_distDeriv_inl, contDiffOn_vsub, fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, IsDistBounded.inv_shift, QuantumMechanics.SpaceDHilbertSpace.memHS_iff, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff, QuantumMechanics.angularMomentum_commutation_radiusRegPow, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, integral_volume_eq_spherical, schwartzMap_slice_integral_differentiable, gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm, volume_eq_addHaar, QuantumMechanics.radiusRegPow_commutation_momentumSqr, QuantumMechanics.radiusRegPowOperator_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, QuantumMechanics.radiusRegPowOperatorSchwartz_isSymmetric, IsDistBounded.integrable_space, volume_metricBall_two, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, apply_eq_basis_repr_apply, QuantumMechanics.SpaceDHilbertSpace.toBra_surjective, 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, QuantumMechanics.position_comp_radiusRegPow_commute, basis_succAbove_eq_slice, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, IsDistBounded.integrable_time_space, radialAngularMeasure_zero_eq_volume, SpaceTime.distTimeSlice_symm_apply, QuantumMechanics.SpaceDHilbertSpace.toBra_injective, 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, lintegral_radialMeasure_eq_spherical_mul, QuantumMechanics.position_commutation_momentum_momentum, schwartMap_fderiv_comm, distCurl_distConst, QuantumMechanics.comp_eq_comp_sub_commute, distCurl_apply_two, distSpaceDeriv_apply', QuantumMechanics.lie_leibniz, pow_mul_iteratedFDeriv_norm_le, integrable_isDistBounded_inner_grad_schwartzMap_spherical, time_integral_iteratedFDeriv_eq, QuantumMechanics.radiusPowOperator_apply_stronglyMeasurable, 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, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_of_smooth, distCurl_apply, integral_one_dim_eq_integral_real, basis_apply, QuantumMechanics.position_commutation_radiusRegPow, IsDistBounded.aeStronglyMeasurable_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.coe_hilbertSpace_memHS, gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm, IsDistBounded.nat_pow_shift, distDeriv_distConst, contDiffOn_vadd, schwartzMap_slice_bound, IsDistBounded.zpow_smul_repr_self, HasVarAdjDerivAt.gradient, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, mk_contDiff, QuantumMechanics.momentum_comp_angularMomentum_eq, QuantumMechanics.comp_eq_comp_add_commute, grad_norm_sq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.SpaceDHilbertSpace.inner_mk_mk, basis_eq_mfderiv_modelDiffeo_single, basis_repr_apply, QuantumMechanics.radiusRegPowOperator_apply_fun, QuantumMechanics.positionOperatorSqr_eq, QuantumMechanics.angularMomentum_commutation_position, IsTestFunction.gradient, vadd_hasTemperateGrowth, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, deriv_eq_fderiv_basis, lintegral_radialMeasure, 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, QuantumMechanics.positionOperatorSchwartz_isSymmetric, IsDistBounded.comp_sub_right, QuantumMechanics.momentum_commutation_momentum, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, gradient_dist_normPowerSeries_log, QuantumMechanics.radiusRegPow_commutation_momentum, 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, QuantumMechanics.angularMomentumSqr_commutation_radiusRegPow, SpaceTime.distTimeSlice_apply, repr_grad_inner_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, distGrad_apply, QuantumMechanics.SpaceDHilbertSpace.mk_add, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Electromagnetism.ElectromagneticPotential.harmonicWaveX_isPlaneWave, SpaceTime.toTimeAndSpace_basis_inr, schwartzMap_slice_integral_contDiff, gradient_dist_normPowerSeries_zpow, integrableOn_norm_rpow_iff_of_isBounded_nhds, QuantumMechanics.HydrogenAtom.lrlOperator_eq'', Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, basis_inner, distDeriv_constantSliceDist_same, inner_contDiff, QuantumMechanics.radiusPowOperator_apply, QuantumMechanics.momentumSqr_comp_momentum_commute, QuantumMechanics.position_commutation_momentum, QuantumMechanics.radiusPowOperator_apply_fun, 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, integrableOn_norm_rpow_ball_iff, schwartzMap_slice_integral_iteratedFDeriv_norm_le, QuantumMechanics.angularMomentumOperatorSqr_apply, QuantumMechanics.momentum_comp_position_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, distDeriv_constantSliceDist_succAbove, QuantumMechanics.position_commutation_momentumSqr, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, IsDistBounded.pow_shift, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_space, integrableOn_norm_rpow_shell, IsDistBounded.zpow_smul_repr_self_sub, distDiv_inv_pow_eq_dim, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, QuantumMechanics.HydrogenAtom.hamiltonianReg_commutation_lrl, gradient_eq_grad, QuantumMechanics.HydrogenAtom.lrl_commutation_lrl, QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrlSqr, distTranslate_ofFunction, distTranslate_distGrad, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, QuantumMechanics.momentumOperatorSqr_apply, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, QuantumMechanics.position_commutation_position, distDiv_apply_eq_sum_fderivD, deriv_eq, distDiv_ofFunction, integrableOn_norm_rpow_of_isBounded_compl_nhds, grad_inner_space_unit_vector, distGrad_distOfFunction_log_norm, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_inner, constantTime_distSpaceDiv, schwartzMap_slice_integral_hasFDerivAt, QuantumMechanics.HydrogenAtom.lrlOperator_eq', QuantumMechanics.HydrogenAtom.lrlOperatorSqr_eq, grad_eq_gradiant, integrable_time_integral, contDiff_grad, basis_repr_inner_eq, QuantumMechanics.SpaceDHilbertSpace.eLpNorm_mk, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, eval_contDiff, QuantumMechanics.position_position_commutation_momentum, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, IsDistBounded.integrable_space_fderiv_mul, time_integral_iteratedFDeriv_apply, translateSchwartz_coe_eq, QuantumMechanics.angularMomentumOperator_antisymm, normPowerSeries_aestronglyMeasurable, lintegral_volume_eq_spherical, Electromagnetism.ElectromagneticPotential.electricField_contDiff, grad_inner_repr_eq, distOfFunction_inner, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, QuantumMechanics.SpaceDHilbertSpace.mem_iff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, distDiv_distConst, QuantumMechanics.momentumOperatorSchwartz_isSymmetric, radialAngularMeasure_eq_volume_withDensity, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, distOfFunction_vector_eval, deriv_eq_mfderiv, distDeriv_apply, QuantumMechanics.radiusPowOperator_apply_memHS, QuantumMechanics.SpaceDHilbertSpace.schwartzEquiv_coe_ae, 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, QuantumMechanics.angularMomentumSqr_commutation_momentumSqr, gradSchwartz_apply_eq_grad, QuantumMechanics.normRegularizedPow_hasTemperateGrowth, HasVarAdjoint.div, integral_radialAngularMeasure, iteratedFDeriv_integrable, QuantumMechanics.positionOperator_apply_fun, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_space, QuantumMechanics.momentumOperator_apply, QuantumMechanics.momentumSqr_comp_angularMomentum_commute, IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.aeEqFun_mk_mem_iff, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, integrable_isDistBounded_inner_grad_schwartzMap, QuantumMechanics.HydrogenAtom.lrlOperator_eq, IsLocalizedFunctionTransform.div_comp_repr, ClassicalMechanics.wave_dx2, distSpaceGrad_apply, gradient_eq_sum, QuantumMechanics.momentumOperator_apply_fun, modelDiffeo_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, IsDistBounded.aestronglyMeasurable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.leibniz_lie, QuantumMechanics.angularMomentumOperator_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, constantTime_distSpaceDeriv, QuantumMechanics.radiusRegPowOperator_comp_eq, deriv_contDiff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, integrableOn_norm_rpow_ball_compl_iff, IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul, QuantumMechanics.SpaceDHilbertSpace.val_eq_coe, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, grad_inner_right, IsTestFunction.of_div, IsDistBounded.isDistBounded_smul_self, inner_basis, integrableOn_norm_rpow_of_compl_nhds, schwartzMap_slice_integral_iteratedFDeriv, distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, QuantumMechanics.position_comp_commute, constantSliceDist_apply, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, QuantumMechanics.SpaceDHilbertSpace.aeStronglyMeasurable_of_memHS, IsDistBounded.inv_pow_smul_self, QuantumMechanics.angularMomentum_commutation_momentumSqr, time_integral_contDiff, Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff_space, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, QuantumMechanics.radiusRegPowOperator_zero, IsLocalizedFunctionTransform.gradient, divergence_eq_space_div, IsDistBounded.inv_pow_smul_repr_self, distSpaceDeriv_commute, QuantumMechanics.momentum_comp_radiusRegPow_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, QuantumMechanics.momentum_comp_commute, QuantumMechanics.SpaceDHilbertSpace.ext_iff, QuantumMechanics.momentumOperatorSqr_eq, QuantumMechanics.angularMomentum_commutation_momentum, distDiv_distTranslate, QuantumMechanics.SpaceDHilbertSpace.schwartzSubmodule_dense, QuantumMechanics.SpaceDHilbertSpace.toBra_apply, Time.deriv_contDiff_of_space, distDeriv_commute, distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, apply_fderiv_eq_distTimeDeriv, distGrad_eq_of_inner, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, distGrad_toFun_eq_distDeriv, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, HasVarAdjDerivAt.grad, 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, volume_metricBall_three_real, QuantumMechanics.SpaceDHilbertSpace.coe_mk_ae, grad_inner, instHasTemperateGrowthRadialAngularMeasure, QuantumMechanics.radiusRegPow_commutation_radiusRegPow, iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, QuantumMechanics.radiusPowOperator_apply_contDiffAt, oneEquiv_measurePreserving, IsDistBounded.aeStronglyMeasurable_inv_pow, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, grad_inner_space, iteratedFDeriv_norm_integrable, QuantumMechanics.SpaceDHilbertSpace.mk_const_smul, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, gradient_dist_normPowerSeries_log_tendsTo, distOfFunction_eculid_eval, QuantumMechanics.HydrogenAtom.angularMomentumSqr_commutation_lrlSqr, ClassicalMechanics.crossProduct_differentiable_of_right_eq_planewave, QuantumMechanics.SpaceDHilbertSpace.mk_eq_iff, HasVarAdjDerivAt.div, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_space_of_smooth, grad_inner_left, constantTime_distSpaceGrad, apply_fderiv_eq_distSpaceDeriv, distCurl_distGrad_eq_zero, lintegral_volume_eq_spherical_mul, 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 | 14 mathmath: integral_volume_eq_spherical, IsDistBounded.zpow_smul_self, lintegral_radialMeasure_eq_spherical_mul, smul_val, SpaceTime.toTimeAndSpace_basis_inl', grad_inner_space_unit_vector, lintegral_volume_eq_spherical, gradient_eq_sum, smul_vadd_zero, IsDistBounded.isDistBounded_smul_self, IsDistBounded.inv_pow_smul_self, smul_apply, grad_inner_space, lintegral_volume_eq_spherical_mul
|
instSeminormedAddCommGroup π | CompOp | 31 mathmath: fderiv_basis_repr_symm, schwartzMap_fderiv_integrable_slice_symm, oneEquiv_measurableEmbedding, oneEquiv_symm_measurePreserving, pow_mul_iteratedFDeriv_norm_le, time_integral_iteratedFDeriv_eq, time_integral_hasFDerivAt, time_integral_iteratedFDeriv_norm_le, integral_one_dim_eq_integral_real, oneEquiv_symm_coe, schwartzMap_slice_bound, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, fderiv_basis_repr, schwartzMap_slice_integral_iteratedFDeriv_norm_le, oneEquiv_coe, schwartzMap_slice_integral_hasFDerivAt, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, iteratedFDeriv_integrable, oneEquiv_symm_apply, dist_eq_norm, oneEquiv_symm_continuous, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, schwartzMap_slice_integral_iteratedFDeriv, oneEquiv_symm_measurableEmbedding, integrable_fderiv_space, iteratedFDeriv_norm_mul_pow_integrable, oneEquiv_measurePreserving, iteratedFDeriv_norm_integrable, time_integral_mul_pow_iteratedFDeriv_norm_le, schwartzMap_iteratedFDeriv_slice_symm_integrable, oneEquiv_continuous
|
instZero π | CompOp | 36 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, radialAngularMeasure_real_closedBall, point_dim_zero_eq, fderiv_basis_repr, integrableOn_norm_rpow_ball_iff, integrableOn_norm_rpow_shell, distDiv_inv_pow_eq_dim, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_eq_electricField, inner_vadd_zero, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, integrableOn_norm_rpow_ball_compl_iff, 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, volume_metricBall_three_real, radialAngularMeasure_closedBall
|
modelDiffeo π | CompOp | 2 mathmath: basis_eq_mfderiv_modelDiffeo_single, modelDiffeo_apply
|
oneEquiv π | CompOp | 10 mathmath: oneEquiv_measurableEmbedding, oneEquiv_symm_measurePreserving, integral_one_dim_eq_integral_real, oneEquiv_symm_coe, oneEquiv_coe, oneEquiv_symm_apply, oneEquiv_symm_continuous, oneEquiv_symm_measurableEmbedding, oneEquiv_measurePreserving, oneEquiv_continuous
|
oneEquivCLE π | CompOp | β |
termπ π | CompOp | β |
toDirection π | CompOp | β |