Research proof index

The derivative of tanh(x) is 1 - tanh(x)^2

toISQHom is injective: PhysLib dimensions include faithfully into ISQ.

The creation of an electromagnetic potential from a static vector potential. -/ noncomputable def ofStaticVectorPotential {d} (c : SpeedOfLight) : ((Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) →ₗ[ℝ] DistElectromagneticPotential d := ofVectorPotential c ∘ₗ Space.constantTime TODO "Add a constructor for DistElectromagneticPotential from electric and magnetic f...

The variational gradient of the free current potential for distributional potentials. -/ noncomputable def gradFreeCurrentPotential {d} : DistLorentzCurrentDensity d →ₗ[ℝ] ((SpaceTime d) →d[ℝ] Lorentz.Vector d) where toFun J := { toFun ε := ∑ μ, (η μ μ • (J ε μ) • Lorentz.Vector.basis μ) map_add' ε₁ ε₂ := by simp [Finset.sum_add_distrib, add_smul] map_smu...

The electromagnetic potential of an infinite wire along the x-axis carrying a current I. -/ noncomputable def infiniteWire (𝓕 : FreeSpace) (I : ℝ) : DistElectromagneticPotential 3 := (SpaceTime.distTimeSlice 𝓕.c).symm <| constantTime <| constantSliceDist 0 ((- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) => Real.log ‖x‖ • Lorentz.Vec...

The proposition on an electromagnetic potential, corresponding to the statement that it is an extrema of the lagrangian. -/ def IsExtrema {d} (𝓕 : FreeSpace) (A : DistElectromagneticPotential d) (J : DistLorentzCurrentDensity d) : Prop := A.gradLagrangian 𝓕 J = 0 lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : DistElectromagneticPotential d) (J...