Research proof index

Curl and time derivative commute.

Derivatives on spacetime commute with one another (Clairaut's theorem).

Derivatives on spacetime commute with one another (Clairaut's theorem). -/ lemma deriv_commute {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) (hf : ContDiff ℝ 2 f) : ∂_ μ (∂_ ν f) = ∂_ ν (∂_ μ f) := by ext x show fderiv ℝ (fun y => fderiv ℝ f y (Lorentz.Vector.basis ν)) x (Lorentz.Vector.basis μ) =...

Derivatives on spacetime commute with one another (Clairaut's theorem). -/ lemma deriv_commute {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) (hf : ContDiff ℝ 2 f) : ∂_ μ (∂_ ν f) = ∂_ ν (∂_ μ f) := by ext x show fderiv ℝ (fun y => fderiv ℝ f y (Lorentz.Vector.basis ν)) x (Lorentz.Vector.basis μ) =...

The equivalence on of SpaceTime taking (1, 0, 0, ...) to of (c, 0, 0, ....) and keeping all other components the same. -/ def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) : SpaceTime d ≃L[ℝ] SpaceTime d where toFun x := fun μ => match μ with | Sum.inl 0 => c.val * x (Sum.inl 0) | Sum.inr i => x (Sum.inr i) invFun x := fun μ => match μ with | Sum.i...

Given a distribution (function) f : Space d →d[ℝ] M the derivative of f in direction μ. -/ noncomputable def distDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin 1 ⊕ Fin d) : ((SpaceTime d) →d[ℝ] M) →ₗ[ℝ] (SpaceTime d) →d[ℝ] M where toFun f := let ev : (SpaceTime d →L[ℝ] M) →L[ℝ] M := { toFun v := v (Lorentz.Vector.basis μ) map_add' v1...