Research proof index

Second derivatives distribute coordinate-wise over subtraction (two components for curl). -/ lemma deriv_coord_2nd_sub (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : ∂[u] (fun x => ∂[v] (fun x => f x w) x - ∂[w] (fun x => f x v) x) = (∂[u] (∂[v] (fun x => f x w))) - (∂[u] (∂[w] (fun x => f x v))) := by repeat rw [deriv_eq_fderiv_fun] ext x...

The homotopy operator is defined as ∫ t in 0..1, (t • x) ⨯ f (t • x). This is the integrand of that function. -/ private noncomputable def homotopyOperatorIntegrand (f : Space → EuclideanSpace ℝ (Fin 3)) : Space → ℝ → EuclideanSpace ℝ (Fin 3) := fun x t => (t • basis.repr x) ⨯ₑ₃ f (t • x) private lemma homotopyOperatorIntegrand_eq (f : Space → Euclidean...

The curl of a grad is equal to zero.

Second derivatives distribute coordinate-wise over subtraction (two components for curl). -/ lemma deriv_coord_2nd_sub (f : Space → EuclideanSpace ℝ (Fin 3)) (hf : ContDiff ℝ 2 f) : ∂[u] (fun x => ∂[v] (fun x => f x w) x - ∂[w] (fun x => f x v) x) = (∂[u] (∂[v] (fun x => f x w))) - (∂[u] (∂[w] (fun x => f x v))) := by repeat rw [deriv_eq_fderiv_fun] ext x...

A constructive form of the statement that if the curl of a function is zero, then it is equal to the grad of another function. In the context of e.g. electromagnetism the potential given by this lemma corresponds to that defined by the work done to move a unit charge from the origin to the point x along a straight line.