Physlib.Mathematics.Calculus.Divergence

Imports

/-
Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
module

public import Mathlib.LinearAlgebra.Trace
public import Physlib.Mathematics.Calculus.AdjFDeriv
public import Physlib.SpaceAndTime.Space.Derivatives.Div

Divergence

In this module we define and create an API around the divergence of a map f : E → E where E is a normed space over a field 𝕜.

              @[expose] public section@[simp]
lemma divergence_zero : divergence 𝕜 (fun _ : E => 0) = fun _ => 0 := by𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 E⊢ (divergence 𝕜 fun x => 0) = fun x => 0
  unfold divergence𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 E⊢ (fun x => (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 (fun x => 0) x)) = fun x => 0
  simpAll goals completed! 🐙

lemma divergence_eq_sum_fderiv {s : Finset E} (b : Basis s 𝕜 E) {f : E → E} :
    divergence 𝕜 f = fun x => ∑ i : s, b.repr (fderiv 𝕜 f x (b i)) i := by𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → E⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  funext x𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → Ex:E⊢ divergence 𝕜 f x = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  unfold divergence𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → Ex:E⊢ (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 f x) = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  rw[LinearMap.trace_eq_matrix_trace_of_finset (s:=s) _ b𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → Ex:E⊢ ((LinearMap.toMatrix b b) ↑(fderiv 𝕜 f x)).trace = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → Ex:E⊢ ((LinearMap.toMatrix b b) ↑(fderiv 𝕜 f x)).trace = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i]𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → Ex:E⊢ ((LinearMap.toMatrix b b) ↑(fderiv 𝕜 f x)).trace = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  simp only [Matrix.trace, Matrix.diag, LinearMap.toMatrix_apply]𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Es:Finset Eb:Basis (↥s) 𝕜 Ef:E → Ex:E⊢ ∑ x_1, (b.repr (↑(fderiv 𝕜 f x) (b x_1))) x_1 = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  rflAll goals completed! 🐙

lemma divergence_eq_sum_fderiv' {ι} [Fintype ι] (b : Basis ι 𝕜 E) {f : E → E} :
    divergence 𝕜 f = fun x => ∑ i, b.repr (fderiv 𝕜 f x (b i)) i := by𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → E⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  let s : Finset E := Finset.univ.map ⟨b, Basis.injective b⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univ⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  let f' : ι → s := fun i => ⟨b i, by𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univi:ι⊢ b i ∈ s𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i simp [s]All goals completed! 🐙𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  have h : Function.Injective f' := by
    intro i j h𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩i:ιj:ιh:f' i = f' j⊢ i = j𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
    simp [f'] at h𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩i:ιj:ιh:b i = b j⊢ i = j𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
    exact Basis.injective b h𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  have h' : Function.Surjective f' := by
    intro ⟨x, hx⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'x:Ehx:x ∈ s⊢ ∃ a, f' a = ⟨x, hx⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
    simp [s] at hx𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'x:Ehx✝:x ∈ shx:∃ a, b a = x⊢ ∃ a, f' a = ⟨x, hx⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
    obtain ⟨i, rfl⟩ := hx𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'i:ιhx:b i ∈ s⊢ ∃ a, f' a = ⟨b i, hx⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
    simp [f']𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  let e : ι ≃ s := Equiv.ofBijective f' ⟨h, h'⟩𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  let b' : Basis s 𝕜 E := b.reindex e𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex e⊢ divergence 𝕜 f = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  rw [divergence_eq_sum_fderiv b'𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex e⊢ (fun x => ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i) = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex e⊢ (fun x => ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i) = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i]𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex e⊢ (fun x => ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i) = fun x => ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  ext x𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex ex:E⊢ ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i = ∑ i, (b.repr ((fderiv 𝕜 f x) (b i))) i
  rw [← e.symm.sum_comp𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex ex:E⊢ ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i = ∑ i, (b.repr ((fderiv 𝕜 f x) (b (e.symm i)))) (e.symm i)𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex ex:E⊢ ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i = ∑ i, (b.repr ((fderiv 𝕜 f x) (b (e.symm i)))) (e.symm i)]𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Eι:Type u_4inst✝:Fintype ιb:Basis ι 𝕜 Ef:E → Es:Finset E := Finset.map { toFun := ⇑b, inj' := ⋯ } Finset.univf':ι → ↥s := fun i => ⟨b i, ⋯⟩h:Function.Injective f'h':Function.Surjective f'e:ι ≃ ↥s := Equiv.ofBijective f' ⋯b':Basis (↥s) 𝕜 E := b.reindex ex:E⊢ ∑ i, (b'.repr ((fderiv 𝕜 f x) (b' i))) i = ∑ i, (b.repr ((fderiv 𝕜 f x) (b (e.symm i)))) (e.symm i)
  simp [b']All goals completed! 🐙

lemma divergence_eq_space_div {d} (f : Space d → Space d)
    (h : Differentiable ℝ f) : divergence ℝ f = Space.div (Space.basis.repr ∘ f) := byd:ℕf:Space d → Space dh:Differentiable ℝ f⊢ divergence ℝ f = Space.div (⇑Space.basis.repr ∘ f)
  let b := (Space.basis (d:=d)).toBasisd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasis⊢ divergence ℝ f = Space.div (⇑Space.basis.repr ∘ f)
  rw[divergence_eq_sum_fderiv' bd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasis⊢ (fun x => ∑ i, (b.repr ((fderiv ℝ f x) (b i))) i) = Space.div (⇑Space.basis.repr ∘ f)d:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasis⊢ (fun x => ∑ i, (b.repr ((fderiv ℝ f x) (b i))) i) = Space.div (⇑Space.basis.repr ∘ f)]d:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasis⊢ (fun x => ∑ i, (b.repr ((fderiv ℝ f x) (b i))) i) = Space.div (⇑Space.basis.repr ∘ f)
  funext xd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space d⊢ ∑ i, (b.repr ((fderiv ℝ f x) (b i))) i = Space.div (⇑Space.basis.repr ∘ f) x
  simp +zetaDelta only [OrthonormalBasis.coe_toBasis, OrthonormalBasis.coe_toBasis_repr_apply,
    Space.basis_repr_apply, Space.div, Space.deriv, Function.comp_apply]d:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space d⊢ ∑ x_1, ((fderiv ℝ f x) (Space.basis x_1)).val x_1 = ∑ x_1, (fderiv ℝ (fun x => (f x).val x_1) x) (Space.basis x_1)
  congre_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space d⊢ (fun x_1 => ((fderiv ℝ f x) (Space.basis x_1)).val x_1) = fun x_1 =>
  (fderiv ℝ (fun x => (f x).val x_1) x) (Space.basis x_1)
  funext ie_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin d⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)
  have h1 : (fderiv ℝ (fun x => f x i) x)
    = fderiv ℝ (Space.coordCLM i ∘ f) x := byd:ℕf:Space d → Space dh:Differentiable ℝ f⊢ divergence ℝ f = Space.div (⇑Space.basis.repr ∘ f)e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)
    congre_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin d⊢ (fun x => (f x).val i) = ⇑(Space.coordCLM i) ∘ fe_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)
    ext je_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dj:Space d⊢ (f j).val i = (⇑(Space.coordCLM i) ∘ f) je_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)
    simp only [Function.comp_apply]e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dj:Space d⊢ (f j).val i = (Space.coordCLM i) (f j)e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)
    rw [Space.coordCLM_apply,e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dj:Space d⊢ (f j).val i = Space.coord i (f j)e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i) Space.coord_applye_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dj:Space d⊢ (f j).val i = (f j).val ie_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)]e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (fun x => (f x).val i) x) (Space.basis i)
  rw [h1e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x) (Space.basis i)e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x) (Space.basis i)]e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x) (Space.basis i)
  rw [fderiv_compe_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (⇑(Space.coordCLM i)) (f x) ∘SL fderiv ℝ f x) (Space.basis i)e_f.hgd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ (⇑(Space.coordCLM i)) (f x)e_f.hfd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ f xe_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (⇑(Space.coordCLM i)) (f x) ∘SL fderiv ℝ f x) (Space.basis i)e_f.hgd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ (⇑(Space.coordCLM i)) (f x)e_f.hfd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ f x]e_fd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ ((fderiv ℝ f x) (Space.basis i)).val i = (fderiv ℝ (⇑(Space.coordCLM i)) (f x) ∘SL fderiv ℝ f x) (Space.basis i)e_f.hgd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ (⇑(Space.coordCLM i)) (f x)e_f.hfd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ f x
  simp [Space.coordCLM_apply, Space.coord_apply]e_f.hgd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ (⇑(Space.coordCLM i)) (f x)e_f.hfd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ f x
  ·e_f.hgd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ (⇑(Space.coordCLM i)) (f x) fun_propAll goals completed! 🐙
  ·e_f.hfd:ℕf:Space d → Space dh:Differentiable ℝ fb:Basis (Fin d) ℝ (Space d) := Space.basis.toBasisx:Space di:Fin dh1:fderiv ℝ (fun x => (f x).val i) x = fderiv ℝ (⇑(Space.coordCLM i) ∘ f) x⊢ DifferentiableAt ℝ f x exact h xAll goals completed! 🐙

lemma divergence_prodMk [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F]
    {f : E×F → E} {g : E×F → F} {xy : E×F}
    (hf : DifferentiableAt 𝕜 f xy) (hg : DifferentiableAt 𝕜 g xy) :
    divergence 𝕜 (fun xy : E×F => (f xy, g xy)) xy
    =
    divergence 𝕜 (fun x' => f (x',xy.2)) xy.1
    +
    divergence 𝕜 (fun y' => g (xy.1,y')) xy.2 := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xy⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  divergence 𝕜 (fun x' => f (x', xy.2)) xy.1 + divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  obtain ⟨s, ⟨bX⟩⟩ := Basis.exists_basis 𝕜 E𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 E⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  divergence 𝕜 (fun x' => f (x', xy.2)) xy.1 + divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  haveI : Fintype s := FiniteDimensional.fintypeBasisIndex bX𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis:Fintype ↑s⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  divergence 𝕜 (fun x' => f (x', xy.2)) xy.1 + divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  obtain ⟨sY, ⟨bY⟩⟩ := Basis.exists_basis 𝕜 F𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 F⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  divergence 𝕜 (fun x' => f (x', xy.2)) xy.1 + divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  haveI : Fintype sY := FiniteDimensional.fintypeBasisIndex bY𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  divergence 𝕜 (fun x' => f (x', xy.2)) xy.1 + divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  let bXY := bX.prod bY𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  divergence 𝕜 (fun x' => f (x', xy.2)) xy.1 + divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  rw[divergence_eq_sum_fderiv' bX𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    divergence 𝕜 (fun y' => g (xy.1, y')) xy.2𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    divergence 𝕜 (fun y' => g (xy.1, y')) xy.2]𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    divergence 𝕜 (fun y' => g (xy.1, y')) xy.2
  rw[divergence_eq_sum_fderiv' bY𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    (fun x => ∑ i, (bY.repr ((fderiv 𝕜 (fun y' => g (xy.1, y')) x) (bY i))) i) xy.2𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    (fun x => ∑ i, (bY.repr ((fderiv 𝕜 (fun y' => g (xy.1, y')) x) (bY i))) i) xy.2]𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ divergence 𝕜 (fun xy => (f xy, g xy)) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    (fun x => ∑ i, (bY.repr ((fderiv 𝕜 (fun y' => g (xy.1, y')) x) (bY i))) i) xy.2
  rw[divergence_eq_sum_fderiv' bXY𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ (fun x => ∑ i, (bXY.repr ((fderiv 𝕜 (fun xy => (f xy, g xy)) x) (bXY i))) i) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    (fun x => ∑ i, (bY.repr ((fderiv 𝕜 (fun y' => g (xy.1, y')) x) (bY i))) i) xy.2𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ (fun x => ∑ i, (bXY.repr ((fderiv 𝕜 (fun xy => (f xy, g xy)) x) (bXY i))) i) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    (fun x => ∑ i, (bY.repr ((fderiv 𝕜 (fun y' => g (xy.1, y')) x) (bY i))) i) xy.2]𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 EF:Type u_3inst✝³:NormedAddCommGroup Finst✝²:NormedSpace 𝕜 Finst✝¹:FiniteDimensional 𝕜 Einst✝:FiniteDimensional 𝕜 Ff:E × F → Eg:E × F → Fxy:E × Fhf:DifferentiableAt 𝕜 f xyhg:DifferentiableAt 𝕜 g xys:Set EbX:Basis (↑s) 𝕜 Ethis✝:Fintype ↑ssY:Set FbY:Basis (↑sY) 𝕜 Fthis:Fintype ↑sYbXY:Basis (↑s ⊕ ↑sY) 𝕜 (E × F) := bX.prod bY⊢ (fun x => ∑ i, (bXY.repr ((fderiv 𝕜 (fun xy => (f xy, g xy)) x) (bXY i))) i) xy =
  (fun x => ∑ i, (bX.repr ((fderiv 𝕜 (fun x' => f (x', xy.2)) x) (bX i))) i) xy.1 +
    (fun x => ∑ i, (bY.repr ((fderiv 𝕜 (fun y' => g (xy.1, y')) x) (bY i))) i) xy.2
  simp[hf.fderiv_prodMk hg,bXY,fderiv_wrt_prod hf,fderiv_wrt_prod hg]All goals completed! 🐙lemma divergence_add {f g : E → E} {x : E}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    divergence 𝕜 (fun x => f x + g x) x
    =
    divergence 𝕜 f x + divergence 𝕜 g x := by𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Eg:E → Ex:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ divergence 𝕜 (fun x => f x + g x) x = divergence 𝕜 f x + divergence 𝕜 g x
  unfold divergence𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Eg:E → Ex:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 (fun x => f x + g x) x) =
  (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 f x) + (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 g x)
  simp [fderiv_fun_add hf hg]All goals completed! 🐙lemma divergence_neg {f : E → E} {x : E} :
    divergence 𝕜 (fun x => -f x) x = -divergence 𝕜 f x := by𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Ex:E⊢ divergence 𝕜 (fun x => -f x) x = -divergence 𝕜 f x
  unfold divergence𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Ex:E⊢ (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 (fun x => -f x) x) = -(LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 f x)
  simpAll goals completed! 🐙lemma divergence_sub {f g : E → E} {x : E}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    divergence 𝕜 (fun x => f x - g x) x
    =
    divergence 𝕜 f x - divergence 𝕜 g x := by𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Eg:E → Ex:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ divergence 𝕜 (fun x => f x - g x) x = divergence 𝕜 f x - divergence 𝕜 g x
  unfold divergence𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Eg:E → Ex:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 (fun x => f x - g x) x) =
  (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 f x) - (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 g x)
  simp [fderiv_fun_sub hf hg]All goals completed! 🐙lemma divergence_const_smul {f : E → E} {x : E} {c : 𝕜}
    (hf : DifferentiableAt 𝕜 f x) :
    divergence 𝕜 (fun x => c • f x) x
    =
    c * divergence 𝕜 f x := by𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Ex:Ec:𝕜hf:DifferentiableAt 𝕜 f x⊢ divergence 𝕜 (fun x => c • f x) x = c * divergence 𝕜 f x
  unfold divergence𝕜:Type u_1inst✝²:RCLike 𝕜E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace 𝕜 Ef:E → Ex:Ec:𝕜hf:DifferentiableAt 𝕜 f x⊢ (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 (fun x => c • f x) x) = c * (LinearMap.trace 𝕜 E) ↑(fderiv 𝕜 f x)
  simp [fderiv_fun_const_smul hf]All goals completed! 🐙