ConstantTimeDist

📁 Source: PhysLean/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean

Statistics

Metric	Count
Definitions constantTime, timeIntegralSchwartz	2
Theorems constantTime_apply, constantTime_distSpaceDeriv, constantTime_distSpaceDiv, constantTime_distSpaceGrad, constantTime_distTimeDeriv, constantTime_spaceCurlD, continuous_time_integral, integrable_fderiv_space, integrable_time_integral, iteratedFDeriv_integrable, iteratedFDeriv_norm_integrable, iteratedFDeriv_norm_mul_pow_integrable, pow_mul_iteratedFDeriv_norm_le, timeIntegralSchwartz_apply, time_integral_contDiff, time_integral_differentiable, time_integral_hasFDerivAt, time_integral_iteratedFDeriv_apply, time_integral_iteratedFDeriv_eq, time_integral_iteratedFDeriv_norm_le, time_integral_mul_pow_iteratedFDeriv_norm_le	21
Total	23

Space

Definitions

Name	Category	Theorems
constantTime 📖	CompOp	21 math math: constantTime_spaceCurlD, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_scalarPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_div_electricField, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential_fst, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.wireCurrentDensity_currentDensity_fst, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_electricField, Electromagnetism.DistElectromagneticPotential.infiniteWire_vectorPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticle_electricField, constantTime_distSpaceDiv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_chargeDensity, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_scalarPotential, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_eq_distTranslate, constantTime_distSpaceDeriv, Electromagnetism.DistElectromagneticPotential.threeDimPointParticleCurrentDensity_eq_distTranslate, Electromagnetism.DistElectromagneticPotential.threeDimPointParticle_div_electricField, constantTime_apply, Electromagnetism.DistElectromagneticPotential.oneDimPointParticleCurrentDensity_chargeDensity, constantTime_distSpaceGrad, constantTime_distTimeDeriv
timeIntegralSchwartz 📖	CompOp	2 math math: timeIntegralSchwartz_apply, constantTime_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constantTime_apply 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal constantTime timeIntegralSchwartz	—	—
constantTime_distSpaceDeriv 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal distSpaceDeriv constantTime distDeriv	—	constantTime_apply instFiniteDimensionalReal distDeriv_apply Time.instFiniteDimensionalReal distSpaceDeriv_apply Distribution.fderivD_apply Time.instBorelSpace timeIntegralSchwartz_apply time_integral_hasFDerivAt integrable_fderiv_space
constantTime_distSpaceDiv 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal distSpaceDiv constantTime distDiv	—	constantTime_apply distSpaceDiv_apply_eq_sum_distSpaceDeriv distDiv_apply_eq_sum_distDeriv constantTime_distSpaceDeriv
constantTime_distSpaceGrad 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal distSpaceGrad constantTime distGrad	—	constantTime_apply distSpaceGrad_apply distGrad_apply constantTime_distSpaceDeriv
constantTime_distTimeDeriv 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal distTimeDeriv constantTime	—	Time.instFiniteDimensionalReal instFiniteDimensionalReal distTimeDeriv_apply Distribution.fderivD_apply constantTime_apply Time.instBorelSpace timeIntegralSchwartz_apply integrable_time_integral
constantTime_spaceCurlD 📖	mathematical	—	Distribution Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal distSpaceCurl constantTime distCurl	—	constantTime_apply constantTime_distSpaceDeriv
continuous_time_integral 📖	mathematical	—	Space instSeminormedAddCommGroup Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace
integrable_fderiv_space 📖	mathematical	—	Space instSeminormedAddCommGroup instAddCommGroup instModuleReal instInnerProductSpaceReal Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace instNormedAddCommGroup Time.instNormedSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace instSubsingletonOfNatNat zero_apply basis_apply instFiniteDimensionalReal
integrable_time_integral 📖	mathematical	—	Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace instBorelSpace instFiniteDimensionalReal
iteratedFDeriv_integrable 📖	mathematical	—	Time Space Time.instNormedAddCommGroup instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal Time.instAddCommGroup instAddCommGroup Time.instSeminormedAddCommGroup instSeminormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace	—	Time.instFiniteDimensionalReal Time.instBorelSpace iteratedFDeriv_norm_integrable
iteratedFDeriv_norm_integrable 📖	mathematical	—	Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal Time.instSeminormedAddCommGroup instSeminormedAddCommGroup	—	Time.instFiniteDimensionalReal Time.instBorelSpace iteratedFDeriv_norm_mul_pow_integrable
iteratedFDeriv_norm_mul_pow_integrable 📖	mathematical	—	Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Space Time.instNorm instNorm instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal Time.instSeminormedAddCommGroup instSeminormedAddCommGroup	—	Time.instFiniteDimensionalReal Time.instBorelSpace pow_mul_iteratedFDeriv_norm_le
pow_mul_iteratedFDeriv_norm_le 📖	mathematical	—	Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instNorm Space instNorm instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal Time.instSeminormedAddCommGroup instSeminormedAddCommGroup	—	Time.instFiniteDimensionalReal Time.instBorelSpace
timeIntegralSchwartz_apply 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal Time Time.instNormedAddCommGroup Time.instNormedSpaceReal timeIntegralSchwartz Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace	—	—
time_integral_contDiff 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instNormedSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace continuous_time_integral instFiniteDimensionalReal integrable_fderiv_space time_integral_hasFDerivAt
time_integral_differentiable 📖	mathematical	—	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace time_integral_hasFDerivAt
time_integral_hasFDerivAt 📖	mathematical	—	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace instNormedAddCommGroup Time.instNormedSpaceReal instInnerProductSpaceReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace instFiniteDimensionalReal instBorelSpace IsDistBounded.instHasTemperateGrowthProdProdOfOpensMeasurableSpace zero_apply basis_apply
time_integral_iteratedFDeriv_apply 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instNormedSpaceReal Time.instOfNat	—	Time.instFiniteDimensionalReal Time.instBorelSpace time_integral_contDiff time_integral_hasFDerivAt integrable_fderiv_space
time_integral_iteratedFDeriv_eq 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instNormedSpaceReal instAddCommMonoid instModuleReal instSeminormedAddCommGroup Time.instSeminormedAddCommGroup Time.instModuleReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace time_integral_iteratedFDeriv_apply iteratedFDeriv_integrable
time_integral_iteratedFDeriv_norm_le 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal instSeminormedAddCommGroup Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instNormedSpaceReal Time.instSeminormedAddCommGroup instAddCommMonoid instModuleReal Time.instModuleReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace time_integral_iteratedFDeriv_eq
time_integral_mul_pow_iteratedFDeriv_norm_le 📖	mathematical	—	Time Time.instNormedAddCommGroup Time.instInnerProductSpaceReal Time.instFiniteDimensionalReal Time.instMeasurableSpace Time.instBorelSpace Time.instNorm Space instNorm instNormedAddCommGroup instInnerProductSpaceReal instSeminormedAddCommGroup Time.instNormedSpaceReal instAddCommMonoid Time.instSeminormedAddCommGroup instModuleReal Time.instModuleReal	—	Time.instFiniteDimensionalReal Time.instBorelSpace pow_mul_iteratedFDeriv_norm_le time_integral_iteratedFDeriv_norm_le iteratedFDeriv_norm_integrable iteratedFDeriv_norm_mul_pow_integrable

---

← Back to Index