Physlib.SpaceAndTime.Space.Derivatives.Div — Physlib

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.Grad
public import Physlib.SpaceAndTime.Space.DistOfFunction

Divergence on Space

i. Overview

In this module we define the divergence operator on functions and distributions from Space d to EuclideanSpace ℝ (Fin d), and prove various basic properties about it.

ii. Key results

div : The divergence operator on functions from Space d to EuclideanSpace ℝ (Fin d).

distDiv : The divergence operator on distributions from Space d to EuclideanSpace ℝ (Fin d).

distDiv_ofFunction : The divergence of a distribution from a bounded function.

iii. Table of contents

A. The divergence on functions

A.1. The divergence on the zero function

A.2. The divergence on a constant function

A.3. The divergence distributes over addition

A.4. The divergence distributes over scalar multiplication

A.5. The divergence of a linear map is a linear map

B. Divergence of distributions

B.1. Basic equalities

B.2. Divergence on distributions from bounded functions

iv. References

@[expose] public section

A. The divergence on functions

@[inherit_doc div]
macro (name := divNotation) "∇" "⬝" f:term:100 : term => `(div $f)



lemma div_eq_sum_fderiv {d} (f : Space d → EuclideanSpace ℝ (Fin d))
    (hf : Differentiable ℝ f) (x : Space d) :
    (∇ ⬝ f) x = ∑ i, fderiv ℝ f x (basis i) i := byd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space d⊢ div f x = ∑ i, ((fderiv ℝ f x) (basis i)).ofLp i
  simp [div, Space.deriv]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space d⊢ ∑ x_1, (fderiv ℝ (fun x => (f x).ofLp x_1) x) (basis x_1) = ∑ x_1, ((fderiv ℝ f x) (basis x_1)).ofLp x_1
  congre_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space d⊢ (fun x_1 => (fderiv ℝ (fun x => (f x).ofLp x_1) x) (basis x_1)) = fun x_1 => ((fderiv ℝ f x) (basis x_1)).ofLp x_1
  funext ie_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ (fderiv ℝ (fun x => (f x).ofLp i) x) (basis i) = ((fderiv ℝ f x) (basis i)).ofLp i
  rw [← Space.deriv_eqe_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ deriv i (fun x => (f x).ofLp i) x = ((fderiv ℝ f x) (basis i)).ofLp ie_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ deriv i (fun x => (f x).ofLp i) x = ((fderiv ℝ f x) (basis i)).ofLp i]e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ deriv i (fun x => (f x).ofLp i) x = ((fderiv ℝ f x) (basis i)).ofLp i
  rw [deriv_euclide_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ (deriv i (fun x => f x) x).ofLp i = ((fderiv ℝ f x) (basis i)).ofLp ie_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ Differentiable ℝ fe_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ (deriv i (fun x => f x) x).ofLp i = ((fderiv ℝ f x) (basis i)).ofLp ie_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ Differentiable ℝ f]e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ (deriv i (fun x => f x) x).ofLp i = ((fderiv ℝ f x) (basis i)).ofLp ie_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ Differentiable ℝ f
  rfle_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:Differentiable ℝ fx:Space di:Fin d⊢ Differentiable ℝ f
  fun_propAll goals completed! 🐙

A.1. The divergence on the zero function

@[simp]
lemma div_zero : ∇ ⬝ (0 : Space d → EuclideanSpace ℝ (Fin d)) = 0 := byd:ℕ⊢ div 0 = 0
  unfold div Space.deriv Finset.sumd:ℕ⊢ (fun x => (Multiset.map (fun i => (fderiv ℝ (fun x => (0 x).ofLp i) x) (basis i)) Finset.univ.val).sum) = 0
  simp only [Pi.ofNat_apply, fderiv_fun_const, _root_.zero_apply, Multiset.map_const',
    Finset.card_val, Finset.card_univ, Fintype.card_fin, Multiset.sum_replicate, smul_zero]d:ℕ⊢ (fun x => 0) = 0
  rflAll goals completed! 🐙

A.2. The divergence on a constant function

@[simp]
lemma div_const : ∇ ⬝ (fun _ : Space d => v) = 0 := byd:ℕv:EuclideanSpace ℝ (Fin d)⊢ (div fun x => v) = 0
  unfold div Space.deriv Finset.sumd:ℕv:EuclideanSpace ℝ (Fin d)⊢ (fun x => (Multiset.map (fun i => (fderiv ℝ (fun x => ((fun x => v) x).ofLp i) x) (basis i)) Finset.univ.val).sum) = 0
  simp only [fderiv_fun_const, Pi.ofNat_apply, _root_.zero_apply, Multiset.map_const',
    Finset.card_val, Finset.card_univ, Fintype.card_fin, Multiset.sum_replicate, smul_zero]d:ℕv:EuclideanSpace ℝ (Fin d)⊢ (fun x => 0) = 0
  rflAll goals completed! 🐙

A.3. The divergence distributes over addition



lemma div_add (f1 f2 : Space d → EuclideanSpace ℝ (Fin d))
    (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) :
    ∇ ⬝ (f1 + f2) = ∇ ⬝ f1 + ∇ ⬝ f2 := byd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ div (f1 + f2) = div f1 + div f2
  unfold divd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ (fun x => ∑ i, deriv i (fun x => ((f1 + f2) x).ofLp i) x) =
  (fun x => ∑ i, deriv i (fun x => (f1 x).ofLp i) x) + fun x => ∑ i, deriv i (fun x => (f2 x).ofLp i) x
  simp only [Pi.add_apply]d:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ (fun x => ∑ x_1, deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x) =
  (fun x => ∑ x_1, deriv x_1 (fun x => (f1 x).ofLp x_1) x) + fun x => ∑ x_1, deriv x_1 (fun x => (f2 x).ofLp x_1) x
  funext xd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ ∑ x_1, deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x =
  ((fun x => ∑ x_1, deriv x_1 (fun x => (f1 x).ofLp x_1) x) + fun x => ∑ x_1, deriv x_1 (fun x => (f2 x).ofLp x_1) x) x
  simp only [Pi.add_apply]d:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ ∑ x_1, deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x =
  ∑ x_1, deriv x_1 (fun x => (f1 x).ofLp x_1) x + ∑ x_1, deriv x_1 (fun x => (f2 x).ofLp x_1) x
  rw [← Finset.sum_add_distribd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ ∑ x_1, deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x =
  ∑ x_1, (deriv x_1 (fun x => (f1 x).ofLp x_1) x + deriv x_1 (fun x => (f2 x).ofLp x_1) x)d:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ ∑ x_1, deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x =
  ∑ x_1, (deriv x_1 (fun x => (f1 x).ofLp x_1) x + deriv x_1 (fun x => (f2 x).ofLp x_1) x)]d:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ ∑ x_1, deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x =
  ∑ x_1, (deriv x_1 (fun x => (f1 x).ofLp x_1) x + deriv x_1 (fun x => (f2 x).ofLp x_1) x)
  congre_fd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space d⊢ (fun x_1 => deriv x_1 (fun x => (f1 x + f2 x).ofLp x_1) x) = fun x_1 =>
  deriv x_1 (fun x => (f1 x).ofLp x_1) x + deriv x_1 (fun x => (f2 x).ofLp x_1) x
  funext ie_fd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ deriv i (fun x => (f1 x + f2 x).ofLp i) x = deriv i (fun x => (f1 x).ofLp i) x + deriv i (fun x => (f2 x).ofLp i) x
  simp [Space.deriv]e_fd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (fderiv ℝ (fun x => (f1 x).ofLp i + (f2 x).ofLp i) x) (basis i) =
  (fderiv ℝ (fun x => (f1 x).ofLp i) x) (basis i) + (fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i)
  rw [fderiv_fun_adde_fd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (fderiv ℝ (fun x => (f1 x).ofLp i) x + fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i) =
  (fderiv ℝ (fun x => (f1 x).ofLp i) x) (basis i) + (fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i)e_f.hfd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f1 x).ofLp i) xe_f.hgd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f2 x).ofLp i) xe_fd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (fderiv ℝ (fun x => (f1 x).ofLp i) x + fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i) =
  (fderiv ℝ (fun x => (f1 x).ofLp i) x) (basis i) + (fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i)e_f.hfd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f1 x).ofLp i) xe_f.hgd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f2 x).ofLp i) x]e_fd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (fderiv ℝ (fun x => (f1 x).ofLp i) x + fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i) =
  (fderiv ℝ (fun x => (f1 x).ofLp i) x) (basis i) + (fderiv ℝ (fun x => (f2 x).ofLp i) x) (basis i)e_f.hfd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f1 x).ofLp i) xe_f.hgd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f2 x).ofLp i) x
  simp only [_root_.add_apply]e_f.hfd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f1 x).ofLp i) xe_f.hgd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f2 x).ofLp i) x
  ·e_f.hfd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f1 x).ofLp i) x fun_propAll goals completed! 🐙
  ·e_f.hgd:ℕf1:Space d → EuclideanSpace ℝ (Fin d)f2:Space d → EuclideanSpace ℝ (Fin d)hf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f2 x).ofLp i) x fun_propAll goals completed! 🐙

A.4. The divergence distributes over scalar multiplication



lemma div_smul (f : Space d → EuclideanSpace ℝ (Fin d)) (k : ℝ)
    (hf : Differentiable ℝ f) :
    ∇ ⬝ (k • f) = k • ∇ ⬝ f := byd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ div (k • f) = k • div f
  unfold divd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (fun x => ∑ i, deriv i (fun x => ((k • f) x).ofLp i) x) = k • fun x => ∑ i, deriv i (fun x => (f x).ofLp i) x
  simp only [Pi.smul_apply]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ f⊢ (fun x => ∑ x_1, deriv x_1 (fun x => (k • f x).ofLp x_1) x) = k • fun x => ∑ x_1, deriv x_1 (fun x => (f x).ofLp x_1) x
  funext xd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space d⊢ ∑ x_1, deriv x_1 (fun x => (k • f x).ofLp x_1) x = (k • fun x => ∑ x_1, deriv x_1 (fun x => (f x).ofLp x_1) x) x
  simp only [Pi.smul_apply, smul_eq_mul]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space d⊢ ∑ x_1, deriv x_1 (fun x => (k • f x).ofLp x_1) x = k * ∑ x_1, deriv x_1 (fun x => (f x).ofLp x_1) x
  rw [Finset.mul_sumd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space d⊢ ∑ x_1, deriv x_1 (fun x => (k • f x).ofLp x_1) x = ∑ i, k * deriv i (fun x => (f x).ofLp i) xd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space d⊢ ∑ x_1, deriv x_1 (fun x => (k • f x).ofLp x_1) x = ∑ i, k * deriv i (fun x => (f x).ofLp i) x]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space d⊢ ∑ x_1, deriv x_1 (fun x => (k • f x).ofLp x_1) x = ∑ i, k * deriv i (fun x => (f x).ofLp i) x
  congre_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space d⊢ (fun x_1 => deriv x_1 (fun x => (k • f x).ofLp x_1) x) = fun i => k * deriv i (fun x => (f x).ofLp i) x
  funext ie_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ deriv i (fun x => (k • f x).ofLp i) x = k * deriv i (fun x => (f x).ofLp i) x
  simp [Space.deriv]e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (fderiv ℝ (fun x => k * (f x).ofLp i) x) (basis i) = k * (fderiv ℝ (fun x => (f x).ofLp i) x) (basis i)
  rw [fderiv_const_mule_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (k • fderiv ℝ (fun x => (f x).ofLp i) x) (basis i) = k * (fderiv ℝ (fun x => (f x).ofLp i) x) (basis i)e_f.had:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f x).ofLp i) xe_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (k • fderiv ℝ (fun x => (f x).ofLp i) x) (basis i) = k * (fderiv ℝ (fun x => (f x).ofLp i) x) (basis i)e_f.had:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f x).ofLp i) x]e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (k • fderiv ℝ (fun x => (f x).ofLp i) x) (basis i) = k * (fderiv ℝ (fun x => (f x).ofLp i) x) (basis i)e_f.had:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f x).ofLp i) x
  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]e_f.had:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f x).ofLp i) x
  ·e_f.had:ℕf:Space d → EuclideanSpace ℝ (Fin d)k:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ DifferentiableAt ℝ (fun x => (f x).ofLp i) x fun_propAll goals completed! 🐙

A.5. The divergence of a linear map is a linear map



lemma div_linear_map (f : W → Space 3 → EuclideanSpace ℝ (Fin 3))
    (hf : ∀ w, Differentiable ℝ (f w))
    (hf' : IsLinearMap ℝ f) :
    IsLinearMap ℝ (fun w => ∇ ⬝ (f w)) := byW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ f⊢ IsLinearMap ℝ fun w => div (f w)
  constructormap_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ f⊢ ∀ (x y : W), div (f (x + y)) = div (f x) + div (f y)map_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ f⊢ ∀ (c : ℝ) (x : W), div (f (c • x)) = c • div (f x)
  ·map_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ f⊢ ∀ (x y : W), div (f (x + y)) = div (f x) + div (f y) intro w w'map_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ div (f (w + w')) = div (f w) + div (f w')
    rw [hf'.map_addmap_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ div (f w + f w') = div (f w) + div (f w')map_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ div (f w + f w') = div (f w) + div (f w')]map_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ div (f w + f w') = div (f w) + div (f w')
    rw [div_addmap_addW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ div (f w) + div (f w') = div (f w) + div (f w')map_add.hf1W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ Differentiable ℝ (f w)map_add.hf2W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ Differentiable ℝ (f w')map_add.hf1W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ Differentiable ℝ (f w)map_add.hf2W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ Differentiable ℝ (f w')]map_add.hf1W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ Differentiable ℝ (f w)map_add.hf2W:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fw:Ww':W⊢ Differentiable ℝ (f w')
    repeat fun_propAll goals completed! 🐙
  ·map_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ f⊢ ∀ (c : ℝ) (x : W), div (f (c • x)) = c • div (f x) intros k wmap_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fk:ℝw:W⊢ div (f (k • w)) = k • div (f w)
    rw [hf'.map_smulmap_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fk:ℝw:W⊢ div (k • f w) = k • div (f w)map_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fk:ℝw:W⊢ div (k • f w) = k • div (f w)]map_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fk:ℝw:W⊢ div (k • f w) = k • div (f w)
    rw [div_smulmap_smulW:Type u_1inst✝¹:NormedAddCommGroup Winst✝:NormedSpace ℝ Wf:W → Space → EuclideanSpace ℝ (Fin 3)hf:∀ (w : W), Differentiable ℝ (f w)hf':IsLinearMap ℝ fk:ℝw:W⊢ k • div (f w) = k • div (f w)map_smul.hfW: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)map_smul.hfW: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)]map_smul.hfW: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)
    fun_propAll goals completed! 🐙

B. Divergence of distributions

@[inherit_doc distDiv]
macro (name := distDivNotation) "∇ᵈ" "⬝" f:term:100 : term => `(distDiv $f)

B.1. Basic equalities

lemma distDiv_apply_eq_sum_fderivD {d}
    (f : (Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) (η : 𝓢(Space d, ℝ)) :
    (∇ᵈ ⬝ f) η = ∑ i, fderivD ℝ f η (basis i) i := byd:ℕf:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ (distDiv f) η = ∑ i, ((((fderivD ℝ) f) η) (basis i)).ofLp i
  simp [distDiv, EuclideanSpace.inner_single_right]All goals completed! 🐙



lemma distDiv_apply_eq_sum_distDeriv {d}
    (f : (Space d) →d[ℝ] EuclideanSpace ℝ (Fin d)) (η : 𝓢(Space d, ℝ)) :
    (∇ᵈ ⬝ f) η = ∑ i, ∂ᵈ[i] f η i := byd:ℕf:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ (distDiv f) η = ∑ i, (((distDeriv i) f) η).ofLp i
  rw [distDiv_apply_eq_sum_fderivDd:ℕf:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) f) η) (basis i)).ofLp i = ∑ i, (((distDeriv i) f) η).ofLp id:ℕf:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) f) η) (basis i)).ofLp i = ∑ i, (((distDeriv i) f) η).ofLp i]d:ℕf:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)η:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) f) η) (basis i)).ofLp i = ∑ i, (((distDeriv i) f) η).ofLp i
  rflAll goals completed! 🐙

B.2. Divergence on distributions from bounded functions

The divergence of a distribution from a bounded function.


lemma distDiv_ofFunction {d : ℕ} {f : Space d → EuclideanSpace ℝ (Fin d)}
    {hf : IsDistBounded f} (η : 𝓢(Space d, ℝ)) :
    (∇ᵈ ⬝ (distOfFunction f hf)) η =
    - ∫ x : Space d, ⟪f x, ∇ η x⟫_ℝ := byd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ (distDiv (distOfFunction f hf)) η = -∫ (x : Space d), ⟪f x, ∇ (⇑η) x⟫_ℝ
  rw [distDiv_apply_eq_sum_fderivDd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) (distOfFunction f hf)) η) (basis i)).ofLp i = -∫ (x : Space d), ⟪f x, ∇ (⇑η) x⟫_ℝd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) (distOfFunction f hf)) η) (basis i)).ofLp i = -∫ (x : Space d), ⟪f x, ∇ (⇑η) x⟫_ℝ]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∑ i, ((((fderivD ℝ) (distOfFunction f hf)) η) (basis i)).ofLp i = -∫ (x : Space d), ⟪f x, ∇ (⇑η) x⟫_ℝ
  conv_rhs =>
    enter [1, 2, x]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)x:Space d| ⟪f x, ∇ (⇑η) x⟫_ℝ
    rw [grad_eq_sum, inner_sum]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)x:Space d| ∑ i, ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ
  conv_lhs =>
    enter [2, i]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin d| ((((fderivD ℝ) (distOfFunction f hf)) η) (basis i)).ofLp i
    rw [fderivD_apply, distOfFunction_apply]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin d| (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i
  /- The following lemma could probably be moved out of this result. -/
  have integrable_lemma (i j : Fin d) :
      Integrable (fun x =>
        (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i))
        ((fderivCLM ℝ (Space d) ℝ) η)) x • f x) j) volume := byd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ (distDiv (distOfFunction f hf)) η = -∫ (x : Space d), ⟪f x, ∇ (⇑η) x⟫_ℝd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∫ (x : Space d), ∑ i, ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ
    simp only [PiLp.smul_apply]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin dj:Fin d⊢ Integrable (fun x => ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • (f x).ofLp j)
  volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∫ (x : Space d), ∑ i, ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ
    exact (hf.pi_comp j).integrable_space _d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∫ (x : Space d), ∑ i, ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∫ (x : Space d), ∑ i, ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ
  rw [MeasureTheory.integral_finsetSumd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∑ i, ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝhfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∀ i ∈ Finset.univ, Integrable (fun x => ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ) volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∑ i, ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝhfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∀ i ∈ Finset.univ, Integrable (fun x => ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ) volume]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∑ i, ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝhfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∀ i ∈ Finset.univ, Integrable (fun x => ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ) volume
  ·d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ i, (-∫ (x : Space d), ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp i =
  -∑ i, ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ simpd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∑ x, (∫ (x_1 : Space d), (fderiv ℝ (⇑η) x_1) (basis x) • f x_1).ofLp x =
  ∑ i, ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ
    congre_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ (fun x => (∫ (x_1 : Space d), (fderiv ℝ (⇑η) x_1) (basis x) • f x_1).ofLp x) = fun i =>
  ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ
    funext ie_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ (∫ (x : Space d), (fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i =
  ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ
    rw [MeasureTheory.eval_integral_piLpe_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∫ (x : Space d), ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i =
  ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝe_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∀ (i_1 : Fin d), Integrable (fun x => ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i_1) volumee_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∫ (x : Space d), ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i =
  ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝe_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∀ (i_1 : Fin d), Integrable (fun x => ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i_1) volume]e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∫ (x : Space d), ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i =
  ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝe_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∀ (i_1 : Fin d), Integrable (fun x => ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i_1) volume
    ·e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∫ (x : Space d), ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i =
  ∫ (a : Space d), ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ congre_f.e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ (fun x => ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i) = fun a => ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ
      funext xe_f.e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dx:Space d⊢ ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i = ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ
      simp [inner_smul_right, EuclideanSpace.inner_single_right]e_f.e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dx:Space d⊢ (fderiv ℝ (⇑η) x) (basis i) = deriv i (⇑η) x ∨ (f x).ofLp i = 0
      lefte_f.e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dx:Space d⊢ (fderiv ℝ (⇑η) x) (basis i) = deriv i (⇑η) x
      rw [deriv_eq_fderiv_basise_f.e_fd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dx:Space d⊢ (fderiv ℝ (⇑η) x) (basis i) = (fderiv ℝ (⇑η) x) (basis i)All goals completed! 🐙]All goals completed! 🐙
    ·e_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin d⊢ ∀ (i_1 : Fin d), Integrable (fun x => ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp i_1) volume intro je_f.hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dj:Fin d⊢ Integrable (fun x => ((fderiv ℝ (⇑η) x) (basis i) • f x).ofLp j) volume
      exact integrable_lemma i jAll goals completed! 🐙
  ·hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ ∀ i ∈ Finset.univ, Integrable (fun x => ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ) volume intro i hihfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univ⊢ Integrable (fun x => ⟪f x, deriv i (⇑η) x • EuclideanSpace.single i 1⟫_ℝ) volume
    simp only [inner_smul_right, EuclideanSpace.inner_single_right, conj_trivial, one_mul]hfd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univ⊢ Integrable (fun x => deriv i (⇑η) x * (f x).ofLp i) volume
    convert integrable_lemma i i using 2d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univx✝:Space d⊢ deriv i (⇑η) x✝ * (f x✝).ofLp i =
  (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x✝ • f x✝).ofLp i
    rename_i xd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univx:Space d⊢ deriv i (⇑η) x✝ * (f x✝).ofLp i =
  (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x✝ • f x✝).ofLp i
    simp only [evalCLM_apply_apply, fderivCLM_apply, PiLp.smul_apply, smul_eq_mul,
      mul_eq_mul_right_iff]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univx:Space d⊢ deriv i (⇑η) x = (fderiv ℝ (⇑η) x) (basis i) ∨ (f x).ofLp i = 0
    leftd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univx:Space d⊢ deriv i (⇑η) x = (fderiv ℝ (⇑η) x) (basis i)
    rw [deriv_eq_fderiv_basisd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)integrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumei:Fin dhi:i ∈ Finset.univx:Space d⊢ (fderiv ℝ (⇑η) x) (basis i) = (fderiv ℝ (⇑η) x) (basis i)All goals completed! 🐙]All goals completed! 🐙