Physlib.Mathematics.VariationalCalculus.IsTestFunction

Imports

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

public import Physlib.Mathematics.Calculus.Divergence
public import Mathlib.Topology.ContinuousMap.CompactlySupported

Test functions

Definition of test function, smooth and compactly supported function, and theorems about them.

@[expose] public section

A test function is a smooth function with compact support.

@[fun_prop]
structure IsTestFunction (f : X → U) where
  smooth : ContDiff ℝ ∞ f
  supp : HasCompactSupport f

A compactly supported continuous map from a test function.

def IsTestFunction.toCompactlySupportedContinuousMap {f : X → U}
    (hf : IsTestFunction f) : CompactlySupportedContinuousMap X U where
  toFun := f
  hasCompactSupport' := hf.supp
  continuous_toFun := hf.smooth.continuous

              lemma IsTestFunction.of_compactlySupportedContinuousMap {f : CompactlySupportedContinuousMap X U}
    (hf : ContDiff ℝ ∞ f) :
    IsTestFunction f.toFun where
  smooth := hf
  supp := f.hasCompactSupport'@[fun_prop]
lemma IsTestFunction.integrable [MeasurableSpace X] [OpensMeasurableSpace X]
    {f : X → U} (hf : IsTestFunction f)
    (μ : Measure X) [IsFiniteMeasureOnCompacts μ] :
    MeasureTheory.Integrable f μ :=
  Continuous.integrable_of_hasCompactSupport (continuous hf.smooth) hf.supp@[fun_prop]
lemma IsTestFunction.differentiable {f : X → U} (hf : IsTestFunction f) :
    Differentiable ℝ f := hf.1.differentiable (byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ∞ ≠ 0 simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.contDiff {f : X → U} (hf : IsTestFunction f) :
    ContDiff ℝ ∞ f := hf.1@[fun_prop]
lemma IsTestFunction.zero :
    IsTestFunction (fun _ : X => (0 : U)) where
  smooth := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ U⊢ ContDiff ℝ ∞ fun x => 0 fun_propAll goals completed! 🐙
  supp := HasCompactSupport.zero

@[fun_prop]
lemma IsTestFunction.comp_left {f : X → V} (hf : IsTestFunction f)
    {g : V → U} (hg1 : g 0 = 0) (hg : ContDiff ℝ ∞ g) :
    IsTestFunction (fun x => g (f x)) where
  smooth := ContDiff.comp hg hf.smooth
  supp := byX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V → Uhg1:g 0 = 0hg:ContDiff ℝ ∞ g⊢ HasCompactSupport fun x => g (f x)
    obtain ⟨K, cK, hK⟩ := exists_compact_iff_hasCompactSupport.mpr hf.suppX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V → Uhg1:g 0 = 0hg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0⊢ HasCompactSupport fun x => g (f x)
    refine exists_compact_iff_hasCompactSupport.mp ⟨K, cK, fun x hx => ?_⟩X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V → Uhg1:g 0 = 0hg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ g (f x) = 0
    rw [hK x hxX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V → Uhg1:g 0 = 0hg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ g 0 = 0X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V → Uhg1:g 0 = 0hg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ g 0 = 0]X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V → Uhg1:g 0 = 0hg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ g 0 = 0
    exact hg1All goals completed! 🐙@[fun_prop]
lemma IsTestFunction.pi {ι} [Fintype ι] {φ : X → ι → U} (hφ : ∀ i, IsTestFunction (φ · i)) :
    IsTestFunction (fun x i => φ x i) where
  smooth := contDiff_pi' (fun i => (hφ i).smooth)
  supp := byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x i⊢ HasCompactSupport fun x i => φ x i
    let K : ι → Set X := fun i =>
      Classical.choose (exists_compact_iff_hasCompactSupport.mpr (hφ i).supp)X:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x iK:ι → Set X := fun i => Classical.choose ⋯⊢ HasCompactSupport fun x i => φ x i
    have hK (i : ι) := Classical.choose_spec (exists_compact_iff_hasCompactSupport.mpr (hφ i).supp)X:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x iK:ι → Set X := fun i => Classical.choose ⋯hK:∀ (i : ι), IsCompact (Classical.choose ⋯) ∧ ∀ x ∉ Classical.choose ⋯, φ x i = 0⊢ HasCompactSupport fun x i => φ x i
    refine exists_compact_iff_hasCompactSupport.mp
      ⟨⋃ i, K i, isCompact_iUnion (fun i => (hK i).1), fun x hx => ?_⟩X:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x iK:ι → Set X := fun i => Classical.choose ⋯hK:∀ (i : ι), IsCompact (Classical.choose ⋯) ∧ ∀ x ∉ Classical.choose ⋯, φ x i = 0x:Xhx:x ∉ ⋃ i, K i⊢ (fun i => φ x i) = 0
    simp at hxX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x iK:ι → Set X := fun i => Classical.choose ⋯hK:∀ (i : ι), IsCompact (Classical.choose ⋯) ∧ ∀ x ∉ Classical.choose ⋯, φ x i = 0x:Xhx:∀ (x_1 : ι), x ∉ K x_1⊢ (fun i => φ x i) = 0
    conv_lhs =>
      enter [i]X:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x iK:ι → Set X := fun i => Classical.choose ⋯hK:∀ (i : ι), IsCompact (Classical.choose ⋯) ∧ ∀ x ∉ Classical.choose ⋯, φ x i = 0x:Xhx:∀ (x_1 : ι), x ∉ K x_1i:ι| φ x i
      rw [(hK i).2 x (hx i)]X:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x iK:ι → Set X := fun i => Classical.choose ⋯hK:∀ (i : ι), IsCompact (Classical.choose ⋯) ∧ ∀ x ∉ Classical.choose ⋯, φ x i = 0x:Xhx:∀ (x_1 : ι), x ∉ K x_1i:ι| 0
    rflAll goals completed! 🐙

lemma IsTestFunction.space_component {φ : X → Space d} (hφ : IsTestFunction φ) :
    IsTestFunction (fun x => φ x i) where
  smooth := byX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φ⊢ ContDiff ℝ ∞ fun x => (φ x).val i
    have hφ := hφ.smoothX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ✝:IsTestFunction φhφ:ContDiff ℝ ∞ φ⊢ ContDiff ℝ ∞ fun x => (φ x).val i
    fun_propAll goals completed! 🐙
  supp := byX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φ⊢ HasCompactSupport fun x => (φ x).val i
    obtain ⟨K, cK, hK⟩ := exists_compact_iff_hasCompactSupport.mpr hφ.suppX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φK:Set XcK:IsCompact KhK:∀ x ∉ K, φ x = 0⊢ HasCompactSupport fun x => (φ x).val i
    refine exists_compact_iff_hasCompactSupport.mp ⟨K, cK, fun x hx => ?_⟩X:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φK:Set XcK:IsCompact KhK:∀ x ∉ K, φ x = 0x:Xhx:x ∉ K⊢ (φ x).val i = 0
    rw [hK x hxX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φK:Set XcK:IsCompact KhK:∀ x ∉ K, φ x = 0x:Xhx:x ∉ K⊢ Space.val 0 i = 0X:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φK:Set XcK:IsCompact KhK:∀ x ∉ K, φ x = 0x:Xhx:x ∉ K⊢ Space.val 0 i = 0]X:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕi:Fin dφ:X → Space dhφ:IsTestFunction φK:Set XcK:IsCompact KhK:∀ x ∉ K, φ x = 0x:Xhx:x ∉ K⊢ Space.val 0 i = 0
    simpAll goals completed! 🐙@[fun_prop]
lemma IsTestFunction.prodMk {f : X → U} {g : X → V}
    (hf : IsTestFunction f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => (f x, g x)) where
  smooth := byX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_2inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_3inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Ug:X → Vhf:IsTestFunction fhg:IsTestFunction g⊢ ContDiff ℝ ∞ fun x => (f x, g x) fun_propAll goals completed! 🐙
  supp := byX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_2inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_3inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Ug:X → Vhf:IsTestFunction fhg:IsTestFunction g⊢ HasCompactSupport fun x => (f x, g x)
    obtain ⟨Kf, cKf, hKf⟩ := exists_compact_iff_hasCompactSupport.mpr hf.suppX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_2inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_3inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Ug:X → Vhf:IsTestFunction fhg:IsTestFunction gKf:Set XcKf:IsCompact KfhKf:∀ x ∉ Kf, f x = 0⊢ HasCompactSupport fun x => (f x, g x)
    obtain ⟨Kg, cKg, hKg⟩ := exists_compact_iff_hasCompactSupport.mpr hg.suppX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_2inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_3inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Ug:X → Vhf:IsTestFunction fhg:IsTestFunction gKf:Set XcKf:IsCompact KfhKf:∀ x ∉ Kf, f x = 0Kg:Set XcKg:IsCompact KghKg:∀ x ∉ Kg, g x = 0⊢ HasCompactSupport fun x => (f x, g x)
    refine exists_compact_iff_hasCompactSupport.mp
      ⟨Kf ∪ Kg, IsCompact.union cKf cKg, fun x hx => ?_⟩X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_2inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_3inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Ug:X → Vhf:IsTestFunction fhg:IsTestFunction gKf:Set XcKf:IsCompact KfhKf:∀ x ∉ Kf, f x = 0Kg:Set XcKg:IsCompact KghKg:∀ x ∉ Kg, g x = 0x:Xhx:x ∉ Kf ∪ Kg⊢ (f x, g x) = 0
    simp at hxX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_2inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_3inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Ug:X → Vhf:IsTestFunction fhg:IsTestFunction gKf:Set XcKf:IsCompact KfhKf:∀ x ∉ Kf, f x = 0Kg:Set XcKg:IsCompact KghKg:∀ x ∉ Kg, g x = 0x:Xhx:x ∉ Kf ∧ x ∉ Kg⊢ (f x, g x) = 0
    simp [hKf x hx.1, hKg x hx.2]All goals completed! 🐙@[fun_prop]
lemma IsTestFunction.prod_fst {f : X → U × V} (hf : IsTestFunction f) :
    IsTestFunction (fun x => (f x).1) := byX:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_1inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → U × Vhf:IsTestFunction f⊢ IsTestFunction fun x => (f x).1 fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.prod_snd {f : X → U × V} (hf : IsTestFunction f) :
    IsTestFunction (fun x => (f x).2) := byX:Type u_3inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_1inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → U × Vhf:IsTestFunction f⊢ IsTestFunction fun x => (f x).2 fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.neg {f : X → U} (hf : IsTestFunction f) :
    IsTestFunction (fun x => - f x) := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ IsTestFunction fun x => -f x fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.add {f g : X → U} (hf : IsTestFunction f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => f x + g x) := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Ug:X → Uhf:IsTestFunction fhg:IsTestFunction g⊢ IsTestFunction fun x => f x + g x fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.sub {f g : X → U} (hf : IsTestFunction f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => f x - g x) := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Ug:X → Uhf:IsTestFunction fhg:IsTestFunction g⊢ IsTestFunction fun x => f x - g x fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.mul {f g : X → ℝ} (hf : IsTestFunction f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => f x * g x) := byX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xf:X → ℝg:X → ℝhf:IsTestFunction fhg:IsTestFunction g⊢ IsTestFunction fun x => f x * g x fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.mul_left {f g : X → ℝ} (hf : ContDiff ℝ ∞ f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => f x * g x) where
  smooth := ContDiff.mul hf hg.smooth
  supp := HasCompactSupport.mul_left hg.supp@[fun_prop]
lemma IsTestFunction.mul_right {f g : X → ℝ} (hf : IsTestFunction f) (hg : ContDiff ℝ ∞ g) :
    IsTestFunction (fun x => f x * g x) where
  smooth := ContDiff.mul hf.smooth hg
  supp := HasCompactSupport.mul_right hf.supp@[fun_prop]
lemma IsTestFunction.inner [InnerProductSpace' ℝ V]
    {f g : X → V} (hf : IsTestFunction f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => ⟪f x, g x⟫_ℝ) := byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:IsTestFunction fhg:IsTestFunction g⊢ IsTestFunction fun x => ⟪f x, g x⟫_ℝ fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.inner_left [InnerProductSpace' ℝ V]
    {f : X → V} {g : X → V} (hf : ContDiff ℝ ∞ f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => ⟪f x, g x⟫_ℝ) where
  smooth := ContDiff.inner' hf hg.smooth
  supp := byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:ContDiff ℝ ∞ fhg:IsTestFunction g⊢ HasCompactSupport fun x => ⟪f x, g x⟫_ℝ
    obtain ⟨K, cK, hK⟩ := exists_compact_iff_hasCompactSupport.mpr hg.suppX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:ContDiff ℝ ∞ fhg:IsTestFunction gK:Set XcK:IsCompact KhK:∀ x ∉ K, g x = 0⊢ HasCompactSupport fun x => ⟪f x, g x⟫_ℝ
    exact exists_compact_iff_hasCompactSupport.mp ⟨K, cK, fun x hx => byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:ContDiff ℝ ∞ fhg:IsTestFunction gK:Set XcK:IsCompact KhK:∀ x ∉ K, g x = 0x:Xhx:x ∉ K⊢ ⟪f x, g x⟫_ℝ = 0 simp [hK x hx]All goals completed! 🐙⟩    -- HasCompactSupport.inner_left hf hg.supp

@[fun_prop]
lemma IsTestFunction.inner_right [InnerProductSpace' ℝ V]
    {f : X → V} {g : X → V} (hf : IsTestFunction f) (hg : ContDiff ℝ ∞ g) :
    IsTestFunction (fun x => ⟪f x, g x⟫_ℝ) where
  smooth := ContDiff.inner' hf.smooth hg
  supp := byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:IsTestFunction fhg:ContDiff ℝ ∞ g⊢ HasCompactSupport fun x => ⟪f x, g x⟫_ℝ
    obtain ⟨K, cK, hK⟩ := exists_compact_iff_hasCompactSupport.mpr hf.suppX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:IsTestFunction fhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0⊢ HasCompactSupport fun x => ⟪f x, g x⟫_ℝ
    exact exists_compact_iff_hasCompactSupport.mp ⟨K, cK, fun x hx => byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XV:Type u_1inst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:InnerProductSpace' ℝ Vf:X → Vg:X → Vhf:IsTestFunction fhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ ⟪f x, g x⟫_ℝ = 0 simp [hK x hx]All goals completed! 🐙⟩    -- HasCompactSupport.inner_right hf.supp hg

@[fun_prop]
lemma IsTestFunction.smul {f : X → ℝ} {g : X → U} (hf : IsTestFunction f) (hg : IsTestFunction g) :
    IsTestFunction (fun x => f x • g x) := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → ℝg:X → Uhf:IsTestFunction fhg:IsTestFunction g⊢ IsTestFunction fun x => f x • g x fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.smul_left {f : X → ℝ} {g : X → U}
    (hf : ContDiff ℝ ∞ f) (hg : IsTestFunction g) : IsTestFunction (fun x => f x • g x) where
  smooth := ContDiff.smul hf hg.smooth
  supp := HasCompactSupport.smul_left hg.supp@[fun_prop]
lemma IsTestFunction.smul_right {f : X → ℝ} {g : X → U}
    (hf : IsTestFunction f) (hg : ContDiff ℝ ∞ g) : IsTestFunction (fun x => f x • g x) where
  smooth := ContDiff.smul hf.smooth hg
  supp := HasCompactSupport.smul_right hf.supp@[fun_prop]
lemma IsTestFunction.sum {ι} [Fintype ι] {φ : X → ι → U} {hφ : ∀ i, IsTestFunction (φ · i)} :
    IsTestFunction (fun x => ∑ i, φ x i) := byX:Type u_2inst✝⁴:NormedAddCommGroup Xinst✝³:NormedSpace ℝ XU:Type u_3inst✝²:NormedAddCommGroup Uinst✝¹:NormedSpace ℝ Uι:Type u_1inst✝:Fintype ιφ:X → ι → Uhφ:∀ (i : ι), IsTestFunction fun x => φ x i⊢ IsTestFunction fun x => ∑ i, φ x i fun_prop (disch:=simpAll goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.coord {φ : X → Space d} (hφ : IsTestFunction φ) (i : Fin d) :
    IsTestFunction (fun x => (φ x).coord i) := byX:Type u_1inst✝¹:NormedAddCommGroup Xinst✝:NormedSpace ℝ Xd:ℕφ:X → Space dhφ:IsTestFunction φi:Fin d⊢ IsTestFunction fun x => Space.coord i (φ x) fun_prop (disch:=simp[Space.coord]All goals completed! 🐙)@[fun_prop]
lemma IsTestFunction.linearMap_comp {f : X → V} (hf : IsTestFunction f)
    {g : V →ₗ[ℝ] U} (hg : ContDiff ℝ ∞ g) :
    IsTestFunction (fun x => g (f x)) := byX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:V →ₗ[ℝ] Uhg:ContDiff ℝ ∞ ⇑g⊢ IsTestFunction fun x => g (f x) fun_prop (disch:=simpAll goals completed! 🐙)

@[fun_prop]
lemma IsTestFunction.family_linearMap_comp {f : X → V} (hf : IsTestFunction f)
    {g : X → V →L[ℝ] U} (hg : ContDiff ℝ ∞ g) :
    IsTestFunction (fun x => g x (f x)) where
  smooth := byX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ fun x => (g x) (f x)
    fun_propAll goals completed! 🐙
  supp := byX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ g⊢ HasCompactSupport fun x => (g x) (f x)
    have hf' := hf.suppX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ ghf':HasCompactSupport f⊢ HasCompactSupport fun x => (g x) (f x)
    rw [← exists_compact_iff_hasCompactSupportX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ ghf':∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0⊢ ∃ K, IsCompact K ∧ ∀ x ∉ K, (g x) (f x) = 0X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ ghf':∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0⊢ ∃ K, IsCompact K ∧ ∀ x ∉ K, (g x) (f x) = 0] at hf' ⊢X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ ghf':∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0⊢ ∃ K, IsCompact K ∧ ∀ x ∉ K, (g x) (f x) = 0
    obtain ⟨K, cK, hK⟩ := hf'X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0⊢ ∃ K, IsCompact K ∧ ∀ x ∉ K, (g x) (f x) = 0
    refine ⟨K, cK, fun x hx => ?_⟩X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ (g x) (f x) = 0
    rw [hK x hxX:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ (g x) 0 = 0X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ (g x) 0 = 0]X:Type u_1inst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace ℝ XU:Type u_3inst✝³:NormedAddCommGroup Uinst✝²:NormedSpace ℝ UV:Type u_2inst✝¹:NormedAddCommGroup Vinst✝:NormedSpace ℝ Vf:X → Vhf:IsTestFunction fg:X → V →L[ℝ] Uhg:ContDiff ℝ ∞ gK:Set XcK:IsCompact KhK:∀ x ∉ K, f x = 0x:Xhx:x ∉ K⊢ (g x) 0 = 0
    simpAll goals completed! 🐙@[fun_prop]
lemma IsTestFunction.deriv {f : ℝ → U} (hf : IsTestFunction f) :
    IsTestFunction (fun x => deriv f x) where
  smooth := deriv' hf.smooth
  supp := HasCompactSupport.deriv hf.supp@[fun_prop]
lemma IsTestFunction.of_fderiv {f : X → U} (hf : IsTestFunction f) :
    IsTestFunction (fderiv ℝ f ·) where
  smooth := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ContDiff ℝ ∞ fun x => fderiv ℝ f x
    apply ContDiff.fderiv (m := ∞)hfX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ContDiff ℝ ∞ (Function.uncurry fun x => f)hgX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ContDiff ℝ ∞ fun x => xhnmX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ∞ + 1 ≤ ∞
    ·hfX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ContDiff ℝ ∞ (Function.uncurry fun x => f) fun_propAll goals completed! 🐙
    ·hgX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ContDiff ℝ ∞ fun x => x fun_propAll goals completed! 🐙
    ·hnmX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ ∞ + 1 ≤ ∞ exact Preorder.le_refl (∞ + 1)All goals completed! 🐙
  supp := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ HasCompactSupport fun x => fderiv ℝ f x
    apply HasCompactSupport.fderivX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction f⊢ HasCompactSupport f
    exact hf.suppAll goals completed! 🐙@[fun_prop]
lemma IsTestFunction.fderiv_apply {f : X → U} (hf : IsTestFunction f) (δx : X) :
    IsTestFunction (fderiv ℝ f · δx) where
  smooth := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ fun x => (fderiv ℝ f x) δx
    apply ContDiff.fderiv_apply (m := ∞)hfX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ (Function.uncurry fun x => f)hgX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ fun x => xhkX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ fun x => δxhnmX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ∞ + 1 ≤ ∞
    ·hfX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ (Function.uncurry fun x => f) fun_propAll goals completed! 🐙
    ·hgX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ fun x => x fun_propAll goals completed! 🐙
    ·hkX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ContDiff ℝ ∞ fun x => δx fun_propAll goals completed! 🐙
    ·hnmX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ ∞ + 1 ≤ ∞ exact Preorder.le_refl (∞ + 1)All goals completed! 🐙
  supp := byX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ HasCompactSupport fun x => (fderiv ℝ f x) δx
    apply HasCompactSupport.fderiv_applyX:Type u_1inst✝³:NormedAddCommGroup Xinst✝²:NormedSpace ℝ XU:Type u_2inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → Uhf:IsTestFunction fδx:X⊢ HasCompactSupport f
    exact hf.suppAll goals completed! 🐙

@[fun_prop]
lemma IsTestFunction.divergence {f : X → X} [FiniteDimensional ℝ X] (hf : IsTestFunction f) :
    IsTestFunction (fun x => divergence ℝ f x) := byX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction f⊢ IsTestFunction fun x => _root_.divergence ℝ f x
  obtain ⟨s, ⟨bX⟩⟩ := Basis.exists_basis ℝ XX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ X⊢ IsTestFunction fun x => _root_.divergence ℝ f x
  haveI : Fintype s := FiniteDimensional.fintypeBasisIndex bXX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑s⊢ IsTestFunction fun x => _root_.divergence ℝ f x
  conv_rhs =>
    enter [x]X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑sx:X| _root_.divergence ℝ f x
    rw [divergence_eq_sum_fderiv' bX]X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑sx:X| (fun x => ∑ i, (bX.repr ((fderiv ℝ f x) (bX i))) i) x
  apply IsTestFunction.sumX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑s⊢ ∀ (i : ↑s), IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i
  intro iX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑s⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i
  let reprMap : X →ₗ[ℝ] ℝ := {
      toFun := (bX.repr · i)
      map_add' := byX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑s⊢ ∀ (x y : X), (bX.repr (x + y)) i = (bX.repr x) i + (bX.repr y) iX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i simpAll goals completed! 🐙X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i
      map_smul' := byX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑s⊢ ∀ (m : ℝ) (x : X), (bX.repr (m • x)) i = (RingHom.id ℝ) m • (bX.repr x) iX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i simpAll goals completed! 🐙X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i

    }X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i
  let f' : X →L[ℝ] ℝ := reprMap.toContinuousLinearMapX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMap⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i
  have h_trace_contDiff : ContDiff ℝ ∞ f' := f'.contDiffX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ IsTestFunction fun x => (bX.repr ((fderiv ℝ f x) (bX i))) i
  change IsTestFunction (fun x => f' ((fderiv ℝ f x) (bX i)))X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ IsTestFunction fun x => f' ((fderiv ℝ f x) (bX i))
  apply IsTestFunction.comp_left
    (f:=fun x : X => (fderiv ℝ f x) (bX i)) (g:=f')hfX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ IsTestFunction fun x => (fderiv ℝ f x) (bX i)hg1X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ f' 0 = 0hgX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ ContDiff ℝ ∞ ⇑f'
  ·hfX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ IsTestFunction fun x => (fderiv ℝ f x) (bX i) fun_propAll goals completed! 🐙
  ·hg1X:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ f' 0 = 0 simp [f']All goals completed! 🐙
  ·hgX:Type u_1inst✝²:NormedAddCommGroup Xinst✝¹:NormedSpace ℝ Xf:X → Xinst✝:FiniteDimensional ℝ Xhf:IsTestFunction fs:Set XbX:Basis ↑s ℝ Xthis:Fintype ↑si:↑sreprMap:X →ₗ[ℝ] ℝ := { toFun := fun x => (bX.repr x) i, map_add' := ⋯, map_smul' := ⋯ }f':X →L[ℝ] ℝ := LinearMap.toContinuousLinearMap reprMaph_trace_contDiff:ContDiff ℝ ∞ ⇑f'⊢ ContDiff ℝ ∞ ⇑f' exact h_trace_contDiffAll goals completed! 🐙@[fun_prop]
lemma IsTestFunction.gradient {d : ℕ} (φ : Space d → ℝ)
    (hφ : IsTestFunction φ) :
    IsTestFunction (gradient φ) := byd:ℕφ:Space d → ℝhφ:IsTestFunction φ⊢ IsTestFunction (_root_.gradient φ)
  have h := fun x => gradient_eq_adjFDeriv (hφ.differentiable x)d:ℕφ:Space d → ℝhφ:IsTestFunction φh:∀ (x : Space d), _root_.gradient φ x = _root_.adjFDeriv ℝ φ x 1⊢ IsTestFunction (_root_.gradient φ)
  eta_expandd:ℕφ:Space d → ℝhφ:IsTestFunction φh:∀ (x : Space d), _root_.gradient φ x = _root_.adjFDeriv ℝ φ x 1⊢ IsTestFunction fun x => _root_.gradient (fun a => φ a) x; simp[h]d:ℕφ:Space d → ℝhφ:IsTestFunction φh:∀ (x : Space d), _root_.gradient φ x = _root_.adjFDeriv ℝ φ x 1⊢ IsTestFunction fun x => _root_.adjFDeriv ℝ φ x 1
  fun_propAll goals completed! 🐙@[fun_prop]
lemma IsTestFunction.of_div {d : ℕ} (φ : Space d → EuclideanSpace ℝ (Fin d))
    (hφ : IsTestFunction φ) :
    IsTestFunction (Space.div φ) := byd:ℕφ:Space d → EuclideanSpace ℝ (Fin d)hφ:IsTestFunction φ⊢ IsTestFunction (Space.div φ)
  unfold Space.div Space.derivd:ℕφ:Space d → EuclideanSpace ℝ (Fin d)hφ:IsTestFunction φ⊢ IsTestFunction fun x => ∑ i, (fderiv ℝ (fun x => (φ x).ofLp i) x) (Space.basis i); dsimpd:ℕφ:Space d → EuclideanSpace ℝ (Fin d)hφ:IsTestFunction φ⊢ IsTestFunction fun x => ∑ i, (fderiv ℝ (fun x => (φ x).ofLp i) x) (Space.basis i); fun_prop (disch:=simpAll goals completed! 🐙)