Documentation Verification Report

ConstantSliceDist

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

Statistics

Metric	Count
Definitions `constantSliceDist`, `sliceSchwartz`	2
Theorems `constantSliceDist_apply`, `continuous_schwartzMap_slice_integral`, `distDeriv_constantSliceDist_same`, `distDeriv_constantSliceDist_succAbove`, `schwartzMap_fderiv_integrable_slice_symm`, `schwartzMap_fderiv_left_integrable_slice_symm`, `schwartzMap_integrable_slice_symm`, `schwartzMap_iteratedFDeriv_norm_slice_symm_integrable`, `schwartzMap_iteratedFDeriv_slice_symm_integrable`, `schwartzMap_mul_iteratedFDeriv_integrable_slice_symm`, `schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le`, `schwartzMap_slice_bound`, `schwartzMap_slice_integral_contDiff`, `schwartzMap_slice_integral_differentiable`, `schwartzMap_slice_integral_hasFDerivAt`, `schwartzMap_slice_integral_iteratedFDeriv`, `schwartzMap_slice_integral_iteratedFDeriv_apply`, `schwartzMap_slice_integral_iteratedFDeriv_norm_le`, `sliceSchwartz_apply`	19
Total	21

Space

Definitions

Name	Category	Theorems
`constantSliceDist` 📖	CompOp	6 math math: `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst`, `Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst`, `distDeriv_constantSliceDist_same`, `Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential`, `distDeriv_constantSliceDist_succAbove`, `constantSliceDist_apply`
`sliceSchwartz` 📖	CompOp	2 math math: `constantSliceDist_apply`, `sliceSchwartz_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constantSliceDist_apply` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `constantSliceDist` `sliceSchwartz`	—	—
`continuous_schwartzMap_slice_integral` 📖	mathematical	—	`Space` `instSeminormedAddCommGroup` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_slice_bound`
`distDeriv_constantSliceDist_same` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distDeriv` `constantSliceDist`	—	`instFiniteDimensionalReal` `distDeriv_apply` `Distribution.fderivD_apply` `constantSliceDist_apply` `sliceSchwartz_apply` `basis_self_eq_slice` `fderiv_fun_slice_symm_left_apply` `schwartzMap_fderiv_left_integrable_slice_symm` `schwartzMap_integrable_slice_symm`
`distDeriv_constantSliceDist_succAbove` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distDeriv` `constantSliceDist`	—	`instFiniteDimensionalReal` `distDeriv_apply` `Distribution.fderivD_apply` `constantSliceDist_apply` `sliceSchwartz_apply` `schwartzMap_slice_integral_hasFDerivAt` `schwartzMap_fderiv_integrable_slice_symm` `basis_succAbove_eq_slice` `fderiv_fun_slice_symm_right_apply`
`schwartzMap_fderiv_integrable_slice_symm` 📖	mathematical	—	`Space` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal` `instInnerProductSpaceReal` `instNormedAddCommGroup` `instAddCommMonoid` `slice`	—	`schwartzMap_mul_iteratedFDeriv_integrable_slice_symm` `instFiniteDimensionalReal` `fderiv_slice_symm`
`schwartzMap_fderiv_left_integrable_slice_symm` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`fderiv_slice_symm_left_apply` `schwartzMap_integrable_slice_symm`
`schwartzMap_integrable_slice_symm` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_mul_iteratedFDeriv_integrable_slice_symm`
`schwartzMap_iteratedFDeriv_norm_slice_symm_integrable` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_mul_iteratedFDeriv_integrable_slice_symm`
`schwartzMap_iteratedFDeriv_slice_symm_integrable` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instAddCommGroup` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_iteratedFDeriv_norm_slice_symm_integrable`
`schwartzMap_mul_iteratedFDeriv_integrable_slice_symm` 📖	mathematical	—	`Space` `instNorm` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice` `instNormedAddCommGroup` `instInnerProductSpaceReal`	—	`schwartzMap_slice_bound`
`schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le` 📖	mathematical	—	`Space` `instNorm` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_slice_bound` `schwartzMap_slice_integral_iteratedFDeriv_norm_le` `schwartzMap_iteratedFDeriv_norm_slice_symm_integrable` `schwartzMap_mul_iteratedFDeriv_integrable_slice_symm`
`schwartzMap_slice_bound` 📖	mathematical	—	`Space` `instNorm` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice` `instNormedAddCommGroup` `instInnerProductSpaceReal`	—	`abs_right_le_norm_slice_symm`
`schwartzMap_slice_integral_contDiff` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`continuous_schwartzMap_slice_integral` `instFiniteDimensionalReal` `schwartzMap_fderiv_integrable_slice_symm` `fderiv_slice_symm_right_apply` `schwartzMap_slice_integral_hasFDerivAt`
`schwartzMap_slice_integral_differentiable` 📖	mathematical	—	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instAddCommMonoid` `slice`	—	`schwartzMap_slice_integral_hasFDerivAt`
`schwartzMap_slice_integral_hasFDerivAt` 📖	mathematical	—	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instAddCommMonoid` `slice`	—	`schwartzMap_slice_bound` `schwartzMap_integrable_slice_symm` `instFiniteDimensionalReal` `fderiv_slice_symm`
`schwartzMap_slice_integral_iteratedFDeriv` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_slice_integral_iteratedFDeriv_apply` `schwartzMap_iteratedFDeriv_slice_symm_integrable`
`schwartzMap_slice_integral_iteratedFDeriv_apply` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_slice_integral_contDiff` `schwartzMap_slice_integral_hasFDerivAt` `schwartzMap_fderiv_integrable_slice_symm` `fderiv_fun_slice_symm_right_apply`
`schwartzMap_slice_integral_iteratedFDeriv_norm_le` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	`schwartzMap_slice_integral_iteratedFDeriv`
`sliceSchwartz_apply` 📖	mathematical	—	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `sliceSchwartz` `instSeminormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `slice`	—	—

---

← Back to Index