The field strength tensor

@[reducible, inline]

noncomputable abbrev Electromagnetism.FieldStrength (d : ℕ := 3) : Submodule ℝ (SpaceTime d → (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up, realLorentzTensor.Color.up])

The Field strength is a tensor F^μ^ν which is anti-symmetric..

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.mem_of_repr {d : ℕ} {F : (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]} (h : ∀ (i : Fin ((realLorentzTensor d).repDim (![realLorentzTensor.Color.up, realLorentzTensor.Color.up] 0))) (j : Fin ((realLorentzTensor d).repDim (![realLorentzTensor.Color.up, realLorentzTensor.Color.up] 1))), (((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr F) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => j) = -((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr F) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => j | 1 => i) : F = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-F)

theorem Electromagnetism.FieldStrength.repr_symm {d : ℕ} (F : ↥(FieldStrength d)) (i j : Fin (1 + d)) (x : (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up]) : (((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => j) = -((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => j | 1 => i

@[simp]

theorem Electromagnetism.FieldStrength.repr_diag_zero {d : ℕ} (F : ↥(FieldStrength d)) (i : Fin (1 + d)) (x : (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up]) : (((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => i | 1 => i) = 0

noncomputable def Electromagnetism.FieldStrength.ofElectricFieldAux {d : ℕ} (E : ElectricField d) (x : SpaceTime d) : (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]

The field strength from an electric field as an element of ℝT[d, .up, .up].

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.timeSliceLinearEquiv_ofElectricFieldAux {d : ℕ} (E : ElectricField d) (t : Time) (x : Space d) : SpaceTime.timeSliceLinearEquiv (ofElectricFieldAux E) t x = (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr.symm (Finsupp.equivFunOnFinite.symm fun (b : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]) => match b 0, b 1 with | ⟨0, ⋯⟩, ⟨j.succ, hj⟩ => -E t x ⟨j, ⋯⟩ | ⟨j.succ, hj⟩, ⟨0, ⋯⟩ => E t x ⟨j, ⋯⟩ | x, x_1 => 0)

noncomputable def Electromagnetism.FieldStrength.ofElectricField {d : ℕ} : ElectricField d →ₗ[ℝ] ↥(FieldStrength d)

The field strength from an eletric field.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.ofElectricField_coe {d : ℕ} (E : ElectricField d) : ↑(ofElectricField E) = ofElectricFieldAux E

noncomputable def Electromagnetism.FieldStrength.ofMagneticFieldAux (B : MagneticField) (x : realLorentzTensor.Tensor ![realLorentzTensor.Color.up]) : realLorentzTensor.Tensor ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]

The field strength from a magnetic field as an element of ℝT[3, .up, .up]. This is only defined here for 4d spacetime.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.timeSliceLinearEquiv_ofMagneticFieldAux (B : MagneticField) (t : Time) (x : Space) : SpaceTime.timeSliceLinearEquiv (ofMagneticFieldAux B) t x = (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr.symm (Finsupp.equivFunOnFinite.symm fun (b : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]) => match b 0, b 1 with | 1, 2 => -B t x 2 | 1, 3 => B t x 1 | 2, 3 => -B t x 0 | 2, 1 => B t x 2 | 3, 1 => -B t x 1 | 3, 2 => B t x 0 | x, x_1 => 0)

noncomputable def Electromagnetism.FieldStrength.ofMagneticField : MagneticField →ₗ[ℝ] ↥FieldStrength

The field strength from a magnetic field.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.ofMagneticField_coe (B : MagneticField) : ↑(ofMagneticField B) = ofMagneticFieldAux B

noncomputable def Electromagnetism.FieldStrength.electricField {d : ℕ} : ↥(FieldStrength d) →ₗ[ℝ] ElectricField d

The electric field given a field strength.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.electricField_apply {d : ℕ} (F : ↥(FieldStrength d)) (t : Time) (x : Space d) (j : Fin d) : electricField F t x j = ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (SpaceTime.timeSliceLinearEquiv (↑F) t x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => ⟨↑j + 1, ⋯⟩ | 1 => 0

theorem Electromagnetism.FieldStrength.timeSliceLinearEquiv_symm_electricField {d : ℕ} (F : ↥(FieldStrength d)) : SpaceTime.timeSliceLinearEquiv.symm (electricField F) = fun (x : SpaceTime d) (j : Fin d) => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => ⟨↑j + 1, ⋯⟩ | 1 => 0

@[simp]

theorem Electromagnetism.FieldStrength.electricField_ofElectricField {d : ℕ} (E : ElectricField d) : electricField (ofElectricField E) = E

noncomputable def Electromagnetism.FieldStrength.magneticField : ↥FieldStrength →ₗ[ℝ] MagneticField

The magnetic field given a field strength.

Equations

• One or more equations did not get rendered due to their size.

theorem Electromagnetism.FieldStrength.magneticField_apply (F : ↥FieldStrength) (t : Time) (x : Space) (j : Fin 3) : magneticField F t x j = match j with | 0 => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (SpaceTime.timeSliceLinearEquiv (↑F) t x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 3 | 1 => 2 | 1 => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (SpaceTime.timeSliceLinearEquiv (↑F) t x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 3 | 2 => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (SpaceTime.timeSliceLinearEquiv (↑F) t x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 2 | 1 => 1

theorem Electromagnetism.FieldStrength.timeSliceLinearEquiv_symm_magneticField (F : ↥FieldStrength) : SpaceTime.timeSliceLinearEquiv.symm (magneticField F) = fun (x : SpaceTime) (j : Fin 3) => match j with | 0 => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 3 | 1 => 2 | 1 => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 1 | 1 => 3 | 2 => ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑F x)) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => 2 | 1 => 1

@[simp]

theorem Electromagnetism.FieldStrength.magneticField_ofMagneticField (B : MagneticField) : magneticField (ofMagneticField B) = B

@[simp]

theorem Electromagnetism.FieldStrength.electricField_ofMagneticField (B : MagneticField) : electricField (ofMagneticField B) = 0

@[simp]

theorem Electromagnetism.FieldStrength.magneticField_ofElectricField (E : ElectricField) : magneticField (ofElectricField E) = 0

theorem Electromagnetism.FieldStrength.eq_ofElectricField_add_ofMagneticField (F : ↥FieldStrength) : F = ofElectricField (electricField F) + ofMagneticField (magneticField F)

noncomputable def Electromagnetism.FieldStrength.toElectricMagneticField : ↥FieldStrength ≃ₗ[ℝ] ElectricField × MagneticField

The isomorphism between the field strength and the electric and magnetic fields.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Electromagnetism.FieldStrength.fromElectricMagneticField : (ElectricField × MagneticField) ≃ₗ[ℝ] ↥FieldStrength

The field strength from an electric and magnetic field.

Equations

• Electromagnetism.FieldStrength.fromElectricMagneticField = Electromagnetism.FieldStrength.toElectricMagneticField.symm

theorem Electromagnetism.FieldStrength.fromElectricMagneticField_repr (EM : ElectricField × MagneticField) (y : SpaceTime) : (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]).repr (↑(fromElectricMagneticField EM) y) = Finsupp.equivFunOnFinite.symm fun (b : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up, realLorentzTensor.Color.up]) => match b 0, b 1 with | 0, 1 => -SpaceTime.timeSliceLinearEquiv.symm EM.1 y 0 | 0, 2 => -SpaceTime.timeSliceLinearEquiv.symm EM.1 y 1 | 0, 3 => -SpaceTime.timeSliceLinearEquiv.symm EM.1 y 2 | 1, 0 => SpaceTime.timeSliceLinearEquiv.symm EM.1 y 0 | 2, 0 => SpaceTime.timeSliceLinearEquiv.symm EM.1 y 1 | 3, 0 => SpaceTime.timeSliceLinearEquiv.symm EM.1 y 2 | 1, 2 => -SpaceTime.timeSliceLinearEquiv.symm EM.2 y 2 | 1, 3 => SpaceTime.timeSliceLinearEquiv.symm EM.2 y 1 | 2, 3 => -SpaceTime.timeSliceLinearEquiv.symm EM.2 y 0 | 2, 1 => SpaceTime.timeSliceLinearEquiv.symm EM.2 y 2 | 3, 1 => -SpaceTime.timeSliceLinearEquiv.symm EM.2 y 1 | 3, 2 => SpaceTime.timeSliceLinearEquiv.symm EM.2 y 0 | x, x_1 => 0

The field strength from an electric and magnetic field written in terms of a basis.