| Name | Category | Theorems |
|---|
basis 📖 | CompOp | 2 mathmath: basis_apply_eq_one, volume_eq_basis_addHaar
|
instAdd 📖 | CompOp | 4 mathmath: TimeTransMan.toTime_symm_add, TimeTransMan.toTime_symm_add', TimeTransMan.toTime_addTime, add_val
|
instAddCommGroup 📖 | CompOp | 37 mathmath: fderiv_val, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, Space.curl_differentiable_time, ClassicalMechanics.euler_lagrange_varGradient, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_time, ClassicalMechanics.planeWave_differentiable_time, Space.space_deriv_differentiable_time, ClassicalMechanics.planeWave_differentiable, Space.fderiv_time_commute_fderiv_space, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_time, SpaceTime.timeSlice_differentiable, deriv_eq, Electromagnetism.ElectromagneticPotential.electricField_differentiable, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable_time, val_differentiable, deriv_differentiable_of_contDiff, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, ClassicalMechanics.time_differentiable_of_eq_planewave, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.electricField_differentiable_time, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Space.iteratedFDeriv_integrable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, ClassicalMechanics.HarmonicOscillator.kineticEnergy_differentiable, ClassicalMechanics.HarmonicOscillator.energy_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_time, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_time, instFiniteDimensionalReal, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_time, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, ClassicalMechanics.HarmonicOscillator.potentialEnergy_differentiable, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable
|
instAddGroup 📖 | CompOp | — |
instCoeReal 📖 | CompOp | — |
instCoeReal_1 📖 | CompOp | — |
instDecidableEq 📖 | CompOp | — |
instDist 📖 | CompOp | 2 mathmath: dist_eq_real_dist, dist_eq_val
|
instInhabited 📖 | CompOp | — |
instInnerProductSpaceReal 📖 | CompOp | 28 mathmath: Space.continuous_time_integral, Space.time_integral_differentiable, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Space.IsDistBounded.integrable_time_space, ClassicalMechanics.euler_lagrange_varGradient, SpaceTime.toTimeAndSpace_symm_measurePreserving, Space.pow_mul_iteratedFDeriv_norm_le, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_hasFDerivAt, Space.time_integral_iteratedFDeriv_norm_le, basis_apply_eq_one, SpaceTime.spaceTime_integral_eq_time_space_integral, volume_eq_basis_addHaar, Space.integrable_time_integral, Space.time_integral_iteratedFDeriv_apply, ClassicalMechanics.hamiltons_equations_varGradient, Space.iteratedFDeriv_integrable, Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, val_measurePreserving, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae, Space.time_integral_contDiff, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Space.timeIntegralSchwartz_apply, Space.integrable_fderiv_space, Space.iteratedFDeriv_norm_mul_pow_integrable, Space.iteratedFDeriv_norm_integrable, Space.time_integral_mul_pow_iteratedFDeriv_norm_le
|
instInnerReal 📖 | CompOp | 1 mathmath: inner_def
|
instLE 📖 | CompOp | 1 mathmath: le_def
|
instMeasurableSpace 📖 | CompOp | 30 mathmath: Space.continuous_time_integral, Space.time_integral_differentiable, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Space.IsDistBounded.integrable_time_space, ClassicalMechanics.euler_lagrange_varGradient, SpaceTime.toTimeAndSpace_symm_measurePreserving, Space.pow_mul_iteratedFDeriv_norm_le, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_hasFDerivAt, Space.time_integral_iteratedFDeriv_norm_le, SpaceTime.spaceTime_integral_eq_time_space_integral, volume_eq_basis_addHaar, instBorelSpace, Space.integrable_time_integral, Space.time_integral_iteratedFDeriv_apply, ClassicalMechanics.hamiltons_equations_varGradient, Space.iteratedFDeriv_integrable, Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, val_measurableEmbedding, val_measurePreserving, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae, Space.time_integral_contDiff, val_measurable, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Space.timeIntegralSchwartz_apply, Space.integrable_fderiv_space, Space.iteratedFDeriv_norm_mul_pow_integrable, Space.iteratedFDeriv_norm_integrable, Space.time_integral_mul_pow_iteratedFDeriv_norm_le
|
instModuleReal 📖 | CompOp | 87 mathmath: Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, SpaceTime.spaceTime_integrable_iff_space_time_integrable, fderiv_val, rank_eq_one, finRank_eq_one, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, SpaceTime.deriv_sum_inr, Space.curl_differentiable_time, ClassicalMechanics.euler_lagrange_varGradient, SpaceTime.toTimeAndSpace_symm_measurePreserving, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_time, ClassicalMechanics.planeWave_differentiable_time, SpaceTime.spaceTime_integral_eq_time_space_integral, Space.space_deriv_differentiable_time, SpaceTime.deriv_sum_inl, ClassicalMechanics.planeWave_differentiable, Space.fderiv_time_commute_fderiv_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, SpaceTime.timeSlice_differentiable, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, deriv_eq, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_differentiable, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, SpaceTime.time_val_toCoord_symm, SpaceTime.toTimeAndSpace_basis_inr, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable_time, SpaceTime.boost_zero_apply_time_space, SpaceTime.time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, val_differentiable, deriv_differentiable_of_contDiff, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, SpaceTime.toTimeAndSpace_symm_apply_inr, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, ClassicalMechanics.time_differentiable_of_eq_planewave, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, SpaceTime.toTimeAndSpace_symm_apply_inl, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.electricField_differentiable_time, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, ClassicalMechanics.HarmonicOscillator.kineticEnergy_differentiable, ClassicalMechanics.HarmonicOscillator.energy_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_time, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_time, instFiniteDimensionalReal, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_time, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, SpaceTime.toTimeAndSpace_basis_inl, ClassicalMechanics.HarmonicOscillator.potentialEnergy_differentiable, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, 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, Space.time_integral_mul_pow_iteratedFDeriv_norm_le
|
instNatCast 📖 | CompOp | 4 mathmath: natCast_zero, natCast_val, natCast_one, realCast_of_natCast
|
instNeg 📖 | CompOp | 3 mathmath: TimeTransMan.toTime_symm_neg, neg_val, TimeTransMan.toTime_neg
|
instNorm 📖 | CompOp | 3 mathmath: Space.pow_mul_iteratedFDeriv_norm_le, Space.iteratedFDeriv_norm_mul_pow_integrable, Space.time_integral_mul_pow_iteratedFDeriv_norm_le
|
instNormedAddCommGroup 📖 | CompOp | 168 mathmath: 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, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Space.time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, SpaceTime.spaceTime_integrable_iff_space_time_integrable, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, rank_eq_one, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, finRank_eq_one, Space.distSpaceDeriv_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, Space.IsDistBounded.integrable_time_space, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, Electromagnetism.LorentzCurrentDensity.chargeDensity_contDiff, SpaceTime.deriv_sum_inr, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, SpaceTime.toTimeAndSpace_symm_measurePreserving, SpaceTime.space_toTimeAndSpace_symm, Space.distSpaceDeriv_apply', ClassicalMechanics.HarmonicOscillator.contDiff_lagrangian, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Space.pow_mul_iteratedFDeriv_norm_le, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_hasFDerivAt, Space.distTimeDeriv_apply', Space.time_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_time, basis_apply_eq_one, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, SpaceTime.spaceTime_integral_eq_time_space_integral, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, SpaceTime.deriv_sum_inl, ClassicalMechanics.planeWave_differentiable, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, SpaceTime.timeSlice_differentiable, ClassicalMechanics.HarmonicOscillator.hamiltonian_contDiff, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_differentiable, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, SpaceTime.distTimeSlice_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, SpaceTime.time_val_toCoord_symm, SpaceTime.toTimeAndSpace_basis_inr, SpaceTime.boost_zero_apply_time_space, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, volume_eq_basis_addHaar, SpaceTime.time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, SpaceTime.distTimeSlice_distDeriv_inr, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_contDiff, Space.distTimeDeriv_apply_CLM, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, SpaceTime.toTimeAndSpace_symm_apply_inr, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, Space.constantTime_distSpaceDiv, Space.integrable_time_integral, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, Space.time_integral_iteratedFDeriv_apply, Electromagnetism.ElectromagneticPotential.electricField_contDiff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, SpaceTime.toTimeAndSpace_symm_apply_inl, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.LorentzCurrentDensity.currentDensity_ContDiff, SpaceTime.timeSlice_contDiff, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Space.iteratedFDeriv_integrable, Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Space.distSpaceGrad_apply, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, Space.constantTime_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, val_measurePreserving, Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Space.time_integral_contDiff, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, Space.distSpaceDeriv_commute, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, Space.distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, Space.apply_fderiv_eq_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, SpaceTime.distDeriv_inl_distTimeSlice_symm, Space.timeIntegralSchwartz_apply, Space.distTimeDeriv_commute_distSpaceDeriv, Space.constantTime_apply, Space.integrable_fderiv_space, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_time, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, SpaceTime.toTimeAndSpace_basis_inl, ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_contDiff, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, Space.iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, Space.iteratedFDeriv_norm_integrable, Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, SpaceTime.toTimeAndSpace_symm_apply_time_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inl_inr_eq_electricField, Space.constantTime_distSpaceGrad, Space.apply_fderiv_eq_distSpaceDeriv, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_time, Space.distSpaceDeriv_apply_CLM, Space.constantTime_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix, Space.time_integral_mul_pow_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_time_contDiff
|
instNormedSpaceReal 📖 | CompOp | 106 mathmath: Space.constantTime_spaceCurlD, Space.continuous_time_integral, SpaceTime.distTimeSlice_distDeriv_inl, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i, Space.time_integral_differentiable, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Space.distSpaceDeriv_apply, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq, Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, Space.IsDistBounded.integrable_time_space, SpaceTime.distTimeSlice_symm_apply, Electromagnetism.LorentzCurrentDensity.chargeDensity_contDiff, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential, Space.distSpaceDeriv_apply', ClassicalMechanics.HarmonicOscillator.contDiff_lagrangian, Space.pow_mul_iteratedFDeriv_norm_le, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_hasFDerivAt, Space.distTimeDeriv_apply', Space.time_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_time, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential, SpaceTime.distTimeSlice_symm_distTimeDeriv_eq, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv, ClassicalMechanics.HarmonicOscillator.hamiltonian_contDiff, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength, SpaceTime.distTimeSlice_apply, Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff, Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq, volume_eq_basis_addHaar, SpaceTime.distTimeSlice_distDeriv_inr, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_contDiff, Space.distTimeDeriv_apply_CLM, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity, Space.constantTime_distSpaceDiv, Space.integrable_time_integral, Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity, Space.time_integral_iteratedFDeriv_apply, Electromagnetism.ElectromagneticPotential.electricField_contDiff, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd, Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential, Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.LorentzCurrentDensity.currentDensity_ContDiff, SpaceTime.timeSlice_contDiff, Space.iteratedFDeriv_integrable, Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Space.distSpaceGrad_apply, Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff, Space.constantTime_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0, Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Space.time_integral_contDiff, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0, Space.distSpaceDeriv_commute, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd, Space.distTimeDeriv_apply, SpaceTime.distDeriv_inr_distTimeSlice_symm, Space.apply_fderiv_eq_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, SpaceTime.distDeriv_inl_distTimeSlice_symm, Space.timeIntegralSchwartz_apply, Space.distTimeDeriv_commute_distSpaceDeriv, Space.constantTime_apply, Space.integrable_fderiv_space, Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength, Electromagnetism.ElectromagneticPotential.electricField_apply_contDiff_time, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd, ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_contDiff, Space.iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero, Space.iteratedFDeriv_norm_integrable, Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i, Space.constantTime_distSpaceGrad, Space.apply_fderiv_eq_distSpaceDeriv, Electromagnetism.ElectromagneticPotential.scalarPotential_contDiff_time, Space.distSpaceDeriv_apply_CLM, Space.constantTime_distTimeDeriv, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix, Space.time_integral_mul_pow_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_time_contDiff
|
instOfNat 📖 | CompOp | 29 mathmath: eq_zero_iff, fderiv_val, Space.distSpaceDeriv_apply, eq_one_iff, ClassicalMechanics.euler_lagrange_varGradient, Space.distSpaceDeriv_apply', Space.distTimeDeriv_apply', basis_apply_eq_one, ofNat_val, eq_one_smul, deriv_eq, SpaceTime.toTimeAndSpace_basis_inl', natCast_zero, SpaceTime.toTimeAndSpace_basis_inr, zero_val, Space.time_integral_iteratedFDeriv_apply, ClassicalMechanics.HarmonicOscillator.energy_conservation_of_equationOfMotion', ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_position_at_zero, natCast_one, Space.fderiv_cross_commute, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae, Space.distTimeDeriv_apply, Space.apply_fderiv_eq_distTimeDeriv, Space.fderiv_space_eq_fderiv_curry, one_val, Space.apply_fderiv_eq_distSpaceDeriv, TimeTransMan.toTime_zero, ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_at_zero, TimeTransMan.toTime_symm_zero_add
|
instPartialOrder 📖 | CompOp | 1 mathmath: lt_def
|
instSMulReal 📖 | CompOp | 3 mathmath: eq_one_smul, SpaceTime.toTimeAndSpace_basis_inl', smul_real_val
|
instSeminormedAddCommGroup 📖 | CompOp | 104 mathmath: Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic', Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField, SpaceTime.spaceTime_integrable_iff_space_time_integrable, fderiv_val, rank_eq_one, finRank_eq_one, Space.distSpaceDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inl_eq_electricField, Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable, SpaceTime.distTimeSlice_symm_apply, TimeTransMan.toTime_symm_add, SpaceTime.deriv_sum_inr, Space.curl_differentiable_time, ClassicalMechanics.euler_lagrange_varGradient, SpaceTime.toTimeAndSpace_symm_measurePreserving, SpaceTime.space_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential, Space.pow_mul_iteratedFDeriv_norm_le, Space.time_integral_iteratedFDeriv_eq, Space.time_integral_iteratedFDeriv_norm_le, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_time, ClassicalMechanics.planeWave_differentiable_time, TimeTransMan.toTime_val, SpaceTime.spaceTime_integral_eq_time_space_integral, Space.space_deriv_differentiable_time, TimeTransMan.toTime_symm_add', SpaceTime.deriv_sum_inl, TimeTransMan.toTime_symm_sub, TimeTransMan.diff_eq_toTime_sub, ClassicalMechanics.planeWave_differentiable, Space.fderiv_time_commute_fderiv_space, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic, SpaceTime.timeSlice_differentiable, Electromagnetism.ElectromagneticPotential.div_electricField_eq_fieldStrengthMatrix, deriv_eq, Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_differentiable, TimeTransMan.toTime_addTime, TimeTransMan.toTime_symm_neg, SpaceTime.toTimeAndSpace_basis_inl', Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space, SpaceTime.time_val_toCoord_symm, SpaceTime.toTimeAndSpace_basis_inr, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable_time, SpaceTime.boost_zero_apply_time_space, SpaceTime.time_toTimeAndSpace_symm, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic, instBorelSpace, val_differentiable, deriv_differentiable_of_contDiff, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space, SpaceTime.toTimeAndSpace_symm_apply_inr, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable, Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix, ClassicalMechanics.time_differentiable_of_eq_planewave, TimeTransMan.toTime_symm_val, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable, SpaceTime.toTimeAndSpace_symm_apply_inl, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time, Electromagnetism.ElectromagneticPotential.electricField_differentiable_time, Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable, Space.iteratedFDeriv_integrable, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable, ClassicalMechanics.HarmonicOscillator.kineticEnergy_differentiable, ClassicalMechanics.HarmonicOscillator.energy_differentiable, SpaceTime.toTimeAndSpace_symm_fderiv, SpaceTime.toTimeAndSpace_fderiv, Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three, Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_time, Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_time, SpaceTime.spaceTime_integral_eq_space_integral_time_integral, ClassicalMechanics.crossProduct_time_differentiable_of_right_eq_planewave, ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable_time, Electromagnetism.ElectromagneticPotential.electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix, Electromagnetism.ElectromagneticPotential.electricField_apply_differentiable, Space.distTimeDeriv_apply, Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime, SpaceTime.spaceTime_integral_eq_time_integral_space_integral, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq, SpaceTime.toTimeAndSpace_basis_inl, ClassicalMechanics.HarmonicOscillator.potentialEnergy_differentiable, Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic, TimeTransMan.toTime_neg, Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable, Space.iteratedFDeriv_norm_mul_pow_integrable, Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix, Space.iteratedFDeriv_norm_integrable, 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, TimeTransMan.toTime_zero, Space.time_integral_mul_pow_iteratedFDeriv_norm_le, TimeTransMan.toTime_symm_zero_add
|
instSub 📖 | CompOp | 2 mathmath: TimeTransMan.toTime_symm_sub, sub_val
|
toRealCLE 📖 | CompOp | — |
toRealCLM 📖 | CompOp | — |
toRealLIE 📖 | CompOp | — |
val 📖 | CompOp | 54 mathmath: realCast_val, lt_def, dist_eq_real_dist, eq_zero_iff, fderiv_val, Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv, ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv, eq_one_iff, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ, ClassicalMechanics.HarmonicOscillator.InitialConditions.tan_time_eq_of_trajectory_velocity_eq_zero, TimeTransMan.toTime_val, TimeTransMan.diff_eq_toTime_sub, ofNat_val, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ', eq_one_smul, dist_eq_val, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ, Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ, SpaceTime.time_val_toCoord_symm, SpaceTime.boost_zero_apply_time_space, natCast_val, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv, val_differentiable, ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity, Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_magneticFunction, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_succ_zero, val_injective, ClassicalMechanics.planeWave_eq, TimeTransMan.toTime_symm_val, zero_val, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_electricFunction, ext_iff, SpaceTime.toTimeAndSpace_symm_apply_inl, le_def, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_succ_succ, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv, neg_val, smul_real_val, Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv, ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_eq, val_measurableEmbedding, val_measurePreserving, sub_val, Electromagnetism.ElectromagneticPotential.harmonicWaveX_vectorPotential_succ_space_deriv_zero, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_zero, inner_def, val_measurable, one_val, ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_acceleration, Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_apply_x_boost_zero_succ, Electromagnetism.ElectromagneticPotential.harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero, add_val, Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost_succ
|