Research proof index

Total time derivative has a variational derivative, which is zero

If two lagrangians, L and L', differ by a total time derivative, and L has a variational derivative grad, then so does L'. -/ lemma totalTimeDerivative_hasVarGradientAt_equivalence [CompleteSpace X] (L δL : Time → X → X → ℝ) (hδL : IsTotalTimeDerivative δL) (q : Time → X) (hq : ContDiff ℝ ∞ q) (grad : Time → X) (hgrad : HasVarGradientAt (fun q' t => L t (...

A vector-valued plane wave travelling in the direction of s with propagation speed c. -/ noncomputable def planeWave (f₀ : ℝ → EuclideanSpace ℝ (Fin d)) (c : ℝ) (s : Direction d) : Time → Space d → EuclideanSpace ℝ (Fin d) := fun t x => f₀ (⟪x, s.unit⟫ℝ - c * t) lemma planeWave_eq {d f₀ c x} {s : Direction d} : planeWave f₀ c s t x = f₀ (⟪x, s.unit⟫...

If f₀ is a function of (inner ℝ x s - c * t), the fderiv of its components with respect to spatial coordinates is equal to the corresponding component of the propagation direction s times time derivative.

The transverse harmonic planewave representation is equivalent to the general planewave expression with ‖k‖ = ω/c.

The energy eigenstates of the tight binding chain are orthogonal. This is a fundamental quantum mechanical result: eigenstates of a Hermitian operator (the Hamiltonian) with distinct eigenvalues are orthogonal. Here we prove it directly using the periodic boundary conditions which quantize the wavenumbers. The key physical insight is that different wavenu...