Imports
i. Overview
In this module we define gauge transformations of the electromagnetic potential
A^μ ↦ A^μ + ∂^μ χ where χ : SpaceTime d → ℝ is a smooth gauge function, and prove
that the field strength tensor is invariant under such transformations.
The raised-index gradient ∂^μ χ := η^{μν} ∂_ν χ is necessary because the bare covariant gradient
∂_μ χ does not make F^{μν} invariant. The formal witness is
fieldStrengthMatrix_bareGradient_inl_inr (§B.5), which computes a specific nonzero component of
the field strength of a bare-gradient potential. The invariance theorem
toFieldStrength_gaugeTransform doubles as a correctness test of ofGradient.
ii. Key results
ofGradient : The pure-gauge potential A^μ = η^{μν} ∂_ν χ built from a gauge function χ.
gaugeTransform : The gauge transformation A^μ ↦ A^μ + ∂^μ χ.
toFieldStrength_ofGradient : A pure-gauge potential has vanishing field strength.
toFieldStrength_gaugeTransform : The field strength tensor is invariant under gauge
transformations.
fieldStrengthMatrix_gaugeTransform : The field strength matrix is invariant under gauge
transformations.
gaugeTransform_gaugeTransform : Composing two gauge shifts equals shifting by the sum;
upgrades one-step F-invariance to invariance along any finite chain.
ofGradient_equivariant : ofGradient intertwines the Lorentz action with function composition.
gaugeTransform_equivariant : Gauge transformations commute with Lorentz transformations.
fieldStrengthMatrix_bareGradient_inl_inr : The (inl 0, inr i) field-strength component of
the bare-gradient potential χ(x) = x⁰·xⁱ equals 2; in particular the bare gradient does
not give a gauge-invariant field strength (necessity of the metric contraction in ofGradient).
iii. Table of contents
A. The pure-gauge potential
A.1. Definition and basic lemmas
A.2. Differentiability of the pure-gauge potential
A.3. Vanishing field strength of the pure-gauge potential
A.4. Lorentz equivariance of the pure-gauge potential
B. Gauge transformations
B.1. Definition and basic lemmas
B.2. Invariance of the field strength
B.3. Group structure of gauge shifts
B.4. Equivariance under Lorentz transformations
B.5. Necessity: bare gradient does not give gauge invariance
iv. References
@[ expose ] public section attribute [ - simp ] Fintype.sum_sum_type attribute [ - simp ] Nat.succ_eq_add_one
A. The pure-gauge potential
A.1. Definition and basic lemmas
Unfolding of the summed definition of ofGradient.
lemma ofGradient_apply_sum { d } ( χ : SpaceTime d → ℝ ) ( x : SpaceTime d ) ( μ : Fin 1 ⊕ Fin d ) :
ofGradient χ x μ = ∑ κ , η μ κ * ∂_ κ χ x := rfl
Evaluation of ofGradient in the diagonal form; the off-diagonal entries of η vanish so
only the κ = μ term survives.
The pure-gauge potential built from the zero gauge function has all components zero.
ofGradient is additive in the gauge function (when both summands are differentiable).
A.2. Differentiability of the pure-gauge potential
The pure-gauge potential is differentiable when χ is C^2.
The pure-gauge potential is C^n when χ is C^{n+1}.
A.3. Vanishing field strength of the pure-gauge potential
A pure-gauge potential has vanishing field strength.
A.4. Lorentz equivariance of the pure-gauge potential
ofGradient intertwines the Lorentz action on potentials with composition by Λ⁻¹ on the gauge
function: Λ • ofGradient χ = ofGradient (χ ∘ (Λ⁻¹ • ·)). The proof reduces to the
metric-commutativity identity Λ * η = η * (Λ⁻¹)ᵀ, which is the defining property of the
Lorentz group (LorentzGroup.comm_minkowskiMatrix).
ofGradient intertwines the Lorentz action on potentials with composition by Λ⁻¹ on the
gauge function: Λ • ofGradient χ = ofGradient (χ ∘ (Λ⁻¹ • ·)).
lemma ofGradient_equivariant { d } ( χ : SpaceTime d → ℝ ) ( hχ : Differentiable ℝ χ )
( Λ : LorentzGroup d ) :
Λ • ofGradient χ = ofGradient ( χ ∘ ( Λ ⁻¹ • · ) ) := by d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x )
have hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ) ,
∑ ν , Λ . 1 μ ν * η ν κ = ∑ ν , η μ ν * ( Λ ⁻¹ ) . 1 κ ν := by
intro μ κ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) μ : Fin 1 ⊕ Fin d κ : Fin 1 ⊕ Fin d ⊢ ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x )
have h := congr_fun₂ ( LorentzGroup.comm_minkowskiMatrix ( Λ := Λ ) ) μ κ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) μ : Fin 1 ⊕ Fin d κ : Fin 1 ⊕ Fin d h : ( ↑ Λ * η ) μ κ = ( η * ↑ ( LorentzGroup.transpose Λ ⁻¹ ) ) μ κ ⊢ ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x )
simp only [ Matrix.mul_apply , LorentzGroup.transpose_val , Matrix.transpose_apply ] at h d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) μ : Fin 1 ⊕ Fin d κ : Fin 1 ⊕ Fin d h : ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x )
exact h d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x )
apply eq_of_val_eq d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν ⊢ ( Λ • ofGradient χ ) . val = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val ; funext x μ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
set a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
have hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , ( ∑ ν , Λ . 1 μ ν * η ν κ ) * a κ := by d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
simp only [ ElectromagneticPotential.action_val , Lorentz.Vector.smul_eq_sum , a ,
ofGradient_apply_sum , Finset.mul_sum ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) ⊢ ∑ x_1 , ∑ i , ↑ Λ μ x_1 * ( η x_1 i * ∂_ i χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
rw [ Finset.sum_comm d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) ⊢ ∑ y , ∑ x_1 , ↑ Λ μ x_1 * ( η x_1 y * ∂_ y χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) ⊢ ∑ y , ∑ x_1 , ↑ Λ μ x_1 * ( η x_1 y * ∂_ y χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) ⊢ ∑ y , ∑ x_1 , ↑ Λ μ x_1 * ( η x_1 y * ∂_ y χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
apply Finset.sum_congr rfl d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) ⊢ ∀ x_1 ∈ Finset.univ , ∑ x_2 , ↑ Λ μ x_2 * ( η x_2 x_1 * ∂_ x_1 χ ( Λ ⁻¹ • x ) ) = (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ; intro κ _ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ ∑ x_1 , ↑ Λ μ x_1 * ( η x_1 κ * ∂_ κ χ ( Λ ⁻¹ • x ) ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
simp_rw [ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ ∑ x_1 , ↑ Λ μ x_1 * ( η x_1 κ * ∂_ κ χ ( Λ ⁻¹ • x ) ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ← mul_assoc d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ ∑ x_1 , ↑ Λ μ x_1 * η x_1 κ * ∂_ κ χ ( Λ ⁻¹ • x ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ]
rw [ ← Finset.sum_mul d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ (∑ i , ↑ Λ μ i * η i κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
have hrhs : ( ofGradient ( χ ∘ ( Λ ⁻¹ • · ) ) ) . val x μ = ∑ κ , ( ∑ ν , Λ . 1 μ ν * η ν κ ) * a κ := by d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) ⊢ Λ • ofGradient χ = ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
simp only [ ofGradient_apply_sum , a ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ κ , η μ κ * ∂_ κ ( χ ∘ fun x => Λ ⁻¹ • x ) x = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
conv_lhs =>
enter [ 2 , ν ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ν : Fin 1 ⊕ Fin d | η μ ν * ∂_ ν ( χ ∘ fun x => Λ ⁻¹ • x ) x d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
rw [ show ∂_ ν ( χ ∘ ( Λ ⁻¹ • · ) ) x = ∂_ ν ( fun y => χ ( Λ ⁻¹ • y ) ) x from rfl ,
SpaceTime.deriv_comp_lorentz_action ν χ hχ Λ ⁻¹ x ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ν : Fin 1 ⊕ Fin d | η μ ν * ∑ ν_1 , ↑ Λ ⁻¹ ν_1 ν • ∂_ ν_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
simp only [ smul_eq_mul , Finset.mul_sum ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ x_1 , ∑ i , η μ x_1 * ( ↑ Λ ⁻¹ i x_1 * ∂_ i χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
rw [ Finset.sum_comm d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ y , ∑ x_1 , η μ x_1 * ( ↑ Λ ⁻¹ y x_1 * ∂_ y χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ y , ∑ x_1 , η μ x_1 * ( ↑ Λ ⁻¹ y x_1 * ∂_ y χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ y , ∑ x_1 , η μ x_1 * ( ↑ Λ ⁻¹ y x_1 * ∂_ y χ ( Λ ⁻¹ • x ) ) = ∑ x_1 , (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
apply Finset.sum_congr rfl d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∀ x_1 ∈ Finset.univ , ∑ x_2 , η μ x_2 * ( ↑ Λ ⁻¹ x_1 x_2 * ∂_ x_1 χ ( Λ ⁻¹ • x ) ) = (∑ ν , ↑ Λ μ ν * η ν x_1 ) * ∂_ x_1 χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ; intro κ _ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ ∑ x_1 , η μ x_1 * ( ↑ Λ ⁻¹ κ x_1 * ∂_ κ χ ( Λ ⁻¹ • x ) ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
simp_rw [ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ ∑ x_1 , η μ x_1 * ( ↑ Λ ⁻¹ κ x_1 * ∂_ κ χ ( Λ ⁻¹ • x ) ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ← mul_assoc d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ ∑ x_1 , η μ x_1 * ↑ Λ ⁻¹ κ x_1 * ∂_ κ χ ( Λ ⁻¹ • x ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ]
rw [ ← Finset.sum_mul , d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ (∑ i , η μ i * ↑ Λ ⁻¹ κ i ) * ∂_ κ χ ( Λ ⁻¹ • x ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ← hmetric d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ κ : Fin 1 ⊕ Fin d a✝ : κ ∈ Finset.univ ⊢ (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) = (∑ ν , ↑ Λ μ ν * η ν κ ) * ∂_ κ χ ( Λ ⁻¹ • x ) d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ ] d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ( Λ • ofGradient χ ) . val x μ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ
rw [ hlhs , d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ = ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ All goals completed! 🐙 hrhs d : ℕ χ : SpaceTime d → ℝ hχ : Differentiable ℝ χ Λ : ↑ ( LorentzGroup d ) hmetric : ∀ ( μ κ : Fin 1 ⊕ Fin d ), ∑ ν , ↑ Λ μ ν * η ν κ = ∑ ν , η μ ν * ↑ Λ ⁻¹ κ ν x : SpaceTime d μ : Fin 1 ⊕ Fin d a : Fin 1 ⊕ Fin d → ℝ := fun κ => ∂_ κ χ ( Λ ⁻¹ • x ) hlhs : ( Λ • ofGradient χ ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ hrhs : ( ofGradient ( χ ∘ fun x => Λ ⁻¹ • x ) ) . val x μ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ ⊢ ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ = ∑ κ , (∑ ν , ↑ Λ μ ν * η ν κ ) * a κ All goals completed! 🐙 ] All goals completed! 🐙
B.1. Definition and basic lemmas
Evaluation of gaugeTransform.
B.2. Invariance of the field strength
The key ingredient — that a pure-gauge potential has vanishing field strength — is proved in §A.3
(toFieldStrength_ofGradient).
The field strength tensor is invariant under gauge transformations.
The field strength matrix is invariant under gauge transformations.
B.3. Group structure of gauge shifts
Composing two gauge shifts by χ₁ and χ₂ is the same as shifting by χ₁ + χ₂. Together with
gaugeTransform_zero this shows that the map χ ↦ (A ↦ gaugeTransform χ A) is a group action
of the additive group of smooth functions. (We do not build the formal MulAction here —
the composition lemma is the agreeable core, and the rest is straightforward from it.)
The ofGradient lemmas used here — ofGradient_zero and ofGradient_add — are proved in §A.1.
Shifting by the zero gauge function is the identity.
Two successive gauge shifts compose: shifting by χ₂ then χ₁ equals shifting by χ₁ + χ₂.
This upgrades one-step F-invariance to invariance along any finite chain of gauge shifts.
The gauge-transformation map commutes with the Lorentz group action: applying Λ to a potential
and then gauge-transforming by χ is the same as gauge-transforming by χ ∘ (Λ⁻¹ • ·) and then
applying Λ. The proof delegates to ofGradient_equivariant (§A.4).
Gauge transformations commute with Lorentz transformations: applying Λ and then performing
a gauge transformation by χ equals performing a gauge transformation by χ ∘ (Λ⁻¹ • ·)
and then applying Λ.
B.5. Necessity: bare gradient does not give gauge invariance
We exhibit a concrete gauge function χ(x) = x⁰·xⁱ whose bare covariant gradient
B^μ := ∂_μ χ has a nonzero field-strength component (equal to 2), certifying that the metric
contraction in ofGradient is required for gauge invariance.
The (inl 0, inr i) component of the field strength matrix of the bare-gradient potential
B^μ := ∂_μ χ for χ(x) = x⁰·xⁱ equals 2. This witnesses that the bare covariant gradient
does not produce a gauge-invariant field strength, so the raised-index contraction
η^{μν} ∂_ν χ in ofGradient is necessary (see the module overview).
lemma fieldStrengthMatrix_bareGradient_inl_inr { d : ℕ } ( i : Fin d )
( x : SpaceTime d ) :
let χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i )
let B : ElectromagneticPotential d := ⟨ fun y μ => ∂_ μ χ y ⟩
B . fieldStrengthMatrix x ( Sum.inl 0 , Sum.inr i ) = 2 := by d : ℕ i : Fin d x : SpaceTime d ⊢ let χ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ;
let B := { val := fun y μ => ∂_ μ χ y } ;
( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
intro χ B d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
have hχ : ContDiff ℝ 2 χ := by d : ℕ i : Fin d x : SpaceTime d ⊢ let χ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ;
let B := { val := fun y μ => ∂_ μ χ y } ;
( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
show ContDiff ℝ 2 ( fun y : SpaceTime d => y ( Sum.inl 0 ) * y ( Sum.inr i ) ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } ⊢ ContDiff ℝ 2 fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
fun_prop d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
have hB : Differentiable ℝ B := by d : ℕ i : Fin d x : SpaceTime d ⊢ let χ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ;
let B := { val := fun y μ => ∂_ μ χ y } ;
( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
rw [ ← SpaceTime.differentiable_vector d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ∀ ( ν : Fin 1 ⊕ Fin d ), Differentiable ℝ fun x => B . val x ν d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ∀ ( ν : Fin 1 ⊕ Fin d ), Differentiable ℝ fun x => B . val x ν d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ ⊢ ∀ ( ν : Fin 1 ⊕ Fin d ), Differentiable ℝ fun x => B . val x ν d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 ; intro μ d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ μ : Fin 1 ⊕ Fin d ⊢ Differentiable ℝ fun x => B . val x μ d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
exact SpaceTime.differentiable_deriv μ χ hχ d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ ( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2
rw [ toFieldStrength_basis_repr_apply_eq_single d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 * ∂_ ( Sum.inl 0 , Sum.inr i ) .1 B . val x ( Sum.inl 0 , Sum.inr i ) .2 -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 * ∂_ ( Sum.inl 0 , Sum.inr i ) .2 B . val x ( Sum.inl 0 , Sum.inr i ) .1 =
2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 * ∂_ ( Sum.inl 0 , Sum.inr i ) .1 B . val x ( Sum.inl 0 , Sum.inr i ) .2 -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 * ∂_ ( Sum.inl 0 , Sum.inr i ) .2 B . val x ( Sum.inl 0 , Sum.inr i ) .1 =
2 ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 * ∂_ ( Sum.inl 0 , Sum.inr i ) .1 B . val x ( Sum.inl 0 , Sum.inr i ) .2 -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 * ∂_ ( Sum.inl 0 , Sum.inr i ) .2 B . val x ( Sum.inl 0 , Sum.inr i ) .1 =
2
rw [ SpaceTime.deriv_apply_eq ( Sum.inl 0 ) ( Sum.inr i ) B hB , d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 * ∂_ ( Sum.inl 0 , Sum.inr i ) .2 B . val x ( Sum.inl 0 , Sum.inr i ) .1 =
2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
SpaceTime.deriv_apply_eq ( Sum.inr i ) ( Sum.inl 0 ) B hB d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
have hfderiv : ∀ ( y : SpaceTime d ) ,
fderiv ℝ χ y = ( y ( Sum.inr i ) ) • Lorentz.Vector.coordCLM ( Sum.inl 0 ) +
( y ( Sum.inl 0 ) ) • Lorentz.Vector.coordCLM ( Sum.inr i ) := fun y => by d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
have h : fderiv ℝ ( fun z : SpaceTime d => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
( y ( Sum.inr i ) ) • Lorentz.Vector.coordCLM ( Sum.inl 0 ) +
( y ( Sum.inl 0 ) ) • Lorentz.Vector.coordCLM ( Sum.inr i ) := by
have hmul := fderiv_fun_mul ( 𝕜 := ℝ )
( hc := ( Lorentz.Vector.coordCLM ( Sum.inl 0 ) ) . differentiableAt )
( hd := ( Lorentz.Vector.coordCLM ( Sum.inr i ) ) . differentiableAt ) ( x := y ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d hmul : fderiv ℝ (fun y => ( Vector.coordCLM ( Sum.inl 0 ) ) y * ( Vector.coordCLM ( Sum.inr i ) ) y ) y =
( Vector.coordCLM ( Sum.inl 0 ) ) y • fderiv ℝ (⇑ ( Vector.coordCLM ( Sum.inr i ) ) ) y +
( Vector.coordCLM ( Sum.inr i ) ) y • fderiv ℝ (⇑ ( Vector.coordCLM ( Sum.inl 0 ) ) ) y ⊢ fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d h : fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
simp only [ ContinuousLinearMap.fderiv , Lorentz.Vector.coordCLM_apply ] at hmul d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d hmul : fderiv ℝ (fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ) y =
y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) + y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) ⊢ fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d h : fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
rw [ hmul , d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d hmul : fderiv ℝ (fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ) y =
y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) + y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) ⊢ y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) + y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d h : fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 add_comm d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d hmul : fderiv ℝ (fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ) y =
y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) + y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) ⊢ y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d h : fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d h : fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val y : SpaceTime d h : fderiv ℝ (fun z => z ( Sum.inl 0 ) * z ( Sum.inr i ) ) y =
y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
exact h d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 , Sum.inr i ) .1 ( Sum.inl 0 , Sum.inr i ) .1 *
( fderiv ℝ (fun x => B . val x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inl 0 , Sum.inr i ) .2 ( Sum.inl 0 , Sum.inr i ) .2 *
( fderiv ℝ (fun x => B . val x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
simp only [ SpaceTime.deriv_eq , B ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 ) ( Sum.inl 0 ) *
( fderiv ℝ (fun x => ( fderiv ℝ χ x ) ( Vector.basis ( Sum.inr i ) ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inr i ) ( Sum.inr i ) *
( fderiv ℝ (fun x => ( fderiv ℝ χ x ) ( Vector.basis ( Sum.inl 0 ) ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
simp_rw [ d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 ) ( Sum.inl 0 ) *
( fderiv ℝ (fun x => ( fderiv ℝ χ x ) ( Vector.basis ( Sum.inr i ) ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inr i ) ( Sum.inr i ) *
( fderiv ℝ (fun x => ( fderiv ℝ χ x ) ( Vector.basis ( Sum.inl 0 ) ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2 hfderiv d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 ) ( Sum.inl 0 ) *
( fderiv ℝ
(fun x =>
( x ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + x ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) )
( Vector.basis ( Sum.inr i ) ) )
x )
( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inr i ) ( Sum.inr i ) *
( fderiv ℝ
(fun x =>
( x ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + x ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) )
( Vector.basis ( Sum.inl 0 ) ) )
x )
( Vector.basis ( Sum.inr i ) ) =
2 ]
simp only [ _root_.add_apply , FunLike.coe_smul ,
Pi.smul_apply , Lorentz.Vector.coordCLM_apply , smul_eq_mul , Lorentz.Vector.basis_apply ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 ) ( Sum.inl 0 ) *
( fderiv ℝ
(fun x => ( x ( Sum.inr i ) * if Sum.inr i = Sum.inl 0 then 1 else 0 ) + x ( Sum.inl 0 ) * if True then 1 else 0 ) x )
( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inr i ) ( Sum.inr i ) *
( fderiv ℝ
(fun x => ( x ( Sum.inr i ) * if True then 1 else 0 ) + x ( Sum.inl 0 ) * if Sum.inl 0 = Sum.inr i then 1 else 0 ) x )
( Vector.basis ( Sum.inr i ) ) =
2
simp only [ mul_ite , mul_one , mul_zero , ite_add , zero_add , if_true ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ η ( Sum.inl 0 ) ( Sum.inl 0 ) *
( fderiv ℝ (fun x => if Sum.inr i = Sum.inl 0 then x ( Sum.inr i ) + x ( Sum.inl 0 ) else x ( Sum.inl 0 ) ) x )
( Vector.basis ( Sum.inl 0 ) ) -
η ( Sum.inr i ) ( Sum.inr i ) *
( fderiv ℝ (fun x => x ( Sum.inr i ) + if Sum.inl 0 = Sum.inr i then x ( Sum.inl 0 ) else 0 ) x )
( Vector.basis ( Sum.inr i ) ) =
2
simp only [ minkowskiMatrix.inl_0_inl_0 , minkowskiMatrix.inr_i_inr_i ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ 1 *
( fderiv ℝ (fun x => if Sum.inr i = Sum.inl 0 then x ( Sum.inr i ) + x ( Sum.inl 0 ) else x ( Sum.inl 0 ) ) x )
( Vector.basis ( Sum.inl 0 ) ) -
- 1 *
( fderiv ℝ (fun x => x ( Sum.inr i ) + if Sum.inl 0 = Sum.inr i then x ( Sum.inl 0 ) else 0 ) x )
( Vector.basis ( Sum.inr i ) ) =
2
simp only [ reduceCtorEq , ↓ reduceIte , add_zero ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ 1 * ( fderiv ℝ (fun x => x ( Sum.inl 0 ) ) x ) ( Vector.basis ( Sum.inl 0 ) ) -
- 1 * ( fderiv ℝ (fun x => x ( Sum.inr i ) ) x ) ( Vector.basis ( Sum.inr i ) ) =
2
simp only [ Lorentz.Vector.fderiv_coord , Lorentz.Vector.coordCLM_apply ,
Lorentz.Vector.basis_apply , ↓ reduceIte ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } hχ : ContDiff ℝ 2 χ hB : Differentiable ℝ B . val hfderiv : ∀ ( y : SpaceTime d ),
fderiv ℝ χ y = y ( Sum.inr i ) • Vector.coordCLM ( Sum.inl 0 ) + y ( Sum.inl 0 ) • Vector.coordCLM ( Sum.inr i ) ⊢ 1 * 1 - - 1 * 1 = 2
norm_num All goals completed! 🐙
The field strength of the bare-gradient potential B^μ := ∂_μ χ for
χ(x) = x⁰·xⁱ is nonzero (follows from fieldStrengthMatrix_bareGradient_inl_inr).
lemma toFieldStrength_bareGradient_ne_zero { d : ℕ } ( i : Fin d )
( x : SpaceTime d ) :
let χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i )
let B : ElectromagneticPotential d := ⟨ fun y μ => ∂_ μ χ y ⟩
B . toFieldStrength x ≠ 0 := by d : ℕ i : Fin d x : SpaceTime d ⊢ let χ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ;
let B := { val := fun y μ => ∂_ μ χ y } ;
B . toFieldStrength x ≠ 0
intro χ B h d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 ⊢ False
have h2 := fieldStrengthMatrix_bareGradient_inl_inr i x d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : have χ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ;
have B := { val := fun y μ => ∂_ μ χ y } ;
( B . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 ⊢ False
dsimp only at h2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( { val := fun y μ => ∂_ μ (fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ) y } . fieldStrengthMatrix x ) ( Sum.inl 0 , Sum.inr i ) = 2 ⊢ False
rw [ fieldStrengthMatrix_eq , d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( ( CoVector.basis . tensorProduct Vector.basis ) . repr
( { val := fun y μ => ∂_ μ (fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) ) y } . toFieldStrength x ) )
( Sum.inl 0 , Sum.inr i ) =
2 ⊢ False d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 ) ( Sum.inl 0 , Sum.inr i ) = 2 ⊢ False h d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 ) ( Sum.inl 0 , Sum.inr i ) = 2 ⊢ False d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 ) ( Sum.inl 0 , Sum.inr i ) = 2 ⊢ False ] at h2 d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 ) ( Sum.inl 0 , Sum.inr i ) = 2 ⊢ False
have h3 : ( ( Lorentz.CoVector.basis . tensorProduct Lorentz.Vector.basis ) . repr
( 0 : Lorentz.CoVector d ⊗[ ℝ ] Lorentz.Vector d ) ) = 0 := map_zero _ d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : ( ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 ) ( Sum.inl 0 , Sum.inr i ) = 2 h3 : ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 = 0 ⊢ False
erw [ h3 , d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : 0 ( Sum.inl 0 , Sum.inr i ) = 2 h3 : ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 = 0 ⊢ False Finsupp.zero_apply d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : 0 = 2 h3 : ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 = 0 ⊢ False ] d : ℕ i : Fin d x : SpaceTime d χ : SpaceTime d → ℝ := fun y => y ( Sum.inl 0 ) * y ( Sum.inr i ) B : ElectromagneticPotential d := { val := fun y μ => ∂_ μ χ y } h : B . toFieldStrength x = 0 h2 : 0 = 2 h3 : ( CoVector.basis . tensorProduct Vector.basis ) . repr 0 = 0 ⊢ False at h2
norm_num at h2 All goals completed! 🐙