Documentation Verification Report

Basic

📁 Source: PhysLean/Mathematics/Distribution/Basic.lean

Statistics

Metric	Count
Definitions `Distribution`, `const`, `diracDelta`, `diracDelta'`, `fderivD`, `fourierTransform`, `heavisideStep`, `ofLinear`, `«term_→d[_]_»`	9
Theorems `const_apply`, `diracDelta'_apply`, `diracDelta_apply`, `fderivD_apply`, `fderivD_const`, `fourierTransform_apply`, `heavisideStep_apply`, `ofLinear_apply`	8
Total	17

Distribution

Definitions

Name	Category	Theorems
`const` 📖	CompOp	2 math math: `const_apply`, `fderivD_const`
`diracDelta` 📖	CompOp	7 math math: `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst`, `Space.distDiv_inv_pow_eq_dim`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField`, `diracDelta_apply`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity`
`diracDelta'` 📖	CompOp	3 math math: `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate`, `diracDelta'_apply`
`fderivD` 📖	CompOp	8 math math: `Space.distSpaceDeriv_apply`, `Space.distGrad_inner_eq`, `SpaceTime.distDeriv_apply`, `Space.distDiv_apply_eq_sum_fderivD`, `Space.distDeriv_apply`, `Space.distTimeDeriv_apply`, `fderivD_apply`, `fderivD_const`
`fourierTransform` 📖	CompOp	1 math math: `fourierTransform_apply`
`heavisideStep` 📖	CompOp	1 math math: `heavisideStep_apply`
`ofLinear` 📖	CompOp	1 math math: `ofLinear_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_apply` 📖	mathematical	—	`Distribution` `const`	—	—
`diracDelta'_apply` 📖	mathematical	—	`Distribution` `diracDelta'`	—	—
`diracDelta_apply` 📖	mathematical	—	`Distribution` `diracDelta`	—	—
`fderivD_apply` 📖	mathematical	—	`Distribution` `fderivD`	—	—
`fderivD_const` 📖	mathematical	—	`Distribution` `fderivD` `const`	—	`fderivD_apply` `const_apply`
`fourierTransform_apply` 📖	mathematical	—	`Distribution` `fourierTransform`	—	—
`heavisideStep_apply` 📖	mathematical	—	`Distribution` `heavisideStep`	—	—
`ofLinear_apply` 📖	mathematical	—	`Distribution` `ofLinear`	—	—

(root)

Definitions

Name	Category	Theorems
`Distribution` 📖	CompOp	158 math math: `Space.distOfFunction_neg`, `Space.constantTime_spaceCurlD`, `SpaceTime.distTimeSlice_distDeriv_inl`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_gradLagrangian`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_antisymmetric_basis`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inr_i`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_thrd`, `Space.gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField`, `Space.distOfFunction_smul`, `Space.distSpaceDeriv_apply`, `Space.distOfFunction_smul_fun`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inl_eq`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_electricField`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate`, `SpaceTime.distDeriv_apply'`, `SpaceTime.distTimeSlice_symm_apply`, `SpaceTime.distTensorDeriv_toTensor_basis_repr`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_vectorPotential`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum`, `Space.distCurl_distConst`, `Electromagnetism.DistElectromagneticPotential.distDeriv_fieldStrength_diag_zero`, `Space.distCurl_apply_two`, `Space.distSpaceDeriv_apply'`, `Space.distTimeDeriv_apply'`, `Space.distOfFunction_apply`, `Space.distTranslate_apply`, `Space.distCurl_apply`, `Space.gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm`, `Space.distDeriv_distConst`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_space_time`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential`, `SpaceTime.distDeriv_comp_lorentz_action`, `Electromagnetism.DistElectromagneticPotential.deriv_eq_sum_sum`, `SpaceTime.distTimeSlice_symm_distTimeDeriv_eq`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_currentDensity`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv`, `Distribution.heavisideStep_apply`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate`, `Space.distCurl_apply_one`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst`, `Space.distGrad_inner_eq`, `Electromagnetism.DistElectromagneticPotential.isExterma_iff_tensor`, `Space.distOfFunction_zero_eq_zero`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_vectorPotential`, `Space.distGrad_distConst`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField_timeDeriv`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_fieldStrength`, `Space.gradient_dist_normPowerSeries_log`, `Space.gradient_dist_normPowerSeries_zpow_tendsTo`, `SpaceTime.distDeriv_commute`, `SpaceTime.distTensorDeriv_equivariant`, `SpaceTime.distTimeSlice_apply`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_add`, `Space.distGrad_apply`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single`, `Electromagnetism.DistElectromagneticPotential.toTensor_deriv_basis_repr_apply`, `Space.gradient_dist_normPowerSeries_zpow`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_sum_inr_eq`, `Space.distDeriv_constantSliceDist_same`, `Distribution.const_apply`, `SpaceTime.distTimeSlice_distDeriv_inr`, `Space.distCurl_apply_zero`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField`, `SpaceTime.instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution`, `Space.distTimeDeriv_apply_CLM`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential`, `Space.distDeriv_constantSliceDist_succAbove`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distTimeDeriv`, `Space.distDiv_inv_pow_eq_dim`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_basis_repr_eq_vector_potential`, `Space.distTranslate_ofFunction`, `Space.distTranslate_distGrad`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField`, `SpaceTime.distDeriv_apply`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_magneticFieldMatrix`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_currentDensity`, `Space.distDiv_apply_eq_sum_fderivD`, `SpaceTime.apply_fderiv_eq_distDeriv`, `Space.distDiv_ofFunction`, `Distribution.ofLinear_apply`, `Space.distGrad_distOfFunction_log_norm`, `Space.constantTime_distSpaceDiv`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_chargeDesnity`, `Space.distOfFunction_inner`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_snd`, `Space.distDiv_distConst`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential`, `Space.distOfFunction_vector_eval`, `Space.distDeriv_apply`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_fieldStrengthAux`, `Space.distOfFunction_mul_fun`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_sum_inl_0`, `Space.distGrad_distOfFunction_norm_zpow`, `Distribution.fourierTransform_apply`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux`, `Electromagnetism.DistElectromagneticPotential.deriv_basis_repr_apply`, `Space.distGrad_eq_sum_basis`, `Space.distDiv_apply_eq_sum_distDeriv`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential`, `Space.distSpaceGrad_apply`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_scalarPotential`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate`, `Space.constantTime_distSpaceDeriv`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_distSpaceDeriv_0`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_diag_zero`, `Space.distSpaceDiv_apply_eq_sum_distSpaceDeriv`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate`, `Space.constantSliceDist_apply`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inl_0`, `Space.distSpaceDeriv_commute`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_snd`, `Space.distDiv_distTranslate`, `Space.distDeriv_commute`, `Space.distTimeDeriv_apply`, `SpaceTime.distDeriv_inr_distTimeSlice_symm`, `Electromagnetism.DistElectromagneticPotential.deriv_equivariant`, `Distribution.fderivD_apply`, `Space.apply_fderiv_eq_distTimeDeriv`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField`, `Space.distGrad_toFun_eq_distDeriv`, `SpaceTime.distDeriv_inl_distTimeSlice_symm`, `Space.distTimeDeriv_commute_distSpaceDeriv`, `Space.constantTime_apply`, `Electromagnetism.DistElectromagneticPotential.electricField_eq_fieldStrength`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_equivariant`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_thrd`, `Distribution.diracDelta'_apply`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis`, `SpaceTime.lorentzGroup_smul_dist_apply`, `Distribution.diracDelta_apply`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField_timeDeriv`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity`, `Electromagnetism.DistElectromagneticPotential.magneticFieldMatrix_one_dim_eq_zero`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_sum_inr_i`, `Space.gradient_dist_normPowerSeries_log_tendsTo`, `Space.distOfFunction_eculid_eval`, `Electromagnetism.DistElectromagneticPotential.isExtrema_iff_components`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength`, `Space.constantTime_distSpaceGrad`, `Space.apply_fderiv_eq_distSpaceDeriv`, `Space.distCurl_distGrad_eq_zero`, `Distribution.fderivD_const`, `Space.distSpaceDeriv_apply_CLM`, `Space.constantTime_distTimeDeriv`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_magneticFieldMatrix`, `SpaceTime.distTensorDeriv_apply`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr`
`«term_→d[_]_»` 📖	CompOp	—

---

← Back to Index