Documentation Verification Report

DistOfFunction

📁 Source: PhysLean/SpaceAndTime/Space/DistOfFunction.lean

Statistics

Metric	Count
Definitions `distOfFunction`	1
Theorems `distOfFunction_apply`, `distOfFunction_eculid_eval`, `distOfFunction_inner`, `distOfFunction_mul_fun`, `distOfFunction_neg`, `distOfFunction_smul`, `distOfFunction_smul_fun`, `distOfFunction_vector_eval`, `distOfFunction_zero_eq_zero`	9
Total	10

Space

Definitions

Name	Category	Theorems
`distOfFunction` 📖	CompOp	28 math math: `distOfFunction_neg`, `gradient_dist_normPowerSeries_zpow_tendsTo_distGrad_norm`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential`, `distOfFunction_smul`, `distOfFunction_smul_fun`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate`, `distOfFunction_apply`, `gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate`, `distOfFunction_zero_eq_zero`, `gradient_dist_normPowerSeries_log`, `gradient_dist_normPowerSeries_zpow_tendsTo`, `gradient_dist_normPowerSeries_zpow`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential`, `distDiv_inv_pow_eq_dim`, `distTranslate_ofFunction`, `Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField`, `distDiv_ofFunction`, `distGrad_distOfFunction_log_norm`, `distOfFunction_inner`, `distOfFunction_vector_eval`, `distOfFunction_mul_fun`, `distGrad_distOfFunction_norm_zpow`, `Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential`, `gradient_dist_normPowerSeries_log_tendsTo`, `distOfFunction_eculid_eval`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distOfFunction_apply` 📖	mathematical	`IsDistBounded`	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distOfFunction` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace`	—	—
`distOfFunction_eculid_eval` 📖	mathematical	`IsDistBounded`	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distOfFunction` `IsDistBounded.pi_comp`	—	`IsDistBounded.pi_comp` `instFiniteDimensionalReal` `instBorelSpace` `IsDistBounded.integrable_space_mul`
`distOfFunction_inner` 📖	mathematical	`IsDistBounded`	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distOfFunction` `instFiniteDimensionalReal` `instMeasurableSpace` `instBorelSpace`	—	`instFiniteDimensionalReal` `instBorelSpace` `distOfFunction_apply` `IsDistBounded.integrable_space`
`distOfFunction_mul_fun` 📖	mathematical	`IsDistBounded`	`distOfFunction` `IsDistBounded.const_mul_fun` `Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	—	`distOfFunction_smul_fun`
`distOfFunction_neg` 📖	mathematical	`IsDistBounded`	`distOfFunction` `Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `IsDistBounded.neg`	—	`IsDistBounded.neg` `IsDistBounded.const_fun_smul` `distOfFunction.congr_simp` `distOfFunction_smul_fun`
`distOfFunction_smul` 📖	mathematical	`IsDistBounded`	`distOfFunction` `Space` `IsDistBounded.const_smul` `Distribution` `instNormedAddCommGroup` `instInnerProductSpaceReal`	—	`IsDistBounded.const_smul` `instFiniteDimensionalReal` `instBorelSpace` `distOfFunction_apply`
`distOfFunction_smul_fun` 📖	mathematical	`IsDistBounded`	`distOfFunction` `IsDistBounded.const_fun_smul` `Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	—	`IsDistBounded.const_fun_smul` `instFiniteDimensionalReal` `instBorelSpace` `distOfFunction_apply`
`distOfFunction_vector_eval` 📖	mathematical	`IsDistBounded` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup`	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `Lorentz.Vector.isNormedSpace` `distOfFunction` `IsDistBounded.vector_component`	—	`IsDistBounded.vector_component` `instFiniteDimensionalReal` `instBorelSpace` `Lorentz.Vector.basis_inner` `Lorentz.Vector.instFiniteDimensionalReal` `IsDistBounded.integrable_space`
`distOfFunction_zero_eq_zero` 📖	mathematical	—	`distOfFunction` `IsDistBounded.const` `Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	—	`IsDistBounded.const` `instFiniteDimensionalReal` `instBorelSpace`

---

← Back to Index