Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

591 results

Clear filters
Project-declaredLean 4.32.0

Return time

ClassicalMechanics.HarmonicOscillator.return_time

Plain-language statement

Assuming that the initial coordinate and velocity are not simultaneously zero, the time stamps when the harmonic oscillator returns to its initial coordinate and velocity is a multiple of its period

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Mdifferentiable At iff differentiable At coord

ClassicalMechanics.HarmonicOscillator.Trajectory.mdifferentiableAt_iff_differentiableAt_coord

Plain-language statement

A trajectory is MDifferentiableAt a time iff its coordinate curve is ordinarily differentiable there, since the two differ by the coordinate diffeomorphism.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Is Total Time Derivative explicit

ClassicalMechanics.Lagrangian.isTotalTimeDerivative_explicit

Plain-language statement

Explicit reformulation (by the chain rule): δL(t, q, dₜ q) = ∂F/∂t(t, q) + ⟨∇ᵣF(t, q), dₜ q⟩ or δL(t, q, dₜ q) = fderiv ℝ F (t, q) (1, dₜ q)

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Is Total Time Derivative Velocity

ClassicalMechanics.Lagrangian.isTotalTimeDerivativeVelocity

Plain-language statement

A velocity-only function that is a total time derivative must be linear in velocity. If δL depends only on velocity and equals d/dt F(t, q) for some F, then δL(dₜ q) = ⟨g, dₜ q⟩ for some constant vector g. This characterization comes from the requirement that: - d/dt F(t, q) = ∂F/∂t + ⟨∇F, dₜ q⟩ = ∂F/∂t + ⟨∇F, dₜ q⟩ - For the result to be independent of q...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Total Time Derivative cont Diff

ClassicalMechanics.Lagrangian.totalTimeDerivative_contDiff

Plain-language statement

If δL is a total time derivative (of a smooth function), then it is smooth

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Total Time Derivative euler Lagrange equivalenvce

ClassicalMechanics.Lagrangian.totalTimeDerivative_eulerLagrange_equivalenvce

Plain-language statement

Corollary: If L and L' differ by a total time derivative, then the corresponding Euler-Lagrange operators coincide

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record