1. Physlib
  2. SpaceAndTime
  3. Space
  4. Derivatives
  5. Curl
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Zhi Kai Pong, Joseph Tooby-Smith, Lode Vermeulen -/ module public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian public import Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare public import Physlib.SpaceAndTime.Space.CrossProduct public import Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Curl on Space

i. Overview

In this module we define the curl of functions and distributions on 3-dimensional space Space 3.

We also prove some basic vector-identities involving of the curl operator.

ii. Key results

    curl : The curl operator on functions from Space 3 to EuclideanSpace ℝ (Fin 3).

    distCurl : The curl operator on distributions from Space 3 to EuclideanSpace ℝ (Fin 3).

    div_of_curl_eq_zero : The divergence of the curl of a function is zero.

    distCurl_distGrad_eq_zero : The curl of the gradient of a distribution is zero.

iii. Table of contents

    A. The curl on functions

      A.1. The curl on the zero function

      A.2. The curl on a constant function

      A.3. Basic operations on curl

      A.4. The curl of a linear map is a linear map

      A.5. Preliminary lemmas about second derivatives

      A.6. The div of a curl is zero

      A.7. The curl of a grad is zero

      A.8. The curl of a curl

      A.9. A divergence-free field is a curl

      A.10. A curl-free field is a gradient

    B. The curl on distributions

      B.1. The components of the curl

      B.2. Basic equalities

      B.3. The curl of a grad is zero

iv. References

@[expose] public section

A. The curl on functions

@[inherit_doc curl] macro (name := curlNotation) "∇" "⨯" f:term:100 : term => `(curl $f)

A.1. The curl on the zero function

@[simp] lemma curl_zero : ∇ ⨯ (0 : Space → EuclideanSpace ℝ (Fin 3)) = 0 := ⊢ curl 0 = 0 ⊢ (fun x => have fi := fun i x => (0 x).ofLp i; WithLp.toLp 2 fun i => (fderiv ℝ (fi (i + 2)) x) (basis (i + 1)) - (fderiv ℝ (fi (i + 1)) x) (basis (i + 2))) = 0 ⊢ (fun x => WithLp.toLp 2 fun i => 0) = 0 All goals completed! 🐙

A.2. The curl on a constant function

@[simp] lemma curl_const : ∇ ⨯ (fun _ : Space => v₃) = 0 := v₃:EuclideanSpace ℝ (Fin 3)⊢ (curl fun x => v₃) = 0 v₃:EuclideanSpace ℝ (Fin 3)⊢ (fun x => have fi := fun i x => ((fun x => v₃) x).ofLp i; WithLp.toLp 2 fun i => (fderiv ℝ (fi (i + 2)) x) (basis (i + 1)) - (fderiv ℝ (fi (i + 1)) x) (basis (i + 2))) = 0 v₃:EuclideanSpace ℝ (Fin 3)⊢ (fun x => WithLp.toLp 2 fun i => 0) = 0 All goals completed! 🐙

A.3. Basic operations on curl

f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ ((deriv (⟨2, ⋯⟩ + 1) fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 2)) + deriv (⟨2, ⋯⟩ + 1) fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 2)) x - ((deriv (⟨2, ⋯⟩ + 2) fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 1)) + deriv (⟨2, ⋯⟩ + 2) fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 1)) x = deriv (⟨2, ⋯⟩ + 1) (fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 2)) x - deriv (⟨2, ⋯⟩ + 2) (fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 1)) x + (deriv (⟨2, ⋯⟩ + 1) (fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 2)) x - deriv (⟨2, ⋯⟩ + 2) (fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 1)) x)f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f2f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f2 f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ deriv (⟨2, ⋯⟩ + 1) (fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 2)) x + deriv (⟨2, ⋯⟩ + 1) (fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 2)) x - (deriv (⟨2, ⋯⟩ + 2) (fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 1)) x + deriv (⟨2, ⋯⟩ + 2) (fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 1)) x) = deriv (⟨2, ⋯⟩ + 1) (fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 2)) x - deriv (⟨2, ⋯⟩ + 2) (fun x => (f1 x).ofLp (⟨2, ⋯⟩ + 1)) x + (deriv (⟨2, ⋯⟩ + 1) (fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 2)) x - deriv (⟨2, ⋯⟩ + 2) (fun x => (f2 x).ofLp (⟨2, ⋯⟩ + 1)) x)f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f2f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f2 f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f2f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space⊢ Differentiable ℝ f2 repeat All goals completed! 🐙f:Space → EuclideanSpace ℝ (Fin 3)k:ℝhf:Differentiable ℝ fx:Spacei:Fin 3⊢ Differentiable ℝ ff:Space → EuclideanSpace ℝ (Fin 3)k:ℝhf:Differentiable ℝ fx:Spacei:Fin 3⊢ Differentiable ℝ f repeat All goals completed! 🐙All goals completed! 🐙f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ Differentiable ℝ f2f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ Differentiable ℝ f1f1:Space → EuclideanSpace ℝ (Fin 3)f2:Space → EuclideanSpace ℝ (Fin 3)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ Differentiable ℝ (-f2) repeat All goals completed! 🐙

A.4. The curl of a linear map is a linear map

W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fk:ℝw:W⊢ Differentiable ℝ (f w) All goals completed! 🐙

A.5. Preliminary lemmas about second derivatives

Second derivatives distribute coordinate-wise over addition (all three components for div).

i:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) x + (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x + fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x)) (basis i) = (((fun x => (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) x) (basis i)) + fun x => (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x) (basis i)) + fun x => (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x) (basis i)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x + (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x) x i:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) x) (basis i) + ((fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x) (basis i) + (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x) (basis i)) = (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) x) (basis i) + (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x) (basis i) + (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x) (basis i)i:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x + (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x) x i:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp u) x) (basis u)) xi:Fin 3u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis v)) x + (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis w)) x) x repeat All goals completed! 🐙

Second derivatives distribute coordinate-wise over subtraction (two components for curl).

u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis v)) x - fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis w)) x) (basis u) = (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis v)) x) (basis u) - (fderiv ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis w)) x) (basis u)u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis v)) xu:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis w)) x u:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp w) x) (basis v)) xu:Fin 3v:Fin 3w:Fin 3f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ DifferentiableAt ℝ (fun x => (fderiv ℝ (fun x => (f x).ofLp v) x) (basis w)) x repeat All goals completed! 🐙

A.6. The div of a curl is zero

f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ deriv 1 (deriv 0 fun x => (f x).ofLp 2) x - deriv 2 (deriv 0 fun x => (f x).ofLp 1) x + (deriv 2 (deriv 1 fun x => (f x).ofLp 0) x - deriv 1 (deriv 0 fun x => (f x).ofLp 2) x + (deriv 2 (deriv 0 fun x => (f x).ofLp 1) x - deriv 2 (deriv 1 fun x => (f x).ofLp 0) x)) = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 2f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 1f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 f f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 2f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 1f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 f repeat try f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 f All goals completed! 🐙

A.7. The curl of a grad is zero

f:Space → ℝhf:ContDiff ℝ 2 fx:Spacei:Fin 3⊢ deriv (i + 2) (deriv (i + 1) f) x - deriv (i + 2) (fun x => deriv (i + 1) f x) x = 0 All goals completed! 🐙

A.8. The curl of a curl

f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ deriv 2 (deriv 0 fun x => (f x).ofLp 0) x - deriv 0 (deriv 0 fun x => (f x).ofLp 2) x - (deriv 1 (deriv 1 fun x => (f x).ofLp 2) x - deriv 2 (deriv 1 fun x => (f x).ofLp 1) x) = (deriv 2 (deriv 0 fun x => (f x).ofLp 0) + deriv 2 (deriv 1 fun x => (f x).ofLp 1) + deriv 2 (deriv 2 fun x => (f x).ofLp 2)) x - (deriv 0 (deriv 0 fun x => (f x).ofLp 2) x + (deriv 1 (fun x => deriv 1 (fun x => (f x).ofLp 2) x) x + deriv 2 (fun x => deriv 2 (fun x => (f x).ofLp 2) x) x))f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 2f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 1f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 f f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ deriv 2 (deriv 0 fun x => (f x).ofLp 0) x - deriv 0 (deriv 0 fun x => (f x).ofLp 2) x - (deriv 1 (deriv 1 fun x => (f x).ofLp 2) x - deriv 2 (deriv 1 fun x => (f x).ofLp 1) x) = deriv 2 (deriv 0 fun x => (f x).ofLp 0) x + deriv 2 (deriv 1 fun x => (f x).ofLp 1) x + deriv 2 (deriv 2 fun x => (f x).ofLp 2) x - (deriv 0 (deriv 0 fun x => (f x).ofLp 2) x + (deriv 1 (fun x => deriv 1 (fun x => (f x).ofLp 2) x) x + deriv 2 (fun x => deriv 2 (fun x => (f x).ofLp 2) x) x))f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 2f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 1f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 f f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 2f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 1f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 fun x => (f x).ofLp 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 ff:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 2 fx:Space⊢ ContDiff ℝ 2 f repeat All goals completed! 🐙

### A.9. A divergence-free field is a curl

We now prove that if the divergence of a function is zero, then it is equal to the curl of some function.

This proof is involved, thus we have split it up into private definitions and lemmas. The proof is by explicit construction. If f has divergence zero, then we construct

∫ t in 0..1, (t • x) ⨯ f (t • x)

and show that the curl of this is equal to f.

We call the integrand of this function the homotopyOperatorIntegrand. We build API around this to help in our proof.

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 → EuclideanSpace ℝ (Fin 3)) : homotopyOperatorIntegrand f = fun x t => (t • basis.repr x) ⨯ₑ₃ f (t • x) := f:Space → EuclideanSpace ℝ (Fin 3)⊢ homotopyOperatorIntegrand f = fun x t => (fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) (t • basis.repr x) (f (t • x)) All goals completed! 🐙@[fun_prop] private lemma differentiable_homotopyOperatorIntegrand_space {f : Space → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) (t : ℝ) : Differentiable ℝ (homotopyOperatorIntegrand f · t) := f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => homotopyOperatorIntegrand f x t f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp) f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ ∀ (i : Fin 3), Differentiable ℝ fun x => (t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)).ofLp i f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝi:Fin 3⊢ Differentiable ℝ fun x => (t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)).ofLp i f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => (t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)).ofLp ((fun i => i) ⟨0, ⋯⟩)f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => (t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)).ofLp ((fun i => i) ⟨1, ⋯⟩)f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => (t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)).ofLp ((fun i => i) ⟨2, ⋯⟩) all_goals f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => (t • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)).ofLp ((fun i => i) ⟨2, ⋯⟩) f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ ft:ℝ⊢ Differentiable ℝ fun x => t * (x.val 3 0 * (f (t • x)).ofLp 1 - x.val 3 1 * (f (t • x)).ofLp 0) All goals completed! 🐙f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun x_1 => x_1 • WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (x_1 • x)).ofLp) refine Continuous.comp' (f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous (WithLp.toLp 2) All goals completed! 🐙) ?_ f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ ∀ (i : Fin 3), Continuous fun a => (a • (WithLp.equiv 2 (Fin 3 → ℝ)).toFun (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (a • x)).ofLp))) i f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp ii:Fin 3⊢ Continuous fun a => (a • (WithLp.equiv 2 (Fin 3 → ℝ)).toFun (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (a • x)).ofLp))) i f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => (a • (WithLp.equiv 2 (Fin 3 → ℝ)).toFun (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (a • x)).ofLp))) ((fun i => i) ⟨0, ⋯⟩)f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => (a • (WithLp.equiv 2 (Fin 3 → ℝ)).toFun (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (a • x)).ofLp))) ((fun i => i) ⟨1, ⋯⟩)f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => (a • (WithLp.equiv 2 (Fin 3 → ℝ)).toFun (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (a • x)).ofLp))) ((fun i => i) ⟨2, ⋯⟩) all_goals f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => (a • (WithLp.equiv 2 (Fin 3 → ℝ)).toFun (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (a • x)).ofLp))) ((fun i => i) ⟨2, ⋯⟩) f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => a * (x.val 3 0 * (f (a • x)).ofLp 1 - x.val 3 1 * (f (a • x)).ofLp 0) refine Continuous.fun_mul (f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => a All goals completed! 🐙) ?_ f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => x.val 3 0 * (f (a • x)).ofLp 1f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => x.val 3 1 * (f (a • x)).ofLp 0 all_goals f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => x.val 3 1 * (f (a • x)).ofLp 0 f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => x.val 3 1f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => (f (a • x)).ofLp 0 f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => x.val 3 1 All goals completed! 🐙 f:Space → EuclideanSpace ℝ (Fin 3)hf✝:Differentiable ℝ fx:Spacehf:∀ (i : Fin 3), Continuous fun t => (f (t • x)).ofLp i⊢ Continuous fun a => (f (a • x)).ofLp 0 All goals completed! 🐙private lemma intervalIntegrable_homotopyOperatorIntegrand {f : Space → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) (x : Space) : IntervalIntegrable (homotopyOperatorIntegrand f x ·) volume (0 : ℝ) 1 := Continuous.intervalIntegrable (f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Space⊢ Continuous fun x_1 => homotopyOperatorIntegrand f x x_1 All goals completed! 🐙) 0 1f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ t • ((fderiv ℝ (fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) x) y).ofLp i = t • (fderiv ℝ (⇑(EuclideanSpace.proj i)) (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) ∘SL fderiv ℝ (fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) x) yf:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj i)) (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp))f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ DifferentiableAt ℝ (fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj i)) (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp))f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ DifferentiableAt ℝ (fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ DifferentiableAt ℝ (⇑(EuclideanSpace.proj i)) (WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) All goals completed! 🐙 f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacei:Fin 3cross_diff:∀ (t : ℝ), Differentiable ℝ fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)⊢ DifferentiableAt ℝ (fun x => WithLp.toLp 2 ((crossProduct (basis.repr x).ofLp) (f (t • x)).ofLp)) x All goals completed! 🐙 All goals completed! 🐙f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ (x.val 3 0 • fderiv ℝ (fun x => (f (t • x)).ofLp 1) x + (f (t • x)).ofLp 1 • fderiv ℝ (fun x => x.val 3 0) x - (x.val 3 1 • fderiv ℝ (fun x => (f (t • x)).ofLp 0) x + (f (t • x)).ofLp 0 • fderiv ℝ (fun x => x.val 3 1) x)) y = x.val 3 0 * t * ((fderiv ℝ f (t • x)) y).ofLp 1 + (f (t • x)).ofLp 1 * y.val 3 0 - (x.val 3 1 * t * ((fderiv ℝ f (t • x)) y).ofLp 0 + (f (t • x)).ofLp 0 * y.val 3 1) ∨ t = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ Differentiable ℝ f f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ x.val 3 0 * (t * ((fderiv ℝ f (t • x)) y).ofLp 1) + (f (t • x)).ofLp 1 * y.val 3 0 - (x.val 3 1 * (t * ((fderiv ℝ f (t • x)) y).ofLp 0) + (f (t • x)).ofLp 0 * y.val 3 1) = x.val 3 0 * t * ((fderiv ℝ f (t • x)) y).ofLp 1 + (f (t • x)).ofLp 1 * y.val 3 0 - (x.val 3 1 * t * ((fderiv ℝ f (t • x)) y).ofLp 0 + (f (t • x)).ofLp 0 * y.val 3 1) ∨ t = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ Differentiable ℝ f f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ True ∨ t = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ Differentiable ℝ f f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fx:Spacet:ℝy:Spacefderiv_f:∀ (x : Space) (t : ℝ) (y : Space) (i : Fin 3), (fderiv ℝ (fun x => (f (t • x)).ofLp i) x) y = t * ((fderiv ℝ f (t • x)) y).ofLp i⊢ Differentiable ℝ f All goals completed! 🐙f:Space → EuclideanSpace ℝ (Fin 3)hf✝:ContDiff ℝ 1 fy:Spacei:Fin 3hf:Differentiable ℝ f⊢ Continuous fun p => ((fderiv ℝ (fun x => homotopyOperatorIntegrand f x p.2) p.1) y).ofLp i f:Space → EuclideanSpace ℝ (Fin 3)hf✝:ContDiff ℝ 1 fy:Spacehf:Differentiable ℝ f⊢ Continuous fun p => ((fderiv ℝ (fun x => homotopyOperatorIntegrand f x p.2) p.1) y).ofLp ((fun i => i) ⟨0, ⋯⟩)f:Space → EuclideanSpace ℝ (Fin 3)hf✝:ContDiff ℝ 1 fy:Spacehf:Differentiable ℝ f⊢ Continuous fun p => ((fderiv ℝ (fun x => homotopyOperatorIntegrand f x p.2) p.1) y).ofLp ((fun i => i) ⟨1, ⋯⟩)f:Space → EuclideanSpace ℝ (Fin 3)hf✝:ContDiff ℝ 1 fy:Spacehf:Differentiable ℝ f⊢ Continuous fun p => ((fderiv ℝ (fun x => homotopyOperatorIntegrand f x p.2) p.1) y).ofLp ((fun i => i) ⟨2, ⋯⟩) all_goals f:Space → EuclideanSpace ℝ (Fin 3)hf✝:ContDiff ℝ 1 fy:Spacehf:Differentiable ℝ f⊢ Continuous fun p => ((fderiv ℝ (fun x => homotopyOperatorIntegrand f x p.2) p.1) y).ofLp ((fun i => i) ⟨2, ⋯⟩) f:Space → EuclideanSpace ℝ (Fin 3)hf✝:ContDiff ℝ 1 fy:Spacehf:Differentiable ℝ f⊢ Continuous fun p => p.2 * (p.1.val 3 0 * p.2 * ((fderiv ℝ f (p.2 • p.1)) y).ofLp 1 + (f (p.2 • p.1)).ofLp 1 * y.val 3 0 - (p.1.val 3 1 * p.2 * ((fderiv ℝ f (p.2 • p.1)) y).ofLp 0 + (f (p.2 • p.1)).ofLp 0 * y.val 3 1)) All goals completed! 🐙f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝh:t ∈ Set.uIoc 0 1x:Spacehx:x ∈ s x₀hx2:∀ x ∈ s x₀ ×ˢ Set.Icc 0 1, ‖F' x.1 x.2‖ ≤ ‖F' a.1 a.2‖⊢ ‖F' x t‖ ≤ ‖F' a.1 a.2‖ f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝh:t ∈ Set.uIoc 0 1x:Spacehx:x ∈ s x₀hx2:∀ x ∈ s x₀ ×ˢ Set.Icc 0 1, ‖F' x.1 x.2‖ ≤ ‖F' a.1 a.2‖⊢ (x, t) ∈ s x₀ ×ˢ Set.Icc 0 1 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝx:Spacehx:x ∈ s x₀hx2:∀ x ∈ s x₀ ×ˢ Set.Icc 0 1, ‖F' x.1 x.2‖ ≤ ‖F' a.1 a.2‖h:0 < t ∧ t ≤ 1⊢ (x, t) ∈ s x₀ ×ˢ Set.Icc 0 1 All goals completed! 🐙 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ IntervalIntegrable (fun t => ‖F' a.1 a.2‖) volume 0 1 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ Continuous fun t => ‖F' a.1 a.2‖ All goals completed! 🐙 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ ∀ᵐ (t : ℝ), t ∈ Set.uIoc 0 1 → ∀ x ∈ s x₀, HasFDerivAt (fun x => F x t) (F' x t) x f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝ⊢ t ∈ Set.uIoc 0 1 → ∀ x ∈ s x₀, HasFDerivAt (fun x => F x t) (F' x t) x f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝh:t ∈ Set.uIoc 0 1x:Spacehx:x ∈ s x₀⊢ HasFDerivAt (fun x => F x t) (F' x t) x f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝh:t ∈ Set.uIoc 0 1x:Spacehx:x ∈ s x₀⊢ HasFDerivAt (fun x => homotopyOperatorIntegrand f x t) (fderiv ℝ (fun x => homotopyOperatorIntegrand f x t) x) x f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝh:t ∈ Set.uIoc 0 1x:Spacehx:x ∈ s x₀⊢ Differentiable ℝ f exact hf.differentiable (f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fx₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xs:Space → Set Space := fun x₀ => Metric.closedBall x₀ 1a:Space × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) at:ℝh:t ∈ Set.uIoc 0 1x:Spacehx:x ∈ s x₀⊢ 1 ≠ 0 All goals completed! 🐙)f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fi:Fin 3j:Fin 3k:Fin 3m:Fin 3x₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xF'_continuous:Continuous (Function.uncurry F')hfderiv:∀ (x₀ : Space), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, F' x₀ t) x₀F'_apply_apply:∀ (x₀ y : Space) (i : Fin 3), ((∫ (t : ℝ) in 0..1, F' x₀ t) y).ofLp i = ∫ (t : ℝ) in 0..1, ((F' x₀ t) y).ofLp i⊢ IntervalIntegrable (fun t => ((F' x₀ t) (basis i)).ofLp k) volume 0 1f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fi:Fin 3j:Fin 3k:Fin 3m:Fin 3x₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xF'_continuous:Continuous (Function.uncurry F')hfderiv:∀ (x₀ : Space), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, F' x₀ t) x₀F'_apply_apply:∀ (x₀ y : Space) (i : Fin 3), ((∫ (t : ℝ) in 0..1, F' x₀ t) y).ofLp i = ∫ (t : ℝ) in 0..1, ((F' x₀ t) y).ofLp i⊢ IntervalIntegrable (fun t => ((F' x₀ t) (basis j)).ofLp m) volume 0 1 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fi:Fin 3j:Fin 3k:Fin 3m:Fin 3x₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xF'_continuous:Continuous (Function.uncurry F')hfderiv:∀ (x₀ : Space), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, F' x₀ t) x₀F'_apply_apply:∀ (x₀ y : Space) (i : Fin 3), ((∫ (t : ℝ) in 0..1, F' x₀ t) y).ofLp i = ∫ (t : ℝ) in 0..1, ((F' x₀ t) y).ofLp i⊢ IntervalIntegrable (fun t => ((F' x₀ t) (basis i)).ofLp k) volume 0 1 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fi:Fin 3j:Fin 3k:Fin 3m:Fin 3x₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xF'_continuous:Continuous (Function.uncurry F')hfderiv:∀ (x₀ : Space), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, F' x₀ t) x₀F'_apply_apply:∀ (x₀ y : Space) (i : Fin 3), ((∫ (t : ℝ) in 0..1, F' x₀ t) y).ofLp i = ∫ (t : ℝ) in 0..1, ((F' x₀ t) y).ofLp i⊢ Continuous fun t => ((F' x₀ t) (basis i)).ofLp k All goals completed! 🐙 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fi:Fin 3j:Fin 3k:Fin 3m:Fin 3x₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xF'_continuous:Continuous (Function.uncurry F')hfderiv:∀ (x₀ : Space), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, F' x₀ t) x₀F'_apply_apply:∀ (x₀ y : Space) (i : Fin 3), ((∫ (t : ℝ) in 0..1, F' x₀ t) y).ofLp i = ∫ (t : ℝ) in 0..1, ((F' x₀ t) y).ofLp i⊢ IntervalIntegrable (fun t => ((F' x₀ t) (basis j)).ofLp m) volume 0 1 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fi:Fin 3j:Fin 3k:Fin 3m:Fin 3x₀:SpaceF:Space → ℝ → EuclideanSpace ℝ (Fin 3) := homotopyOperatorIntegrand fF':Space → ℝ → Space →L[ℝ] EuclideanSpace ℝ (Fin 3) := fun x t => fderiv ℝ (fun x => F x t) xF'_continuous:Continuous (Function.uncurry F')hfderiv:∀ (x₀ : Space), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, F' x₀ t) x₀F'_apply_apply:∀ (x₀ y : Space) (i : Fin 3), ((∫ (t : ℝ) in 0..1, F' x₀ t) y).ofLp i = ∫ (t : ℝ) in 0..1, ((F' x₀ t) y).ofLp i⊢ Continuous fun t => ((F' x₀ t) (basis j)).ofLp m All goals completed! 🐙f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:∑ i, ((fderiv ℝ f (t • x)) (basis i)).ofLp i = 0⊢ t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2 + (f (t • x)).ofLp 2 - x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1) - t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 - (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2 + (f (t • x)).ofLp 2)) = t * (f (t • x)).ofLp 2 * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp 2 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0⊢ t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2 + (f (t • x)).ofLp 2 - x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1) - t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 - (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2 + (f (t • x)).ofLp 2)) = t * (f (t • x)).ofLp 2 * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp 2 f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2 + (f (t • x)).ofLp 2 - x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1) - t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 - (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2 + (f (t • x)).ofLp 2)) = t * (f (t • x)).ofLp 2 * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp 2 conv_rhs => f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i| t • x f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i| t • ∑ i, (basis.repr x).ofLp i • basis i f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 0 + (f (t • x)).ofLp 0 - x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2) - t * (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 - (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 0 + (f (t • x)).ofLp 0)) = t * (f (t • x)).ofLp 0 * 2 - t * (-(fderiv ℝ f (t • x)) (t • ∑ i, (basis.repr x).ofLp i • basis i)).ofLp 0 linear_combination (norm := f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 0 + (f (t • x)).ofLp 0 - x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2) - t * (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 - (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 0 + (f (t • x)).ofLp 0)) + -t ^ 2 * x.val 3 0 * 0 - (t * (f (t • x)).ofLp 0 * 2 - t * (-(fderiv ℝ f (t • x)) (t • ∑ i, (basis.repr x).ofLp i • basis i)).ofLp 0 + -t ^ 2 * x.val 3 0 * (((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2)) = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 0 + (f (t • x)).ofLp 0 - x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2) - t * (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 - (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 0 + (f (t • x)).ofLp 0)) - (t * (f (t • x)).ofLp 0 * 2 - t * (-(t * (x.val 3 2 * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 0)) + (-(t * (x.val 3 1 * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 0)) + -(t * (x.val 3 0 * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0)))) + -(t ^ 2 * x.val 3 0 * (((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2))) = 0; All goals completed! 🐙}) - t ^ 2 * x 0 * hdiv f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 1 + (f (t • x)).ofLp 1 - x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0) - t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 - (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 1 + (f (t • x)).ofLp 1)) = t * (f (t • x)).ofLp 1 * 2 - t * (-(fderiv ℝ f (t • x)) (t • ∑ i, (basis.repr x).ofLp i • basis i)).ofLp 1 linear_combination (norm := f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 1 + (f (t • x)).ofLp 1 - x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0) - t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 - (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 1 + (f (t • x)).ofLp 1)) + -t ^ 2 * x.val 3 1 * 0 - (t * (f (t • x)).ofLp 1 * 2 - t * (-(fderiv ℝ f (t • x)) (t • ∑ i, (basis.repr x).ofLp i • basis i)).ofLp 1 + -t ^ 2 * x.val 3 1 * (((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2)) = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 1 + (f (t • x)).ofLp 1 - x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0) - t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 - (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 1 + (f (t • x)).ofLp 1)) - (t * (f (t • x)).ofLp 1 * 2 - t * (-(t * (x.val 3 2 * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 1)) + (-(t * (x.val 3 1 * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1)) + -(t * (x.val 3 0 * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 1)))) + -(t ^ 2 * x.val 3 1 * (((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2))) = 0; All goals completed! 🐙}) - t ^ 2 * x 1 * hdiv f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2 + (f (t • x)).ofLp 2 - x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1) - t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 - (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2 + (f (t • x)).ofLp 2)) = t * (f (t • x)).ofLp 2 * 2 - t * (-(fderiv ℝ f (t • x)) (t • ∑ i, (basis.repr x).ofLp i • basis i)).ofLp 2 linear_combination (norm := f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2 + (f (t • x)).ofLp 2 - x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1) - t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 - (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2 + (f (t • x)).ofLp 2)) + -t ^ 2 * x.val 3 2 * 0 - (t * (f (t • x)).ofLp 2 * 2 - t * (-(fderiv ℝ f (t • x)) (t • ∑ i, (basis.repr x).ofLp i • basis i)).ofLp 2 + -t ^ 2 * x.val 3 2 * (((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2)) = 0f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv✝:div f = 0f_differentiable:Differentiable ℝ ffderiv_f_t:∀ (x : Space) (t : ℝ) (i : Fin 3), (fderiv ℝ (fun t => (f (t • x)).ofLp i) t) 1 = ((fderiv ℝ f (t • x)) x).ofLp ihi:∀ (x : Space) (i : Fin 3), ∫ (t : ℝ) in 0..1, t * (f (t • x)).ofLp i * 2 - t * (-(fderiv ℝ f (t • x)) (t • x)).ofLp i = (f x).ofLp ix:Spacet:ℝhdiv:((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2 = 0hx:x = ∑ i, (basis.repr x).ofLp i • basis i⊢ t * (x.val 3 1 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2 + (f (t • x)).ofLp 2 - x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1) - t * (x.val 3 2 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 - (x.val 3 0 * t * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2 + (f (t • x)).ofLp 2)) - (t * (f (t • x)).ofLp 2 * 2 - t * (-(t * (x.val 3 2 * ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2)) + (-(t * (x.val 3 1 * ((fderiv ℝ f (t • x)) (basis 1)).ofLp 2)) + -(t * (x.val 3 0 * ((fderiv ℝ f (t • x)) (basis 0)).ofLp 2)))) + -(t ^ 2 * x.val 3 2 * (((fderiv ℝ f (t • x)) (basis 0)).ofLp 0 + ((fderiv ℝ f (t • x)) (basis 1)).ofLp 1 + ((fderiv ℝ f (t • x)) (basis 2)).ofLp 2))) = 0; All goals completed! 🐙}) - t ^ 2 * x 2 * hdivf:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv:div f = 0⊢ ∃ g, f = -curl g ∧ Differentiable ℝ g f:Space → EuclideanSpace ℝ (Fin 3)hf:ContDiff ℝ 1 fhdiv:div f = 0⊢ (f = -curl fun x => ∫ (t : ℝ) in 0..1, homotopyOperatorIntegrand f x t) ∧ Differentiable ℝ fun x => ∫ (t : ℝ) in 0..1, homotopyOperatorIntegrand f x t All goals completed! 🐙TODO "Generalize the statement that a div-free field is a curl to time-dependent fields."

### A.10. A curl-free field is a gradient

We show that if the curl of a function is zero, then it is equal to the gradient of some function. The key lemma here is Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric, which is a more general version of this result in Mathlib. We turn this here into something more familiar, to the physicists via deriv_comm_of_curl_zero.

f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 2 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 2) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 0 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 0) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':(curl f x).ofLp 2 = 0⊢ deriv 0 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 0) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':deriv 0 (fun x => (f x).ofLp 1) x - deriv 1 (fun x => (f x).ofLp 0) x = 0⊢ deriv 0 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 0) x linear_combination (norm := All goals completed! 🐙) hcurl' f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 0 (fun x => (f x).ofLp 2) x = deriv 2 (fun x => (f x).ofLp 0) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':(curl f x).ofLp 1 = 0⊢ deriv 0 (fun x => (f x).ofLp 2) x = deriv 2 (fun x => (f x).ofLp 0) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':deriv 2 (fun x => (f x).ofLp 0) x - deriv 0 (fun x => (f x).ofLp 2) x = 0⊢ deriv 0 (fun x => (f x).ofLp 2) x = deriv 2 (fun x => (f x).ofLp 0) x linear_combination (norm := All goals completed! 🐙) -hcurl' f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 1 (fun x => (f x).ofLp 0) x = deriv 0 (fun x => (f x).ofLp 1) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':(curl f x).ofLp 2 = 0⊢ deriv 1 (fun x => (f x).ofLp 0) x = deriv 0 (fun x => (f x).ofLp 1) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':deriv 0 (fun x => (f x).ofLp 1) x - deriv 1 (fun x => (f x).ofLp 0) x = 0⊢ deriv 1 (fun x => (f x).ofLp 0) x = deriv 0 (fun x => (f x).ofLp 1) x linear_combination (norm := All goals completed! 🐙) -hcurl' f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 1 (fun x => (f x).ofLp 2) x = deriv 2 (fun x => (f x).ofLp 1) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':(curl f x).ofLp 0 = 0⊢ deriv 1 (fun x => (f x).ofLp 2) x = deriv 2 (fun x => (f x).ofLp 1) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':deriv 1 (fun x => (f x).ofLp 2) x - deriv 2 (fun x => (f x).ofLp 1) x = 0⊢ deriv 1 (fun x => (f x).ofLp 2) x = deriv 2 (fun x => (f x).ofLp 1) x linear_combination (norm := All goals completed! 🐙) hcurl' f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 2 (fun x => (f x).ofLp 0) x = deriv 0 (fun x => (f x).ofLp 2) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':(curl f x).ofLp 1 = 0⊢ deriv 2 (fun x => (f x).ofLp 0) x = deriv 0 (fun x => (f x).ofLp 2) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':deriv 2 (fun x => (f x).ofLp 0) x - deriv 0 (fun x => (f x).ofLp 2) x = 0⊢ deriv 2 (fun x => (f x).ofLp 0) x = deriv 0 (fun x => (f x).ofLp 2) x linear_combination (norm := All goals completed! 🐙) hcurl' f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':∀ (i : Fin 3), (curl f x).ofLp i = 0⊢ deriv 2 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 2) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':(curl f x).ofLp 0 = 0⊢ deriv 2 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 2) x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0x:Spacehcurl':deriv 1 (fun x => (f x).ofLp 2) x - deriv 2 (fun x => (f x).ofLp 1) x = 0⊢ deriv 2 (fun x => (f x).ofLp 1) x = deriv 1 (fun x => (f x).ofLp 2) x linear_combination (norm := All goals completed! 🐙) -hcurl'f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) x⊢ ∃ g, f = ∇ g ∧ Differentiable ℝ g f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) xg:Space → ℝhg:∀ a ∈ s, HasFDerivAt g (ω a) a⊢ ∃ g, f = ∇ g ∧ Differentiable ℝ g f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) xg:Space → ℝhg:∀ a ∈ s, HasFDerivAt g (ω a) a⊢ f = ∇ g ∧ Differentiable ℝ g f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) xg:Space → ℝhg:∀ (a : Space), HasGradientAt g (basis.repr.symm (f a)) a⊢ f = ∇ g ∧ Differentiable ℝ g f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) xg:Space → ℝhg:∀ (a : Space), HasGradientAt g (basis.repr.symm (f a)) a⊢ f = ∇ g f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) xg:Space → ℝhg:∀ (a : Space), HasGradientAt g (basis.repr.symm (f a)) ax:Space⊢ f x = ∇ g x f:Space → EuclideanSpace ℝ (Fin 3)hf:Differentiable ℝ fhcurl:curl f = 0s:Set Space := Set.univhs:Convex ℝ shso:IsOpen sω:Space → Space →L[ℝ] ℝ := fun a => (toDual ℝ Space) (basis.repr.symm (f a))hω:DifferentiableOn ℝ ω shω_fderiv:∀ (a x y : Space), ((fderiv ℝ ω a) x) y = ⟪basis.repr.symm ((fderiv ℝ f a) x), y⟫_ℝhdω:∀ a ∈ s, ∀ (x y : Space), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) xg:Space → ℝx:Spacehg:HasGradientAt g (basis.repr.symm (f x)) x⊢ f x = ∇ g x All goals completed! 🐙

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.

g:Space → ℝhg:Differentiable ℝ ghf:ContDiff ℝ 1 (∇ g)hcurl:curl (∇ g) = 0⊢ ∃ f', Continuous f' ∧ ∀ (x : Space), HasFDerivAt g (f' x) x refine ⟨fun x => ((toDual ℝ Space) (basis.repr.symm (∇ g x))), g:Space → ℝhg:Differentiable ℝ ghf:ContDiff ℝ 1 (∇ g)hcurl:curl (∇ g) = 0⊢ Continuous fun x => (toDual ℝ Space) (basis.repr.symm (∇ g x)) All goals completed! 🐙, fun x => ?_⟩ All goals completed! 🐙
TODO "Generalize the statement that a curl-free field is a gradient to time-dependent fields."

B. The curl on distributions

@[inherit_doc distCurl] macro (name := distCurlNotation) "∇ᵈ" "⨯" f:term:100 : term => `(distCurl $f)

B.1. The components of the curl

lemma distCurl_coord_apply {i : Fin 3} (f : Space →d[ℝ] (EuclideanSpace ℝ (Fin 3))) (η : 𝓢(Space, ℝ)) : (∇ᵈ ⨯ f) η i = - f (SchwartzMap.evalCLM ℝ Space ℝ (basis (i+2)) (fderivCLM ℝ Space ℝ η)) (i+1) + f (SchwartzMap.evalCLM ℝ Space ℝ (basis (i+1)) (fderivCLM ℝ Space ℝ η)) (i+2) := i:Fin 3f:Space→d[ℝ] EuclideanSpace ℝ (Fin 3)η:𝓢(Space, ℝ)⊢ ((distCurl f) η).ofLp i = -(f ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 2))) ((fderivCLM ℝ Space ℝ) η))).ofLp (i + 1) + (f ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 1))) ((fderivCLM ℝ Space ℝ) η))).ofLp (i + 2) All goals completed! 🐙lemma distCurl_apply_one (f : Space →d[ℝ] (EuclideanSpace ℝ (Fin 3))) (η : 𝓢(Space, ℝ)) : (∇ᵈ ⨯ f) η 1 = - f (SchwartzMap.evalCLM ℝ Space ℝ (basis 0) (fderivCLM ℝ Space ℝ η)) 2 + f (SchwartzMap.evalCLM ℝ Space ℝ (basis 2) (fderivCLM ℝ Space ℝ η)) 0 := f:Space→d[ℝ] EuclideanSpace ℝ (Fin 3)η:𝓢(Space, ℝ)⊢ ((distCurl f) η).ofLp 1 = -(f ((SchwartzMap.evalCLM ℝ Space ℝ (basis 0)) ((fderivCLM ℝ Space ℝ) η))).ofLp 2 + (f ((SchwartzMap.evalCLM ℝ Space ℝ (basis 2)) ((fderivCLM ℝ Space ℝ) η))).ofLp 0 All goals completed! 🐙lemma distCurl_apply_two (f : Space →d[ℝ] (EuclideanSpace ℝ (Fin 3))) (η : 𝓢(Space, ℝ)) : (∇ᵈ ⨯ f) η 2 = - f (SchwartzMap.evalCLM ℝ Space ℝ (basis 1) (fderivCLM ℝ Space ℝ η)) 0 + f (SchwartzMap.evalCLM ℝ Space ℝ (basis 0) (fderivCLM ℝ Space ℝ η)) 1 := f:Space→d[ℝ] EuclideanSpace ℝ (Fin 3)η:𝓢(Space, ℝ)⊢ ((distCurl f) η).ofLp 2 = -(f ((SchwartzMap.evalCLM ℝ Space ℝ (basis 1)) ((fderivCLM ℝ Space ℝ) η))).ofLp 0 + (f ((SchwartzMap.evalCLM ℝ Space ℝ (basis 0)) ((fderivCLM ℝ Space ℝ) η))).ofLp 1 All goals completed! 🐙

B.2. Basic equalities

lemma distCurl_apply (f : Space →d[ℝ] (EuclideanSpace ℝ (Fin 3))) (η : 𝓢(Space, ℝ)) : (∇ᵈ ⨯ f) η = WithLp.toLp 2 fun i => - f (SchwartzMap.evalCLM ℝ Space ℝ (basis (i+2)) (fderivCLM ℝ Space ℝ η)) (i+1) + f (SchwartzMap.evalCLM ℝ Space ℝ (basis (i+1)) (fderivCLM ℝ Space ℝ η)) (i+2) := f:Space→d[ℝ] EuclideanSpace ℝ (Fin 3)η:𝓢(Space, ℝ)⊢ (distCurl f) η = WithLp.toLp 2 fun i => -(f ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 2))) ((fderivCLM ℝ Space ℝ) η))).ofLp (i + 1) + (f ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 1))) ((fderivCLM ℝ Space ℝ) η))).ofLp (i + 2) f:Space→d[ℝ] EuclideanSpace ℝ (Fin 3)η:𝓢(Space, ℝ)i:Fin 3⊢ ((distCurl f) η).ofLp i = (WithLp.toLp 2 fun i => -(f ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 2))) ((fderivCLM ℝ Space ℝ) η))).ofLp (i + 1) + (f ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 1))) ((fderivCLM ℝ Space ℝ) η))).ofLp (i + 2)).ofLp i All goals completed! 🐙

B.3. The curl of a grad is zero

The curl of a grad is equal to zero.

f:Space→d[ℝ] ℝη:𝓢(Space, ℝ)i:Fin 3x:Space⊢ ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 2))) ((fderivCLM ℝ Space ℝ) ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 1))) ((fderivCLM ℝ Space ℝ) η)))) x + -((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 2))) ((fderivCLM ℝ Space ℝ) ((SchwartzMap.evalCLM ℝ Space ℝ (basis (i + 1))) ((fderivCLM ℝ Space ℝ) η)))) x = 0 All goals completed! 🐙