awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
hbc :
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
        (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
        (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)

Tactic:
apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le

Premises used: Real, ContinuousLinearMap.norm_compContinuousMultilinearMap_le, ContinuousLinearMap.restrictScalars
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) =
    ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
h₁ : 0 ≤ ‖L‖
grw grw₁ :
  HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
grw [le_seminorm 𝕜 k n f x]

Premises used: SchwartzMap.le_seminorm
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
_ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
_₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
_₂ :
  ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) =
    ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
_₃ :
  ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
calc
    _ = ‖x‖ ^ k * ‖(L.restrictScalars ℝ).compContinuousMultilinearMap
        (iteratedFDeriv ℝ n f x)‖ := by
      congr
      exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)
    _ ≤ ‖x‖ ^ k * (‖L‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le
    _ = ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by ring
    _ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f := by
      grw [le_seminorm 𝕜 k n f x]

Premises used: Norm.norm, Real, ContinuousLinearMap.restrictScalars, HMul.hMul, ContinuousLinearMap.compContinuousMultilinearMap, SchwartzMap.seminorm, HPow.hPow, iteratedFDeriv, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : 𝓢(E, F)
x : E
⊢ Eq.{u_7 + 1} (α := G) ((((postcompCLM L : (a : 𝓢(E, F)) → 𝓢(E, G)) f : 𝓢(E, G)) : (a : E) → G) x : G)
    ((L : (a : F) → G) ((f : (a : E) → F) x : F) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L₁ : F →L[𝕜] G
L₂ : G →L[𝕜] H
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, H))
    ((postcompCLM L₂ : (a : 𝓢(E, G)) → 𝓢(E, H)) ((postcompCLM L₁ : (a : 𝓢(E, F)) → 𝓢(E, G)) f) : 𝓢(E, H))
    ((postcompCLM (L₂ ∘SL L₁) : (a : 𝓢(E, F)) → 𝓢(E, H)) f : 𝓢(E, H))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
a : E
⊢ Function.HasTemperateGrowth (F := E) fun (x : E) ↦ x - a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
a x x_1 : E
⊢ edist x x_1 ≤ (↑1 : ENNReal) * edist.{u_5} (α := E) ((fun (x : E) ↦ x - a) x) ((fun (x : E) ↦ x - a) x_1)

Tactic:
simp [edist_dist, dist_eq_norm]

Premises used: dist_eq_norm, edist_dist
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a x : E
⊢ Eq.{u_6 + 1} (α := F) ((((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((f : (a : E) → F) (x - a) : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_6 + 1} (α := F) ((((compSubConstCLM 𝕜 0 : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
      ((((ContinuousLinearMap.id 𝕜 𝓢(E, F) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (compSubConstCLM 𝕜 0) (ContinuousLinearMap.id 𝕜 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F) ((((compSubConstCLM 𝕜 0 : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((((ContinuousLinearMap.id 𝕜 𝓢(E, F) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b : E
h :
  ∀ (x : E),
    Eq.{u_6 + 1} (α := F)
      ((((compSubConstCLM 𝕜 b : (a : 𝓢(E, F)) → 𝓢(E, F)) ((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
      ((((compSubConstCLM 𝕜 (a + b) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
⊢ Eq (α := 𝓢(E, F))
    ((compSubConstCLM 𝕜 b : (a : 𝓢(E, F)) → 𝓢(E, F)) ((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f) : 𝓢(E, F))
    ((compSubConstCLM 𝕜 (a + b) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
h : Eq.{u_6 + 1} (α := F) ((f : (a : E) → F) (x - b - a) : F) ((f : (a : E) → F) (x - (a + b)) : F)
⊢ Eq.{u_6 + 1} (α := F)
    ((((compSubConstCLM 𝕜 b : (a : 𝓢(E, F)) → 𝓢(E, F)) ((compSubConstCLM 𝕜 a : (a : 𝓢(E, F)) → 𝓢(E, F)) f) : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((compSubConstCLM 𝕜 (a + b) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)

Tactic:
simp only [compSubConstCLM_apply]

Premises used: SchwartzMap.compSubConstCLM_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
h : x - b - a = x - (a + b)
⊢ Eq.{u_6 + 1} (α := F) ((f : (a : E) → F) (x - b - a) : F) ((f : (a : E) → F) (x - (a + b)) : F)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
⊢ x - b - a = x - (a + b)

Tactic:
(sub_add_eq_sub_sub_swap x a b).symm

Premises used: Eq.symm, sub_add_eq_sub_sub_swap
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
⊢ x - b - a = x - (a + b)

Tactic:
exact (sub_add_eq_sub_sub_swap x a b).symm

Premises used: Eq.symm, sub_add_eq_sub_sub_swap
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
V : Type u_9
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace ℝ D
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : NormedSpace 𝕜 V
inst_6 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
f : 𝓢(D, V)
k n : ℕ
⊢ ∫ (x : D),
      ‖x‖ ^ k *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_9} ℝ (fun (i : Fin n) ↦ D) V)
          (iteratedFDeriv ℝ n (⇑f : (a : D) → V) x) ∂μ ≤
    (HPow.hPow (α := ℝ) 2 μ.integrablePower * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑μ.integrablePower : ℝ)) ∂μ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(D, V)) → ℝ) f : ℝ)
        ((SchwartzMap.seminorm 𝕜 (k + μ.integrablePower) n : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
integral_pow_mul_le_of_le_of_pow_mul_le (norm_iteratedFDeriv_le_seminorm ℝ _ _)
    (le_seminorm ℝ _ _ _)

Premises used: Real, SchwartzMap.norm_iteratedFDeriv_le_seminorm, SchwartzMap.le_seminorm, integral_pow_mul_le_of_le_of_pow_mul_le
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
D : Type u_4
V : Type u_9
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_5 : BorelSpace D
inst_6 : SecondCountableTopology D
f : 𝓢(D, V)
k n : ℕ
⊢ Integrable (ε := ℝ)
    (fun (x : D) ↦
      ‖x‖ ^ k *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_9} ℝ (fun (i : Fin n) ↦ D) V)
          (iteratedFDeriv ℝ n (⇑f : (a : D) → V) x))
    μ

Tactic:
integrable_of_le_of_pow_mul_le (norm_iteratedFDeriv_le_seminorm ℝ _ _) (le_seminorm ℝ _ _ _)
    ((f.smooth ⊤).continuous_iteratedFDeriv (mod_cast le_top)).aestronglyMeasurable

Premises used: Real, SchwartzMap.norm_iteratedFDeriv_le_seminorm, SchwartzMap.le_seminorm, ContDiff.continuous_iteratedFDeriv, Top.top, Continuous.aestronglyMeasurable, SchwartzMap.smooth, integrable_of_le_of_pow_mul_le
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
D : Type u_4
V : Type u_9
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_5 : BorelSpace D
inst_6 : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
⊢ Integrable (ε := ℝ)
    (fun (x : D) ↦
      ‖x‖ ^ k *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_9} ℝ (fun (i : Fin 0) ↦ D) V)
          (iteratedFDeriv ℝ 0 (⇑f : (a : D) → V) x))
    μ

Tactic:
integrable_pow_mul_iteratedFDeriv μ f k 0

Premises used: OfNat.ofNat, SchwartzMap.integrable_pow_mul_iteratedFDeriv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
D : Type u_4
V : Type u_9
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_5 : BorelSpace D
inst_6 : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
h :
  ∀ (x : D),
    Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) =
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_9} ℝ (fun (i : Fin 0) ↦ D) V)
        (iteratedFDeriv ℝ 0 (⇑f : (a : D) → V) x)
⊢ Integrable (ε := ℝ) (fun (x : D) ↦ ‖x‖ ^ k * Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V)) μ

Tactic:
convert! integrable_pow_mul_iteratedFDeriv μ f k 0 with x

Premises used: OfNat.ofNat, SchwartzMap.integrable_pow_mul_iteratedFDeriv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
D : Type u_4
V : Type u_9
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_5 : BorelSpace D
inst_6 : SecondCountableTopology D
f : 𝓢(D, V)
k : ℕ
x : D
⊢ Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) =
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_9} ℝ (fun (i : Fin 0) ↦ D) V)
      (iteratedFDeriv ℝ 0 (⇑f : (a : D) → V) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
D : Type u_4
V : Type u_9
inst : NormedAddCommGroup D
inst_1 : NormedSpace ℝ D
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_5 : BorelSpace D
inst_6 : SecondCountableTopology D
f : 𝓢(D, V)
x : D
⊢ Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V) ≤
    ‖HPow.hPow (β := ℕ) ‖x‖ 0 * Norm.norm.{u_9} (E := V) ((f : (a : D) → V) x : V)‖

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
refine :
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, V)),
        Norm.norm.{u_9} (E := V) ((fun (x : 𝓢(D, V)) ↦ (∫ (x_1 : D), (x : (a : D) → V) x_1 ∂μ : V)) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ 𝓢(D, V) →L[𝕜] V

Tactic:
refine mkCLMtoNormedSpace (∫ x, · x ∂μ)
    (fun f g ↦ integral_add f.integrable g.integrable) (integral_smul · ·) ?_

Premises used: MeasureTheory.integral, SchwartzMap.mkCLMtoNormedSpace, SchwartzMap.integrable, DFunLike.coe, MeasureTheory.integral_add
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
rcases :
  ∀ (n : ℕ) (h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(D, V)),
          Norm.norm.{u_9} (E := V) ((fun (x : 𝓢(D, V)) ↦ (∫ (x_1 : D), (x : (a : D) → V) x_1 ∂μ : V)) f) ≤
            HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, V)),
        Norm.norm.{u_9} (E := V) ((fun (x : 𝓢(D, V)) ↦ (∫ (x_1 : D), (x : (a : D) → V) x_1 ∂μ : V)) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
rcases hμ.exists_integrable with ⟨n, h⟩

Premises used: MeasureTheory.Measure.HasTemperateGrowth.exists_integrable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
n : ℕ
h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ
m : ℕ × ℕ := (n, 0)
h₁ :
  0 ≤ HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ ∧
    ∀ (f : 𝓢(D, V)),
      Norm.norm.{u_9} (E := V) ((fun (x : 𝓢(D, V)) ↦ (∫ (x_1 : D), (x : (a : D) → V) x_1 ∂μ : V)) f) ≤
        HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ)
          (((Finset.Iic m).sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, V)),
        Norm.norm.{u_9} (E := V) ((fun (x : 𝓢(D, V)) ↦ (∫ (x_1 : D), (x : (a : D) → V) x_1 ∂μ : V)) f) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D V) : (a : 𝓢(D, V)) → ℝ) f : ℝ)

Tactic:
use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ

Premises used: Nat.cast, Finset.Iic, Neg.neg
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedAddCommGroup V
inst_8 : NormedSpace ℝ V
inst_9 : NormedSpace 𝕜 V
inst_10 : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst_11 : BorelSpace D
inst_12 : SecondCountableTopology D
n : ℕ
h : Integrable (ε := ℝ) (fun (x : D) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ))) μ
m : ℕ × ℕ := (n, 0)
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 n * ∫ (x : D), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑n : ℝ)) ∂μ

Tactic:
positivity