Documentation Verification Report

Derivatives

📁 Source: PhysLean/SpaceAndTime/Time/Derivatives.lean

Statistics

Metric	Count
Definitions `deriv`, `«term∂ₜ»`	2
Theorems `deriv_const`, `deriv_contDiff_of_contDiff`, `deriv_differentiable_of_contDiff`, `deriv_eq`, `deriv_euclid`, `deriv_lorentzVector`, `deriv_neg`, `deriv_smul`, `differentiable_euclid`, `fderiv_euclid`	10
Total	12

Time

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	60 math math: `Space.time_deriv_curl_commute`, `ClassicalMechanics.HarmonicOscillator.hamiltonian_eq_energy`, `Electromagnetism.ElectromagneticPotential.harmonicWaveX_electricField_succ_time_deriv`, `ClassicalMechanics.space_fderiv_of_inner_product_wave_eq_space_fderiv`, `ClassicalMechanics.hamiltonEqOp_eq`, `Space.time_deriv_cross_commute`, `Space.time_deriv_comm_space_deriv`, `Electromagnetism.ElectromagneticPotential.time_deriv_magneticFieldMatrix`, `ClassicalMechanics.HarmonicOscillator.kineticEnergy_eq`, `Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential_time_deriv`, `deriv_lorentzVector`, `Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_time_deriv`, `ClassicalMechanics.hamiltonEqOp_eq_zero_iff_hamiltons_equations`, `ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_hamiltonEqOp_eq_zero`, `deriv_const`, `Electromagnetism.ElectromagneticPotential.electricField_eq`, `SpaceTime.deriv_sum_inl`, `Space.time_deriv_differentiable_space`, `Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic`, `deriv_eq`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv`, `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_at_arctan`, `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_eq_zero_iff`, `ClassicalMechanics.eulerLagrangeOp_eq`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix`, `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema`, `deriv_differentiable_of_contDiff`, `deriv_neg`, `ClassicalMechanics.HarmonicOscillator.gradLagrangian_eq_force`, `deriv_smul`, `ClassicalMechanics.hamiltons_equations_varGradient`, `Electromagnetism.ElectromagneticPotential.time_deriv_comp_vectorPotential_eq_electricField`, `ClassicalMechanics.HarmonicOscillator.equationOfMotion_iff_newtons_2nd_law`, `ClassicalMechanics.HarmonicOscillator.potentialEnergy_deriv`, `Electromagnetism.ElectromagneticPotential.time_deriv_vectorPotential_eq_electricField`, `deriv_contDiff_of_contDiff`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three`, `deriv_euclid`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_time_deriv`, `ClassicalMechanics.HarmonicOscillator.kineticEnergy_deriv`, `ClassicalMechanics.HarmonicOscillator.energy_deriv`, `ClassicalMechanics.HarmonicOscillator.equationOfMotion_tfae`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_eq_fieldStrengthMatrix`, `ClassicalMechanics.HarmonicOscillator.lagrangian_eq_kineticEnergy_sub_potentialEnergy`, `Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema`, `ClassicalMechanics.HarmonicOscillator.InitialConditionsAtTime.toInitialConditions_velocity_at_t₀`, `ClassicalMechanics.planeWave_time_deriv`, `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_acceleration`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv`, `Electromagnetism.ElectromagneticPotential.IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `ClassicalMechanics.planeWave_time_deriv_time_deriv`, `Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `ClassicalMechanics.HarmonicOscillator.InitialConditions.trajectory_velocity_at_zero`, `Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema`, `ClassicalMechanics.HarmonicOscillator.energy_conservation_of_equationOfMotion`
`«term∂ₜ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deriv_const` 📖	mathematical	—	`deriv`	—	`deriv.eq_1`
`deriv_contDiff_of_contDiff` 📖	mathematical	`Time` `instNormedAddCommGroup` `instNormedSpaceReal`	`deriv`	—	—
`deriv_differentiable_of_contDiff` 📖	mathematical	`Time` `instNormedAddCommGroup` `instNormedSpaceReal`	`instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `deriv`	—	—
`deriv_eq` 📖	mathematical	—	`deriv` `Time` `instSeminormedAddCommGroup` `instAddCommGroup` `instModuleReal` `instOfNat`	—	—
`deriv_euclid` 📖	mathematical	`Time` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	`deriv`	—	`deriv_eq`
`deriv_lorentzVector` 📖	mathematical	`Time` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup` `Lorentz.Vector` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup`	`deriv`	—	`deriv_eq`
`deriv_neg` 📖	mathematical	—	`deriv` `Time`	—	`deriv.eq_1`
`deriv_smul` 📖	mathematical	`Time` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	`deriv`	—	`deriv.eq_1`
`differentiable_euclid` 📖	—	`Time` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	—	—	—
`fderiv_euclid` 📖	—	`Time` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	—	—	—

---

← Back to Index