Physlib.SpaceAndTime.Space.Derivatives.Grad

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.Basic
public import Physlib.SpaceAndTime.Space.IsDistBounded
public import Mathlib.Analysis.Calculus.Gradient.Basic

Gradient of functions and distributions on `Space d`

i. Overview

This module defines and proves basic properties of the gradient operator on functions from Space d to ℝ and on distributions from Space d to ℝ.

The gradient operator returns a vector field whose components are the partial derivatives of the input function with respect to each spatial coordinate.

ii. Key results

grad : The gradient operator on functions from Space d to ℝ.

distGrad : The gradient operator on distributions from Space d to ℝ.

iii. Table of contents

A. The gradient of functions on Space d

A.1. Gradient of the zero function

A.2. Gradient distributes over addition

A.3. Gradient of a constant function

A.4. Gradient distributes over scalar multiplication

A.5. Gradient distributes over negation

A.6. Expansion in terms of basis vectors

A.7. Components of the gradient

A.8. Inner product with a gradient

A.9. Gradient is equal to gradient from Mathlib

A.10. Value of gradient in the direction of the position vector

A.11. Gradient of the norm squared function

A.12. Gradient of the inner product function

A.13. Integrability with bounded functions

A.14. Differentiability of gradient

B. Gradient of distributions

B.1. The definition

B.2. The gradient of inner products

B.3. The gradient as a sum over basis vectors

B.4. The underlying function of the gradient distribution

B.5. The gradient applied to a Schwartz function

B.6. Gradient of constant distributions

B.7. The gradient of a Schwartz map

iv. References

@[expose] public section

A. The gradient of functions on `Space d`

@[inherit_doc grad]
scoped[Space] notation "∇" => grad

A.1. Gradient of the zero function

@[simp]
lemma grad_zero : ∇ (0 : Space d → ℝ) = 0 := byd:ℕ⊢ ∇ 0 = 0
  unfold grad Space.derivd:ℕ⊢ (fun x => WithLp.toLp 2 fun i => (fderiv ℝ 0 x) (basis i)) = 0
  simp only [fderiv_zero, Pi.zero_apply, _root_.zero_apply]d:ℕ⊢ (fun x => WithLp.toLp 2 fun i => 0) = 0
  rflAll goals completed! 🐙

A.2. Gradient distributes over addition



@[to_fun]
lemma grad_add (f1 f2 : Space d → ℝ)
    (hf1 : Differentiable ℝ f1) (hf2 : Differentiable ℝ f2) :
    ∇ (f1 + f2) = ∇ f1 + ∇ f2 := byd:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ ∇ (f1 + f2) = ∇ f1 + ∇ f2
  unfold gradd:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2⊢ (fun x => WithLp.toLp 2 fun i => deriv i (f1 + f2) x) =
  (fun x => WithLp.toLp 2 fun i => deriv i f1 x) + fun x => WithLp.toLp 2 fun i => deriv i f2 x
  ext x id:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (WithLp.toLp 2 fun i => deriv i (f1 + f2) x).ofLp i =
  (((fun x => WithLp.toLp 2 fun i => deriv i f1 x) + fun x => WithLp.toLp 2 fun i => deriv i f2 x) x).ofLp i
  simp only [Pi.add_apply]d:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ deriv i (f1 + f2) x = ((WithLp.toLp 2 fun i => deriv i f1 x) + WithLp.toLp 2 fun i => deriv i f2 x).ofLp i
  rw [deriv_add f1 f2 hf1 hf2d:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (deriv i f1 + deriv i f2) x = ((WithLp.toLp 2 fun i => deriv i f1 x) + WithLp.toLp 2 fun i => deriv i f2 x).ofLp id:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (deriv i f1 + deriv i f2) x = ((WithLp.toLp 2 fun i => deriv i f1 x) + WithLp.toLp 2 fun i => deriv i f2 x).ofLp i]d:ℕf1:Space d → ℝf2:Space d → ℝhf1:Differentiable ℝ f1hf2:Differentiable ℝ f2x:Space di:Fin d⊢ (deriv i f1 + deriv i f2) x = ((WithLp.toLp 2 fun i => deriv i f1 x) + WithLp.toLp 2 fun i => deriv i f2 x).ofLp i
  rflAll goals completed! 🐙

@[simp]
lemma grad_fun_add_const (f : Space d → ℝ) (c : ℝ) :
    ∇ (fun x => f x + c) = ∇ f := byd:ℕf:Space d → ℝc:ℝ⊢ (∇ fun x => f x + c) = ∇ f
  ext x id:ℕf:Space d → ℝc:ℝx:Space di:Fin d⊢ (∇ (fun x => f x + c) x).ofLp i = (∇ f x).ofLp i
  simp [grad, deriv]All goals completed! 🐙

A.3. Gradient of a constant function

@[simp]
lemma grad_const : ∇ (fun _ : Space d => c) = 0 := byd:ℕc:ℝ⊢ (∇ fun x => c) = 0
  unfold grad Space.derivd:ℕc:ℝ⊢ (fun x => WithLp.toLp 2 fun i => (fderiv ℝ (fun x => c) x) (basis i)) = 0
  simp only [fderiv_fun_const, Pi.ofNat_apply, _root_.zero_apply]d:ℕc:ℝ⊢ (fun x => WithLp.toLp 2 fun i => 0) = 0
  rflAll goals completed! 🐙

A.4. Gradient distributes over scalar multiplication



@[to_fun]
lemma grad_smul (f : Space d → ℝ) (k : ℝ)
    (hf : Differentiable ℝ f) :
    ∇ (k • f) = k • ∇ f := byd:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ f⊢ ∇ (k • f) = k • ∇ f
  unfold gradd:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ f⊢ (fun x => WithLp.toLp 2 fun i => deriv i (k • f) x) = k • fun x => WithLp.toLp 2 fun i => deriv i f x
  ext x id:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (WithLp.toLp 2 fun i => deriv i (k • f) x).ofLp i = ((k • fun x => WithLp.toLp 2 fun i => deriv i f x) x).ofLp i
  simp only [Pi.smul_apply]d:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ deriv i (k • f) x = (k • WithLp.toLp 2 fun i => deriv i f x).ofLp i
  rw [deriv_const_smul k hfd:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (k • deriv i f) x = (k • WithLp.toLp 2 fun i => deriv i f x).ofLp id:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (k • deriv i f) x = (k • WithLp.toLp 2 fun i => deriv i f x).ofLp i]d:ℕf:Space d → ℝk:ℝhf:Differentiable ℝ fx:Space di:Fin d⊢ (k • deriv i f) x = (k • WithLp.toLp 2 fun i => deriv i f x).ofLp i
  rflAll goals completed! 🐙

A.5. Gradient distributes over negation



@[to_fun]
lemma grad_neg (f : Space d → ℝ) :
    ∇ (- f) = - ∇ f := byd:ℕf:Space d → ℝ⊢ ∇ (-f) = -∇ f
  unfold gradd:ℕf:Space d → ℝ⊢ (fun x => WithLp.toLp 2 fun i => deriv i (-f) x) = -fun x => WithLp.toLp 2 fun i => deriv i f x
  ext x id:ℕf:Space d → ℝx:Space di:Fin d⊢ (WithLp.toLp 2 fun i => deriv i (-f) x).ofLp i = ((-fun x => WithLp.toLp 2 fun i => deriv i f x) x).ofLp i
  simp only [Pi.neg_apply]d:ℕf:Space d → ℝx:Space di:Fin d⊢ deriv i (-f) x = (-WithLp.toLp 2 fun i => deriv i f x).ofLp i
  rw [Space.deriv_eq,d:ℕf:Space d → ℝx:Space di:Fin d⊢ (fderiv ℝ (-f) x) (basis i) = (-WithLp.toLp 2 fun i => deriv i f x).ofLp id:ℕf:Space d → ℝx:Space di:Fin d⊢ (-fderiv ℝ f x) (basis i) = (-WithLp.toLp 2 fun i => deriv i f x).ofLp i fderiv_negd:ℕf:Space d → ℝx:Space di:Fin d⊢ (-fderiv ℝ f x) (basis i) = (-WithLp.toLp 2 fun i => deriv i f x).ofLp id:ℕf:Space d → ℝx:Space di:Fin d⊢ (-fderiv ℝ f x) (basis i) = (-WithLp.toLp 2 fun i => deriv i f x).ofLp i]d:ℕf:Space d → ℝx:Space di:Fin d⊢ (-fderiv ℝ f x) (basis i) = (-WithLp.toLp 2 fun i => deriv i f x).ofLp i
  rflAll goals completed! 🐙

A.6. Expansion in terms of basis vectors

lemma grad_eq_sum {d} (f : Space d → ℝ) (x : Space d) :
    ∇ f x = ∑ i, ∂[i] f x • EuclideanSpace.single i 1 := byd:ℕf:Space d → ℝx:Space d⊢ ∇ f x = ∑ i, deriv i f x • EuclideanSpace.single i 1
  ext jd:ℕf:Space d → ℝx:Space dj:Fin d⊢ (∇ f x).ofLp j = (∑ i, deriv i f x • EuclideanSpace.single i 1).ofLp j
  simp only [grad, PiLp.toLp_apply, WithLp.ofLp_sum, WithLp.ofLp_smul, PiLp.ofLp_single,
    Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero,
    Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]All goals completed! 🐙

A.7. Components of the gradient

lemma grad_apply {d} (f : Space d → ℝ) (x : Space d) (i : Fin d) :
    (∇ f x) i = ∂[i] f x := byd:ℕf:Space d → ℝx:Space di:Fin d⊢ (∇ f x).ofLp i = deriv i f x
  rflAll goals completed! 🐙

A.8. Inner product with a gradient

              lemma grad_inner_single {d} (f : Space d → ℝ) (x : Space d) (i : Fin d) :
    ⟪∇ f x, EuclideanSpace.single i 1⟫_ℝ = ∂[i] f x := byd:ℕf:Space d → ℝx:Space di:Fin d⊢ ⟪∇ f x, EuclideanSpace.single i 1⟫_ℝ = deriv i f x
  simp [EuclideanSpace.inner_single_right, grad_apply]All goals completed! 🐙lemma grad_inner_eq {d} (f : Space d → ℝ) (x : Space d) (y : EuclideanSpace ℝ (Fin d)) :
    ⟪∇ f x, y⟫_ℝ = ∑ i, y i * ∂[i] f x:= byd:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = ∑ i, y.ofLp i * deriv i f x
  simp [PiLp.inner_apply, RCLike.inner_apply, conj_trivial, grad_apply, mul_comm]All goals completed! 🐙lemma inner_grad_eq {d} (f : Space d → ℝ) (x : EuclideanSpace ℝ (Fin d)) (y : Space d) :
    ⟪x, ∇ f y⟫_ℝ = ∑ i, x i * ∂[i] f y :=
  (real_inner_comm (∇ f y) x).trans (grad_inner_eq f y x)lemma grad_inner_repr_eq {d} (f : Space d → ℝ) (x y : Space d) :
    ⟪∇ f x, (Space.basis).repr y⟫_ℝ = fderiv ℝ f x y := byd:ℕf:Space d → ℝx:Space dy:Space d⊢ ⟪∇ f x, basis.repr y⟫_ℝ = (fderiv ℝ f x) y
  simp [grad_inner_eq f x, fderiv_eq_sum_deriv]All goals completed! 🐙lemma repr_grad_inner_eq {d} (f : Space d → ℝ) (x y : Space d) :
    ⟪(Space.basis).repr x, ∇ f y⟫_ℝ = fderiv ℝ f y x :=
  (real_inner_comm (∇ f y) ((Space.basis).repr x)).trans (grad_inner_repr_eq f y x)

A.9. Gradient is equal to `gradient` from Mathlib

              

lemma grad_eq_gradient {d} (f : Space d → ℝ) :
    ∇ f = basis.repr ∘ gradient f := byd:ℕf:Space d → ℝ⊢ ∇ f = ⇑basis.repr ∘ gradient f
  funext xd:ℕf:Space d → ℝx:Space d⊢ ∇ f x = (⇑basis.repr ∘ gradient f) x
  refine ext_inner_right (𝕜 := ℝ) fun y => ?_d:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = ⟪(⇑basis.repr ∘ gradient f) x, y⟫_ℝ
  rw [Function.comp_apply,d:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = ⟪basis.repr (gradient f x), y⟫_ℝd:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = (fderiv ℝ f x) (basis.repr.symm y) gradient,d:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = ⟪basis.repr ((toDual ℝ (Space d)).symm (fderiv ℝ f x)), y⟫_ℝd:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = (fderiv ℝ f x) (basis.repr.symm y) basis_repr_inner_eq,d:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = ⟪(toDual ℝ (Space d)).symm (fderiv ℝ f x), basis.repr.symm y⟫_ℝd:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = (fderiv ℝ f x) (basis.repr.symm y) toDual_symm_applyd:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = (fderiv ℝ f x) (basis.repr.symm y)d:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = (fderiv ℝ f x) (basis.repr.symm y)]d:ℕf:Space d → ℝx:Space dy:EuclideanSpace ℝ (Fin d)⊢ ⟪∇ f x, y⟫_ℝ = (fderiv ℝ f x) (basis.repr.symm y)
  simp [grad_inner_eq f x, fderiv_eq_sum_deriv]All goals completed! 🐙

lemma gradient_eq_grad {d} (f : Space d → ℝ) :
    gradient f = basis.repr.symm ∘ ∇ f := byd:ℕf:Space d → ℝ⊢ gradient f = ⇑basis.repr.symm ∘ ∇ f
  rw [grad_eq_gradient fd:ℕf:Space d → ℝ⊢ gradient f = ⇑basis.repr.symm ∘ ⇑basis.repr ∘ gradient fd:ℕf:Space d → ℝ⊢ gradient f = ⇑basis.repr.symm ∘ ⇑basis.repr ∘ gradient f]d:ℕf:Space d → ℝ⊢ gradient f = ⇑basis.repr.symm ∘ ⇑basis.repr ∘ gradient f
  ext xd:ℕf:Space d → ℝx:Space di✝:Fin d⊢ (gradient f x).val i✝ = ((⇑basis.repr.symm ∘ ⇑basis.repr ∘ gradient f) x).val i✝
  simpAll goals completed! 🐙

lemma gradient_apply_eq_grad {d} (f : Space d → ℝ) (x : Space d) :
    gradient f x = basis.repr.symm (∇ f x) := byd:ℕf:Space d → ℝx:Space d⊢ gradient f x = basis.repr.symm (∇ f x)
  rw [grad_eq_gradient fd:ℕf:Space d → ℝx:Space d⊢ gradient f x = basis.repr.symm ((⇑basis.repr ∘ gradient f) x)d:ℕf:Space d → ℝx:Space d⊢ gradient f x = basis.repr.symm ((⇑basis.repr ∘ gradient f) x)]d:ℕf:Space d → ℝx:Space d⊢ gradient f x = basis.repr.symm ((⇑basis.repr ∘ gradient f) x)
  simpAll goals completed! 🐙lemma gradient_eq_sum {d} (f : Space d → ℝ) (x : Space d) :
    gradient f x = ∑ i, ∂[i] f x • basis i := byd:ℕf:Space d → ℝx:Space d⊢ gradient f x = ∑ i, deriv i f x • basis i
  simp [gradient_eq_grad, grad_eq_sum f x]All goals completed! 🐙

lemma euclid_gradient_eq_sum {d} (f : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) :
    gradient f x = ∑ i, fderiv ℝ f x (EuclideanSpace.single i 1) • EuclideanSpace.single i 1 := byd:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)⊢ gradient f x = ∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1
  apply ext_inner_right (𝕜 := ℝ) fun y => ?_d:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)⊢ ⟪gradient f x, y⟫_ℝ = ⟪∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1, y⟫_ℝ
  simp [gradient]d:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)⊢ (fderiv ℝ f x) y = ⟪∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1, y⟫_ℝ
  have hy : y = ∑ i, y i • EuclideanSpace.single i 1 := byd:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)⊢ gradient f x = ∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1d:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ (fderiv ℝ f x) y = ⟪∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1, y⟫_ℝ
    conv_lhs => rw [← OrthonormalBasis.sum_repr (EuclideanSpace.basisFun (Fin d) ℝ) y]d:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)| ∑ i, ((EuclideanSpace.basisFun (Fin d) ℝ).repr y).ofLp i • (EuclideanSpace.basisFun (Fin d) ℝ) id:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ (fderiv ℝ f x) y = ⟪∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1, y⟫_ℝ
    simpd:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ (fderiv ℝ f x) y = ⟪∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1, y⟫_ℝd:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ (fderiv ℝ f x) y = ⟪∑ i, (fderiv ℝ f x) (EuclideanSpace.single i 1) • EuclideanSpace.single i 1, y⟫_ℝ
  conv_lhs => rw [hy]d:ℕf:EuclideanSpace ℝ (Fin d) → ℝx:EuclideanSpace ℝ (Fin d)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1| (fderiv ℝ f x) (∑ i, y.ofLp i • EuclideanSpace.single i 1)
  simp [sum_inner, inner_smul_left, EuclideanSpace.inner_single_left, mul_comm]All goals completed! 🐙

lemma _root_.DifferentiableAt.hasGradientAt_grad {d} {f : Space d → ℝ} (x : Space d)
    (hf : DifferentiableAt ℝ f x) :
    HasGradientAt f (basis.repr.symm (∇ f x)) x := byd:ℕf:Space d → ℝx:Space dhf:DifferentiableAt ℝ f x⊢ HasGradientAt f (basis.repr.symm (∇ f x)) x
  rw [← gradient_apply_eq_gradd:ℕf:Space d → ℝx:Space dhf:DifferentiableAt ℝ f x⊢ HasGradientAt f (gradient f x) xd:ℕf:Space d → ℝx:Space dhf:DifferentiableAt ℝ f x⊢ HasGradientAt f (gradient f x) x]d:ℕf:Space d → ℝx:Space dhf:DifferentiableAt ℝ f x⊢ HasGradientAt f (gradient f x) x
  exact DifferentiableAt.hasGradientAt hfAll goals completed! 🐙

A.10. Value of gradient in the direction of the position vector

The gradient in the direction of the space position.


lemma grad_inner_space_unit_vector {d} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) :
    ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖
  by_cases hx : x = 0posd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:x = 0⊢ ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖negd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖
  ·posd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:x = 0⊢ ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ subst hxposd:ℕf:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f 0, ‖0‖⁻¹ • basis.repr 0⟫_ℝ = _root_.deriv (fun r => f (r • ‖0‖⁻¹ • 0)) ‖0‖
    simpAll goals completed! 🐙
  symmnegd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ = ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝ
  calc _
    _ = fderiv ℝ (f ∘ (fun r => r • ‖x‖⁻¹ • x)) ‖x‖ 1 := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ = (fderiv ℝ (f ∘ fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 rflAll goals completed! 🐙
    _ = (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ (f ∘ fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 =
  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)
      rw [fderiv_comp _ (byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ DifferentiableAt ℝ f (‖x‖ • ‖x‖⁻¹ • x)d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x) ∘SL fderiv ℝ (fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 =
  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) fun_propAll goals completed! 🐙d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x) ∘SL fderiv ℝ (fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 =
  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)) (byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ DifferentiableAt ℝ (fun r => r • ‖x‖⁻¹ • x) ‖x‖d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x) ∘SL fderiv ℝ (fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 =
  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) fun_propAll goals completed! 🐙d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x) ∘SL fderiv ℝ (fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 =
  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖))]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x) ∘SL fderiv ℝ (fun r => r • ‖x‖⁻¹ • x) ‖x‖) 1 =
  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)
      simpAll goals completed! 🐙
    _ = (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) =
  (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)
      have hx : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hxd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx✝:¬x = 0hx:‖x‖ ≠ 0⊢ (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) =
  (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)
      rw [smul_smul,d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx✝:¬x = 0hx:‖x‖ ≠ 0⊢ (fderiv ℝ f ((‖x‖ * ‖x‖⁻¹) • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) =
  (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)All goals completed! 🐙 mul_inv_cancel₀ hx,d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx✝:¬x = 0hx:‖x‖ ≠ 0⊢ (fderiv ℝ f (1 • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) =
  (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)All goals completed! 🐙 one_smuld:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx✝:¬x = 0hx:‖x‖ ≠ 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) = (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖)All goals completed! 🐙]All goals completed! 🐙
  rw [grad_inner_eq f x (‖x‖⁻¹ • basis.repr x)neg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) = ∑ i, (‖x‖⁻¹ • basis.repr x).ofLp i * deriv i f xneg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) = ∑ i, (‖x‖⁻¹ • basis.repr x).ofLp i * deriv i f x]neg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) = ∑ i, (‖x‖⁻¹ • basis.repr x).ofLp i * deriv i f x
  rw [deriv_smul_const (byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ DifferentiableAt ℝ (fun r => r) ‖x‖neg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r) ‖x‖ • ‖x‖⁻¹ • x) = ∑ i, (‖x‖⁻¹ • basis.repr x).ofLp i * deriv i f x fun_propAll goals completed! 🐙neg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r) ‖x‖ • ‖x‖⁻¹ • x) = ∑ i, (‖x‖⁻¹ • basis.repr x).ofLp i * deriv i f x)]neg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ (fderiv ℝ f x) (_root_.deriv (fun r => r) ‖x‖ • ‖x‖⁻¹ • x) = ∑ i, (‖x‖⁻¹ • basis.repr x).ofLp i * deriv i f x
  simp only [deriv_id'', one_smul, map_smul, fderiv_eq_sum_deriv, smul_eq_mul, Finset.mul_sum,
    PiLp.smul_apply, basis_repr_apply]neg.calc.stepd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ ∑ i, ‖x‖⁻¹ * (x.val i * deriv i f x) = ∑ x_1, ‖x‖⁻¹ * x.val x_1 * deriv x_1 f x
  ring_nfAll goals completed! 🐙

              

lemma grad_inner_space {d} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) :
    ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖
  rw [← grad_inner_space_unit_vector _ _ hd,d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * ⟪∇ f x, ‖x‖⁻¹ • basis.repr x⟫_ℝd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ) inner_smul_rightd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ)d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ)]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ)
  by_cases hx : x = 0posd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:x = 0⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ)negd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:¬x = 0⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ)
  ·posd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx:x = 0⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ) subst hxposd:ℕf:Space d → ℝhd:Differentiable ℝ f⊢ ⟪∇ f 0, basis.repr 0⟫_ℝ = ‖0‖ * (‖0‖⁻¹ * ⟪∇ f 0, basis.repr 0⟫_ℝ)
    simpAll goals completed! 🐙
  have hx : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hxnegd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ fhx✝:¬x = 0hx:‖x‖ ≠ 0⊢ ⟪∇ f x, basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f x, basis.repr x⟫_ℝ)
  field_simpAll goals completed! 🐙

lemma grad_smul_inner_space {d} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) (t : ℝ)
    (ht : 0 < t) :
    ⟪∇ f (t • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) t := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < t⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) t
  by_cases hx : ‖x‖ = 0posd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:‖x‖ = 0⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) tnegd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) t
  ·posd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:‖x‖ = 0⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) t simp at hxposd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:x = 0⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) t
    simp [hx]All goals completed! 🐙
  calc _
    _ = ‖x‖ * ⟪∇ f (t • x), ‖x‖⁻¹ • basis.repr x⟫_ℝ := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = ‖x‖ * ⟪∇ f (t • x), ‖x‖⁻¹ • basis.repr x⟫_ℝ
      simp [inner_smul_right]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ⟪∇ f (t • x), basis.repr x⟫_ℝ = ‖x‖ * (‖x‖⁻¹ * ⟪∇ f (t • x), basis.repr x⟫_ℝ)
      grindAll goals completed! 🐙
    _ = ‖x‖ * ⟪∇ f (t • x), ‖t • x‖⁻¹ • basis.repr (t • x)⟫_ℝ := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * ⟪∇ f (t • x), ‖x‖⁻¹ • basis.repr x⟫_ℝ = ‖x‖ * ⟪∇ f (t • x), ‖t • x‖⁻¹ • basis.repr (t • x)⟫_ℝ
      simp [norm_smul, smul_smul]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ⟪∇ f (t • x), ‖x‖⁻¹ • basis.repr x⟫_ℝ = ⟪∇ f (t • x), (‖x‖⁻¹ * |t|⁻¹ * t) • basis.repr x⟫_ℝ ∨ x = 0
      grindAll goals completed! 🐙
    _ = ‖x‖ * _root_.deriv (fun r => f (r • ‖t • x‖⁻¹ • t • x)) ‖t • x‖ := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * ⟪∇ f (t • x), ‖t • x‖⁻¹ • basis.repr (t • x)⟫_ℝ = ‖x‖ * _root_.deriv (fun r => f (r • ‖t • x‖⁻¹ • t • x)) ‖t • x‖
      rw [grad_inner_space_unit_vector _ _ hdd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * _root_.deriv (fun r => f (r • ‖t • x‖⁻¹ • t • x)) ‖t • x‖ =
  ‖x‖ * _root_.deriv (fun r => f (r • ‖t • x‖⁻¹ • t • x)) ‖t • x‖All goals completed! 🐙]All goals completed! 🐙
    _ = ‖x‖ * _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) (t * ‖x‖) := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * _root_.deriv (fun r => f (r • ‖t • x‖⁻¹ • t • x)) ‖t • x‖ =
  ‖x‖ * _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) (t * ‖x‖)
      simp [smul_smul, norm_smul]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ _root_.deriv (fun r => f ((r * (‖x‖⁻¹ * |t|⁻¹ * t)) • x)) (|t| * ‖x‖) =
    _root_.deriv (fun r => f ((r * ‖x‖⁻¹) • x)) (t * ‖x‖) ∨
  x = 0
      grindAll goals completed! 🐙
    _ = ‖x‖ * _root_.deriv ((fun r => f (r • x)) ∘ (fun r => ‖x‖⁻¹ * r)) (t * ‖x‖) := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) (t * ‖x‖) =
  ‖x‖ * _root_.deriv ((fun r => f (r • x)) ∘ fun r => ‖x‖⁻¹ * r) (t * ‖x‖)
      congre_a.e_fd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ (fun r => f (r • ‖x‖⁻¹ • x)) = (fun r => f (r • x)) ∘ fun r => ‖x‖⁻¹ * r
      funext re_a.e_fd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0r:ℝ⊢ f (r • ‖x‖⁻¹ • x) = ((fun r => f (r • x)) ∘ fun r => ‖x‖⁻¹ * r) r
      simp [smul_smul]e_a.e_fd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0r:ℝ⊢ f ((r * ‖x‖⁻¹) • x) = f ((‖x‖⁻¹ * r) • x)
      grindAll goals completed! 🐙
    _ = _root_.deriv (fun r => f (r • x)) t := byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * _root_.deriv ((fun r => f (r • x)) ∘ fun r => ‖x‖⁻¹ * r) (t * ‖x‖) = _root_.deriv (fun r => f (r • x)) t
      rw [deriv_comp _ (byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ DifferentiableAt ℝ (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖))d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * _root_.deriv (fun r => ‖x‖⁻¹ * r) (t * ‖x‖)) =
  _root_.deriv (fun r => f (r • x)) t fun_propAll goals completed! 🐙d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * _root_.deriv (fun r => ‖x‖⁻¹ * r) (t * ‖x‖)) =
  _root_.deriv (fun r => f (r • x)) t) (byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ DifferentiableAt ℝ (fun r => ‖x‖⁻¹ * r) (t * ‖x‖)d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * _root_.deriv (fun r => ‖x‖⁻¹ * r) (t * ‖x‖)) =
  _root_.deriv (fun r => f (r • x)) t fun_propAll goals completed! 🐙d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * _root_.deriv (fun r => ‖x‖⁻¹ * r) (t * ‖x‖)) =
  _root_.deriv (fun r => f (r • x)) t)]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * _root_.deriv (fun r => ‖x‖⁻¹ * r) (t * ‖x‖)) =
  _root_.deriv (fun r => f (r • x)) t
      rw [deriv_const_mul _ (byd:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ DifferentiableAt ℝ (fun r => r) (t * ‖x‖)d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * (‖x‖⁻¹ * _root_.deriv (fun r => r) (t * ‖x‖))) =
  _root_.deriv (fun r => f (r • x)) t fun_propAll goals completed! 🐙d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * (‖x‖⁻¹ * _root_.deriv (fun r => r) (t * ‖x‖))) =
  _root_.deriv (fun r => f (r • x)) t)]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * (‖x‖⁻¹ * _root_.deriv (fun r => r) (t * ‖x‖))) =
  _root_.deriv (fun r => f (r • x)) t
      simp only [deriv_id'', mul_one]d:ℕx:Space df:Space d → ℝhd:Differentiable ℝ ft:ℝht:0 < thx:¬‖x‖ = 0⊢ ‖x‖ * (_root_.deriv (fun r => f (r • x)) (‖x‖⁻¹ * (t * ‖x‖)) * ‖x‖⁻¹) = _root_.deriv (fun r => f (r • x)) t
      grindAll goals completed! 🐙
lemma eq_integral_grad {f : Space → ℝ} (hf : ContDiff ℝ 1 f) :
    f = (fun x => ∫ t in (0 : ℝ)..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ ∂(volume)
      + f 0) := byf:Space → ℝhf:ContDiff ℝ 1 f⊢ f = fun x => (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0
  ext xf:Space → ℝhf:ContDiff ℝ 1 fx:Space⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0
  have h' := (hf.differentiable (byf:Space → ℝhf:ContDiff ℝ 1 fx:Space⊢ 1 ≠ 0f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ f⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0 simpAll goals completed! 🐙f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ f⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0))f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ f⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0
  by_cases hx : ‖x‖ = 0posf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:‖x‖ = 0⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0negf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0
  ·posf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:‖x‖ = 0⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0 simp at hxposf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:x = 0⊢ f x = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0
    subst hxposf:Space → ℝhf:ContDiff ℝ 1 fh':Differentiable ℝ f⊢ f 0 = (∫ (t : ℝ) in 0..1, ⟪∇ f (t • 0), basis.repr 0⟫_ℝ) + f 0
    simpAll goals completed! 🐙
  symmnegf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0 = f x
  calc _
    _ = ∫ (t : ℝ) in 0..1, (_root_.deriv (fun r => f (r • x)) t) ∂volume + f 0 := byf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ (∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ) + f 0 =
  (∫ (t : ℝ) in 0..1, _root_.deriv (fun r => f (r • x)) t) + f 0
      congr 1e_af:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ ∫ (t : ℝ) in 0..1, ⟪∇ f (t • x), basis.repr x⟫_ℝ = ∫ (t : ℝ) in 0..1, _root_.deriv (fun r => f (r • x)) t
      refine intervalIntegral.integral_congr_ae_restrict ?_e_af:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ (fun t => ⟪∇ f (t • x), basis.repr x⟫_ℝ) =ᵐ[volume.restrict (Set.uIoc 0 1)] _root_.deriv fun r => f (r • x)
      refine (ae_eq_restrict_iff_indicator_ae_eq measurableSet_uIoc).mpr ?_e_af:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ ((Set.uIoc 0 1).indicator fun t => ⟪∇ f (t • x), basis.repr x⟫_ℝ) =ᵐ[volume]
  (Set.uIoc 0 1).indicator (_root_.deriv fun r => f (r • x))
      filter_upwards with pe_af:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝ⊢ (Set.uIoc 0 1).indicator (fun t => ⟪∇ f (t • x), basis.repr x⟫_ℝ) p =
  (Set.uIoc 0 1).indicator (_root_.deriv fun r => f (r • x)) p
      simp only [Set.indicator, zero_le_one, Set.uIoc_of_le, Set.mem_Ioc]e_af:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝ⊢ (if 0 < p ∧ p ≤ 1 then ⟪∇ f (p • x), basis.repr x⟫_ℝ else 0) =
  if 0 < p ∧ p ≤ 1 then _root_.deriv (fun r => f (r • x)) p else 0
      split_ifsposf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ ⟪∇ f (p • x), basis.repr x⟫_ℝ = _root_.deriv (fun r => f (r • x)) pnegf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:¬(0 < p ∧ p ≤ 1)⊢ 0 = 0
      rw [grad_smul_inner_spaceposf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ _root_.deriv (fun r => f (r • x)) p = _root_.deriv (fun r => f (r • x)) ppos.hdf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ Differentiable ℝ fpos.htf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ 0 < pnegf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:¬(0 < p ∧ p ≤ 1)⊢ 0 = 0pos.hdf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ Differentiable ℝ fpos.htf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ 0 < pnegf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:¬(0 < p ∧ p ≤ 1)⊢ 0 = 0]pos.hdf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ Differentiable ℝ fpos.htf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ 0 < pnegf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:¬(0 < p ∧ p ≤ 1)⊢ 0 = 0
      ·pos.hdf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ Differentiable ℝ f exact h'All goals completed! 🐙
      ·pos.htf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:0 < p ∧ p ≤ 1⊢ 0 < p grindAll goals completed! 🐙
      ·negf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0p:ℝh✝:¬(0 < p ∧ p ≤ 1)⊢ 0 = 0 grindAll goals completed! 🐙
    _ = (f (1 • x) - f 0) + f 0 := byf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ (∫ (t : ℝ) in 0..1, _root_.deriv (fun r => f (r • x)) t) + f 0 = f (1 • x) - f 0 + f 0
      rw [intervalIntegral.integral_deriv_eq_sub (byf:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ ∀ x_1 ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun r => f (r • x)) x_1f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ f (1 • x) - f (0 • x) + f 0 = f (1 • x) - f 0 + f 0f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ IntervalIntegrable (_root_.deriv fun r => f (r • x)) volume 0 1 fun_propAll goals completed! 🐙f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ f (1 • x) - f (0 • x) + f 0 = f (1 • x) - f 0 + f 0f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ IntervalIntegrable (_root_.deriv fun r => f (r • x)) volume 0 1)]f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ f (1 • x) - f (0 • x) + f 0 = f (1 • x) - f 0 + f 0f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ IntervalIntegrable (_root_.deriv fun r => f (r • x)) volume 0 1
      simp only [one_smul, zero_smul, sub_add_cancel]f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ IntervalIntegrable (_root_.deriv fun r => f (r • x)) volume 0 1
      ·f:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ IntervalIntegrable (_root_.deriv fun r => f (r • x)) volume 0 1 apply Continuous.intervalIntegrablef:Space → ℝhf:ContDiff ℝ 1 fx:Spaceh':Differentiable ℝ fhx:¬‖x‖ = 0⊢ Continuous (_root_.deriv fun r => f (r • x))
        fun_propAll goals completed! 🐙
  simpAll goals completed! 🐙

A.11. Gradient of the norm squared function



lemma grad_norm_sq (x : Space d) :
    ∇ (fun x => ‖x‖ ^ 2) x = (2 : ℝ) • basis.repr x := byd:ℕx:Space d⊢ ∇ (fun x => ‖x‖ ^ 2) x = 2 • basis.repr x
  ext id:ℕx:Space di:Fin d⊢ (∇ (fun x => ‖x‖ ^ 2) x).ofLp i = (2 • basis.repr x).ofLp i
  rw [grad_apply,d:ℕx:Space di:Fin d⊢ deriv i (fun x => ‖x‖ ^ 2) x = (2 • basis.repr x).ofLp id:ℕx:Space di:Fin d⊢ 2 * x.val i = (2 • basis.repr x).ofLp i deriv_norm_sqd:ℕx:Space di:Fin d⊢ 2 * x.val i = (2 • basis.repr x).ofLp id:ℕx:Space di:Fin d⊢ 2 * x.val i = (2 • basis.repr x).ofLp i]d:ℕx:Space di:Fin d⊢ 2 * x.val i = (2 • basis.repr x).ofLp i
  simpAll goals completed! 🐙

A.12. Gradient of the inner product function

The gradient of the inner product is given by 2 • x.


lemma grad_inner {d : ℕ} :
    ∇ (fun y : Space d => ⟪y, y⟫_ℝ) = fun z => (2 : ℝ) • basis.repr z := byd:ℕ⊢ (∇ fun y => ⟪y, y⟫_ℝ) = fun z => 2 • basis.repr z
  ext z id:ℕz:Space di:Fin d⊢ (∇ (fun y => ⟪y, y⟫_ℝ) z).ofLp i = (2 • basis.repr z).ofLp i
  rw [grad_apply,d:ℕz:Space di:Fin d⊢ deriv i (fun y => ⟪y, y⟫_ℝ) z = (2 • basis.repr z).ofLp id:ℕz:Space di:Fin d⊢ 2 * z.val i = (2 • basis.repr z).ofLp i deriv_eq_inner_selfd:ℕz:Space di:Fin d⊢ 2 * z.val i = (2 • basis.repr z).ofLp id:ℕz:Space di:Fin d⊢ 2 * z.val i = (2 • basis.repr z).ofLp i]d:ℕz:Space di:Fin d⊢ 2 * z.val i = (2 • basis.repr z).ofLp i
  simpAll goals completed! 🐙

lemma grad_inner_left {d : ℕ} (x : Space d) :
    ∇ (fun y : Space d => ⟪y, x⟫_ℝ) = fun _ => basis.repr x := byd:ℕx:Space d⊢ (∇ fun y => ⟪y, x⟫_ℝ) = fun x_1 => basis.repr x
  ext z id:ℕx:Space dz:Space di:Fin d⊢ (∇ (fun y => ⟪y, x⟫_ℝ) z).ofLp i = (basis.repr x).ofLp i
  simp [Space.grad]All goals completed! 🐙

lemma grad_inner_right {d : ℕ} (x : Space d) :
    ∇ (fun y : Space d => ⟪x, y⟫_ℝ) = fun _ => basis.repr x := byd:ℕx:Space d⊢ (∇ fun y => ⟪x, y⟫_ℝ) = fun x_1 => basis.repr x
  simp_rw [d:ℕx:Space d⊢ (∇ fun y => ⟪x, y⟫_ℝ) = fun x_1 => basis.repr x← real_inner_comm xd:ℕx:Space d⊢ (∇ fun y => ⟪y, x⟫_ℝ) = fun x_1 => basis.repr x]
  exact grad_inner_left xAll goals completed! 🐙

A.13. Integrability with bounded functions



/- The quantity `⟪f x, Space.grad η x⟫_ℝ` is integrable for `f` bounded
  and `η` a Schwartz map. -/
lemma integrable_isDistBounded_inner_grad_schwartzMap {d : ℕ}
    {f : Space d → EuclideanSpace ℝ (Fin d)}
    (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) :
    Integrable (fun x => ⟪f x, Space.grad η x⟫_ℝ) volume := byd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) volume
  conv =>d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)| Integrable (fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) volume
    enter [1, 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⟫_ℝ
  apply MeasureTheory.integrable_finsetSumd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ ∀ i ∈ Finset.univ, Integrable (fun a => ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ) volume
  intro i _d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univ⊢ Integrable (fun a => ⟪f a, deriv i (⇑η) a • EuclideanSpace.single i 1⟫_ℝ) volume
  simp [inner_smul_right]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univ⊢ Integrable (fun a => deriv i (⇑η) a * ⟪f a, EuclideanSpace.single i 1⟫_ℝ) volume
  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, ℝ)⊢ Integrable (fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ Integrable (fun a => deriv i (⇑η) a * ⟪f a, EuclideanSpace.single i 1⟫_ℝ) volume
    simp only [PiLp.smul_apply]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i✝:Fin da✝:i ∈ Finset.univi: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, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ Integrable (fun a => deriv i (⇑η) a * ⟪f a, EuclideanSpace.single i 1⟫_ℝ) volume
    exact (hf.pi_comp j).integrable_space _d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ Integrable (fun a => deriv i (⇑η) a * ⟪f a, EuclideanSpace.single i 1⟫_ℝ) volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volume⊢ Integrable (fun a => deriv i (⇑η) a * ⟪f a, EuclideanSpace.single i 1⟫_ℝ) volume
  convert! integrable_lemma i i using 2e'_6d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumex✝:Space d⊢ deriv i (⇑η) x✝ * ⟪f x✝, EuclideanSpace.single i 1⟫_ℝ =
  (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x✝ • f x✝).ofLp i
  rename_i xe'_6d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumex:Space d⊢ deriv i (⇑η) x✝ * ⟪f x✝, EuclideanSpace.single i 1⟫_ℝ =
  (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x✝ • f x✝).ofLp i
  simp only [EuclideanSpace.inner_single_right, conj_trivial, one_mul, evalCLM_apply_apply,
    fderivCLM_apply, PiLp.smul_apply, smul_eq_mul, mul_eq_mul_right_iff]e'_6d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumex:Space d⊢ deriv i (⇑η) x = (fderiv ℝ (⇑η) x) (basis i) ∨ (f x).ofLp i = 0
  lefte'_6d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumex:Space d⊢ deriv i (⇑η) x = (fderiv ℝ (⇑η) x) (basis i)
  rw [deriv_eq_fderiv_basise'_6d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin da✝:i ∈ Finset.univintegrable_lemma:∀ (i j : Fin d),
  Integrable (fun x => (((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) x • f x).ofLp j)
    volumex:Space d⊢ (fderiv ℝ (⇑η) x) (basis i) = (fderiv ℝ (⇑η) x) (basis i)All goals completed! 🐙]All goals completed! 🐙



lemma integrable_isDistBounded_inner_grad_schwartzMap_spherical {d : ℕ}
    {f : Space d → EuclideanSpace ℝ (Fin d)}
    (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) :
    Integrable ((fun x => ⟪f x.1, Space.grad η x.1⟫_ℝ)
      ∘ (homeomorphUnitSphereProd (Space d)).symm)
      ((volume (α := Space d)).toSphere.prod
      (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := byd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  have h1 : Integrable ((fun x => ⟪f x.1, Space.grad η x.1⟫_ℝ))
      (.comap (Subtype.val (p := fun x => x ∈ ({0}ᶜ : Set _))) volume) := by
    change Integrable ((fun x => ⟪f x, Space.grad η x⟫_ℝ) ∘ Subtype.val)
      (.comap (Subtype.val (p := fun x => x ∈ ({0}ᶜ : Set _))) volume)d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ Integrable ((fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) ∘ Subtype.val) (Measure.comap Subtype.val volume)d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    rw [← MeasureTheory.integrableOn_iff_comap_subtypeVald:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ IntegrableOn (fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) {0}ᶜ volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ MeasurableSet {0}ᶜd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ IntegrableOn (fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) {0}ᶜ volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ MeasurableSet {0}ᶜd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ IntegrableOn (fun x => ⟪f x, ∇ (⇑η) x⟫_ℝ) {0}ᶜ volumed:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ MeasurableSet {0}ᶜd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    exact (integrable_isDistBounded_inner_grad_schwartzMap hf η).integrableOnd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ MeasurableSet {0}ᶜd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
    simpd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  have he := (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
    (volume (α := Space d)))d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable ((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))
  rw [← he.integrable_comp_embd:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable
  (((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)h₂d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable
  (((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)h₂d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))]d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ Integrable
  (((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
  (Measure.comap Subtype.val volume)h₂d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))
  convert h1d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))x✝:↑{0}ᶜ⊢ (((fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) ∘ ⇑(homeomorphUnitSphereProd (Space d)).symm) ∘ ⇑(homeomorphUnitSphereProd (Space d)))
    x✝ =
  ⟪f ↑x✝, ∇ ⇑η ↑x✝⟫_ℝh₂d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))
  simp only [Function.comp_apply, Homeomorph.symm_apply_apply]h₂d:ℕf:Space d → EuclideanSpace ℝ (Fin d)hf:IsDistBounded fη:𝓢(Space d, ℝ)h1:Integrable (fun x => ⟪f ↑x, ∇ ⇑η ↑x⟫_ℝ) (Measure.comap Subtype.val volume)he:MeasurePreserving (⇑(homeomorphUnitSphereProd (Space d))) (Measure.comap Subtype.val volume)
  (volume.toSphere.prod (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)))⊢ MeasurableEmbedding ⇑(homeomorphUnitSphereProd (Space d))
  exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d))All goals completed! 🐙

A.14. Differentiability of gradient

@[fun_prop]
lemma contDiff_grad {n} {f : Space → ℝ} (hf : ContDiff ℝ (n + 1) f) :
    ContDiff ℝ n (fun x => ∇ f x) := byn:ℕ∞ωf:Space → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n fun x => ∇ f x
  unfold gradn:ℕ∞ωf:Space → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => deriv i f x
  apply ContDiff.fun_comphgn:ℕ∞ωf:Space → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n (WithLp.toLp 2)hfn:ℕ∞ωf:Space → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n fun x i => deriv i f x
  ·hgn:ℕ∞ωf:Space → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n (WithLp.toLp 2) fun_propAll goals completed! 🐙
  ·hfn:ℕ∞ωf:Space → ℝhf:ContDiff ℝ (n + 1) f⊢ ContDiff ℝ n fun x i => deriv i f x exact deriv_contDiff hfAll goals completed! 🐙

B. Gradient of distributions

B.1. The definition

@[inherit_doc distGrad]
scoped[Space] notation "∇ᵈ" => distGrad

B.2. The gradient of inner products



set_option backward.isDefEq.respectTransparency false in
lemma distGrad_inner_eq {d} (f : (Space d) →d[ℝ] ℝ) (η : 𝓢(Space d, ℝ))
    (y : EuclideanSpace ℝ (Fin d)) : ⟪∇ᵈ f η, y⟫_ℝ = fderivD ℝ f η (basis.repr.symm y) := byd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ = (((fderivD ℝ) f) η) (basis.repr.symm y)
  rw [distGradd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)⊢ ⟪({
          toFun := fun f =>
            LinearMap.toContinuousLinearMap ↑basis.repr.toLinearEquiv ∘SL
              LinearMap.toContinuousLinearMap ↑(toDual ℝ (Space d)).symm.toLinearEquiv ∘SL (fderivD ℝ) f,
          map_add' := ⋯, map_smul' := ⋯ }
        f)
      η,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)⊢ ⟪({
          toFun := fun f =>
            LinearMap.toContinuousLinearMap ↑basis.repr.toLinearEquiv ∘SL
              LinearMap.toContinuousLinearMap ↑(toDual ℝ (Space d)).symm.toLinearEquiv ∘SL (fderivD ℝ) f,
          map_add' := ⋯, map_smul' := ⋯ }
        f)
      η,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)]d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)⊢ ⟪({
          toFun := fun f =>
            LinearMap.toContinuousLinearMap ↑basis.repr.toLinearEquiv ∘SL
              LinearMap.toContinuousLinearMap ↑(toDual ℝ (Space d)).symm.toLinearEquiv ∘SL (fderivD ℝ) f,
          map_add' := ⋯, map_smul' := ⋯ }
        f)
      η,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)
  simp only [LinearIsometryEquiv.toLinearEquiv_symm, LinearMap.coe_mk, AddHom.coe_mk,
    ContinuousLinearMap.coe_comp, LinearMap.coe_toContinuousLinearMap', LinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.coe_symm_toLinearEquiv,
    Function.comp_apply, basis_repr_inner_eq, toDual_symm_apply]All goals completed! 🐙

lemma distGrad_eq_of_inner {d} (f : (Space d) →d[ℝ] ℝ)
    (g : (Space d) →d[ℝ] EuclideanSpace ℝ (Fin d))
    (h : ∀ η y, fderivD ℝ f η y = ⟪g η, basis.repr y⟫_ℝ) :
    ∇ᵈ f = g := byd:ℕf:(Space d)→d[ℝ] ℝg:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)h:∀ (η : 𝓢(Space d, ℝ)) (y : Space d), (((fderivD ℝ) f) η) y = ⟪g η, basis.repr y⟫_ℝ⊢ ∇ᵈ f = g
  ext1 ηd:ℕf:(Space d)→d[ℝ] ℝg:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)h:∀ (η : 𝓢(Space d, ℝ)) (y : Space d), (((fderivD ℝ) f) η) y = ⟪g η, basis.repr y⟫_ℝη:𝓢(Space d, ℝ)⊢ (∇ᵈ f) η = g η
  apply ext_inner_right (𝕜 := ℝ) fun v => ?_d:ℕf:(Space d)→d[ℝ] ℝg:(Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)h:∀ (η : 𝓢(Space d, ℝ)) (y : Space d), (((fderivD ℝ) f) η) y = ⟪g η, basis.repr y⟫_ℝη:𝓢(Space d, ℝ)v:EuclideanSpace ℝ (Fin d)⊢ ⟪(∇ᵈ f) η, v⟫_ℝ = ⟪g η, v⟫_ℝ
  simp [distGrad_inner_eq, h]All goals completed! 🐙

B.3. The gradient as a sum over basis vectors



lemma distGrad_eq_sum_basis {d} (f : (Space d) →d[ℝ] ℝ) (η : 𝓢(Space d, ℝ)) :
    ∇ᵈ f η =
      ∑ i, - f (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i) (fderivCLM ℝ (Space d) ℝ η)) •
      EuclideanSpace.single i 1 := byd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)⊢ (∇ᵈ f) η =
  ∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1
  refine ext_inner_right (𝕜 := ℝ) fun y => ?_d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
  have h1 : ⟪∑ i, - f (SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i) (fderivCLM ℝ (Space d) ℝ η)) •
        EuclideanSpace.single i 1, y⟫_ℝ =
      fderivD ℝ f η (basis.repr.symm y) := byd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)⊢ (∇ᵈ f) η =
  ∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
    have hy : y = ∑ i, y i • EuclideanSpace.single i 1 := byd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)⊢ (∇ᵈ f) η =
  ∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
      conv_lhs => rw [← OrthonormalBasis.sum_repr (EuclideanSpace.basisFun (Fin d) ℝ) y]d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)| ∑ i, ((EuclideanSpace.basisFun (Fin d) ℝ).repr y).ofLp i • (EuclideanSpace.basisFun (Fin d) ℝ) id:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
      simpd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
    rw [hyd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    ∑ i, y.ofLp i • EuclideanSpace.single i 1⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm (∑ i, y.ofLp i • EuclideanSpace.single i 1))d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    ∑ i, y.ofLp i • EuclideanSpace.single i 1⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm (∑ i, y.ofLp i • EuclideanSpace.single i 1))d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ]d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)hy:y = ∑ i, y.ofLp i • EuclideanSpace.single i 1⊢ ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    ∑ i, y.ofLp i • EuclideanSpace.single i 1⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm (∑ i, y.ofLp i • EuclideanSpace.single i 1))d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
    simp [PiLp.inner_apply, RCLike.inner_apply, conj_trivial, map_sum, map_smul, smul_eq_mul,
      Pi.single_apply, fderivD_apply]d:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝd:ℕf:(Space d)→d[ℝ] ℝη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin d)h1:⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ =
  (((fderivD ℝ) f) η) (basis.repr.symm y)⊢ ⟪(∇ᵈ f) η, y⟫_ℝ =
  ⟪∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) η)) • EuclideanSpace.single i 1,
    y⟫_ℝ
  exact (distGrad_inner_eq f η y).trans h1.symmAll goals completed! 🐙

B.4. The underlying function of the gradient distribution



lemma distGrad_toFun_eq_distDeriv {d} (f : (Space d) →d[ℝ] ℝ) :
    (∇ᵈ f).toFun = fun ε => WithLp.toLp 2 fun i => ∂ᵈ[i] f ε := byd:ℕf:(Space d)→d[ℝ] ℝ⊢ (↑(∇ᵈ f)).toFun = fun ε => WithLp.toLp 2 fun i => ((distDeriv i) f) ε
  ext ε id:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)i:Fin d⊢ ((↑(∇ᵈ f)).toFun ε).ofLp i = (WithLp.toLp 2 fun i => ((distDeriv i) f) ε).ofLp i
  simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ContinuousLinearMap.coe_coe]d:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)i:Fin d⊢ ((∇ᵈ f) ε).ofLp i = ((distDeriv i) f) ε
  rw [distGrad_eq_sum_basisd:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)i:Fin d⊢ (∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ε)) • EuclideanSpace.single i 1).ofLp
    i =
  ((distDeriv i) f) εd:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)i:Fin d⊢ (∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ε)) • EuclideanSpace.single i 1).ofLp
    i =
  ((distDeriv i) f) ε]d:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)i:Fin d⊢ (∑ i, -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ε)) • EuclideanSpace.single i 1).ofLp
    i =
  ((distDeriv i) f) ε
  simp only [neg_smul, Finset.sum_neg_distrib, PiLp.neg_apply, WithLp.ofLp_sum, WithLp.ofLp_smul,
    PiLp.ofLp_single, Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_eq_mul,
    mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]d:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)i:Fin d⊢ -f ((SchwartzMap.evalCLM ℝ (Space d) ℝ (basis i)) ((fderivCLM ℝ (Space d) ℝ) ε)) = ((distDeriv i) f) ε
  rflAll goals completed! 🐙

B.5. The gradient applied to a Schwartz function



lemma distGrad_apply {d} (f : (Space d) →d[ℝ] ℝ) (ε : 𝓢(Space d, ℝ)) :
    (∇ᵈ f) ε = fun i => ∂ᵈ[i] f ε := byd:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)⊢ ((∇ᵈ f) ε).ofLp = fun i => ((distDeriv i) f) ε
  change (∇ᵈ f).toFun ε = fun i => ∂ᵈ[i] f εd:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)⊢ ((↑(∇ᵈ f)).toFun ε).ofLp = fun i => ((distDeriv i) f) ε
  rw [distGrad_toFun_eq_distDerivd:ℕf:(Space d)→d[ℝ] ℝε:𝓢(Space d, ℝ)⊢ ((fun ε => WithLp.toLp 2 fun i => ((distDeriv i) f) ε) ε).ofLp = fun i => ((distDeriv i) f) εAll goals completed! 🐙]All goals completed! 🐙

B.6. Gradient of constant distributions

@[simp]
lemma distGrad_const {d} (c : ℝ) :
    ∇ᵈ (Distribution.const ℝ (Space d) c) = 0 := byd:ℕc:ℝ⊢ ∇ᵈ (const ℝ (Space d) c) = 0
  ext ε id:ℕc:ℝε:𝓢(Space d, ℝ)i:Fin d⊢ ((∇ᵈ (const ℝ (Space d) c)) ε).ofLp i = (0 ε).ofLp i
  simp [distGrad_apply, distDeriv_apply, Distribution.fderivD_const]All goals completed! 🐙

B.7. The gradient of a Schwartz map

lemma gradSchwartz_apply_eq_grad {d} (η : 𝓢(Space d, ℝ)) (x : Space d) :
    gradSchwartz η x = ∇ η x := byd:ℕη:𝓢(Space d, ℝ)x:Space d⊢ (gradSchwartz η) x = ∇ (⇑η) x
  simp [gradSchwartz, grad_eq_sum]d:ℕη:𝓢(Space d, ℝ)x:Space d⊢ ∑ x_1, (fderiv ℝ (⇑η) x) (basis x_1) • EuclideanSpace.single x_1 1 = ∑ i, deriv i (⇑η) x • EuclideanSpace.single i 1
  rflAll goals completed! 🐙

Gradient of functions and distributions on Space d

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The gradient of functions on Space d

A.1. Gradient of the zero function

A.2. Gradient distributes over addition

A.3. Gradient of a constant function

A.4. Gradient distributes over scalar multiplication

A.5. Gradient distributes over negation

A.6. Expansion in terms of basis vectors

A.7. Components of the gradient

A.8. Inner product with a gradient

A.9. Gradient is equal to gradient from Mathlib

A.10. Value of gradient in the direction of the position vector

A.11. Gradient of the norm squared function

A.12. Gradient of the inner product function

A.13. Integrability with bounded functions

A.14. Differentiability of gradient

B. Gradient of distributions

B.1. The definition

B.2. The gradient of inner products

B.3. The gradient as a sum over basis vectors

B.4. The underlying function of the gradient distribution

B.5. The gradient applied to a Schwartz function

B.6. Gradient of constant distributions

B.7. The gradient of a Schwartz map

Gradient of functions and distributions on `Space d`

A. The gradient of functions on `Space d`

A.9. Gradient is equal to `gradient` from Mathlib