awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
      fun (x : E) ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
⊢ IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
    fun (x : E) ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
have h : ∀ (x : E), ‖(1 + ‖x‖) ^ k n‖ ≤ ‖(1 + ‖x‖) ^ (Finset.range (N + 1)).sup k‖
Tactic: refine (hk n).trans (isBigO_of_le _ fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
      fun (x : E) ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ ‖(1 + ‖x‖) ^ k n‖ ≤ ‖(1 + ‖x‖) ^ (Finset.range (N + 1)).sup k‖
have h : (1 + ‖x‖) ^ k n ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
Tactic: rw [Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
      fun (x : E) ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
⊢ (1 + ‖x‖) ^ k n ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
have h : 1 ≤ 1 + ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : (n : ℕ) → ℕ
hk :
  ∀ (n : ℕ),
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (F := ℝ) ⊤ (iteratedFDeriv ℝ n f)
      fun (x : E) ↦ (1 + ‖x‖) ^ k n
n : ℕ
hn : n ≤ N
x : E
h : 1 ≤ 1 + ‖x‖
⊢ (1 + ‖x‖) ^ k n ≤ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
have h₁ : k n ≤ (Finset.range (N + 1)).sup k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
n : ℕ
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k
have rcases : ∀ (k : ℕ)
  (hk :
    ∀ n_1 ≤ n,
      IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F) (F := ℝ) ⊤
        (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k),
  ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k
Tactic: rcases hf_temperate.isBigO_uniform n with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k
have this : IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
Tactic: have : F =O[⊤] (fun x ↦ (1 + ‖x‖) ^ k) := by
    simp_rw [F, isBigO_pi, Fin.forall_iff, Nat.lt_succ_iff]
    exact hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
this : IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k
have rcases : ∀ (C : ℝ) (C_nonneg : C ≥ 0) (hC : IsBigOWith (F := ℝ) C ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k),
  ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k
Tactic: rcases this.exists_nonneg with ⟨C, C_nonneg, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
F_1 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F_1
inst_3 : NormedSpace ℝ F_1
f : E → F_1
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F_1) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : E) ↦ (1 + ‖x‖) ^ k
F : (x : E) → (N : Fin (n + 1)) → ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (↑N : ℕ)) ↦ E) F_1 :=
  fun (x : E) (N : Fin (n + 1)) ↦ iteratedFDeriv ℝ (↑N : ℕ) f x
this : IsBigO (F := ℝ) ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
C : ℝ
C_nonneg : C ≥ 0
hC : IsBigOWith (F := ℝ) C ⊤ F fun (x : E) ↦ (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    0 ≤ C ∧
      ∀ N ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin N) ↦ E) F_1) (iteratedFDeriv ℝ N f x) ≤
            C * (1 + ‖x‖) ^ k
have hC₁ : ∀ (x : E) (i : ℕ) (h : i ≤ n),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F_1) (F x (⟨i, sorry⟩ : Fin (n + 1))) ≤
    C * (1 + ‖x‖) ^ k
Tactic: simp (discharger := positivity) only [isBigOWith_top, Real.norm_of_nonneg,
    pi_norm_le_iff_of_nonneg, Fin.forall_iff, Nat.lt_succ_iff] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ HasTemperateGrowth f
have refine : ∀ (n : ℕ),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: refine ⟨contDiff_succ_iff_fderiv.2 ⟨hf, by simp, h'f.1⟩, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
n : ℕ
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
have zero : ∃ (k : ℕ) (C : ℝ),
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x) ≤
      C * (1 + ‖x‖) ^ k
Tactic: rcases n with rfl | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
n : ℕ
zero :
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F) (iteratedFDeriv ℝ 0 f x) ≤
        C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
have succ : ∀ (m : ℕ),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: rcases n with rfl | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m : ℕ
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k
have succ : ∀ (k' : ℕ) (C' : ℝ)
  (h' :
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
        C' * (1 + ‖x‖) ^ k'),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: rcases h'f.2 m with ⟨k', C', h'⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
      C' * (1 + ‖x‖) ^ k'
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (m + 1) f x) ≤
        C * (1 + ‖x‖) ^ k
have succ : ∀ (x : E),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F) (iteratedFDeriv ℝ (m + 1) f x) ≤
    C' * (1 + ‖x‖) ^ k'
Tactic: refine ⟨k', C', ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (F := E →L[ℝ] F) (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m k' : ℕ
C' : ℝ
h' :
  ∀ (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) (iteratedFDeriv ℝ m (fderiv ℝ f) x) ≤
      C' * (1 + ‖x‖) ^ k'
⊢ ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
        (iteratedFDeriv ℝ (m + 1) f x) ≤
      C' * (1 + ‖x‖) ^ k'
have succ : ∀ (x : E),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' ℝ m E F) :
            (a : ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ E) (E →L[ℝ] F)) →
              ContinuousMultilinearMap ℝ (fun (i : Fin (m + 1)) ↦ E) F)
          (iteratedFDeriv ℝ m (fun (y : E) ↦ fderiv ℝ f y) x) :
        ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (m + 1)) ↦ E) F) ≤
    C' * (1 + ‖x‖) ^ k'
Tactic: simpa [iteratedFDeriv_succ_eq_comp_right] using h'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
⊢ HasTemperateGrowth.{u_5, u_6} (F := F) fun (x : E) ↦ 0
have refine : ∀ (n : ℕ) (x : E),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (fun (x : E) ↦ 0) x) ≤
    0 * HPow.hPow (β := ℕ) (1 + ‖x‖) 0
Tactic: refine ⟨contDiff_const, fun n ↦ ⟨0, 0, fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
⊢ HasTemperateGrowth f
have refine : ∀ (n : ℕ),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: refine ⟨h₂, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
have hg : Continuous g
Tactic: have hg : Continuous g := (h₂.continuous_iteratedFDeriv <| mod_cast le_top).norm
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg : Continuous g
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
have obtain : ∀ (x₀ : E) (hx₀ : ∀ (y : E), g y ≤ g x₀),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: obtain ⟨x₀, hx₀⟩ := hg.exists_forall_ge_of_hasCompactSupport ((h₁.iteratedFDeriv _).norm)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg : Continuous g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C * (1 + ‖x‖) ^ k
have refine : ∀ (x : E),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
    g x₀ * HPow.hPow (β := ℕ) (1 + ‖x‖) 0
Tactic: refine ⟨0, g x₀, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
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 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (g ∘ f)
have refine : ∀ (n : ℕ),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: refine ⟨hg₁.comp_contDiff hf.1 (ht ⟨·, rfl⟩), fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
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 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n : ℕ
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
have obtain : ∀ (k₁ : ℕ) (C₁ : ℝ) (hC₁ : 0 ≤ C₁)
  (h₁ :
    ∀ N ≤ n,
      ∀ (x : D),
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
          C₁ * (1 + ‖x‖) ^ k₁),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: obtain ⟨k₁, C₁, hC₁, h₁⟩ := hf.norm_iteratedFDeriv_le_uniform n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
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 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
have obtain : ∀ (k₂ : ℕ) (C₂ : ℝ) (hC₂ : 0 ≤ C₂)
  (h₂ :
    ∀ n_1 ≤ n,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
            (iteratedFDerivWithin ℝ n_1 g t x) ≤
          C₂ * (1 + ‖x‖) ^ k₂),
  ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
Tactic: obtain ⟨k₂, C₂, hC₂, h₂⟩ := hg₂ n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
D : Type u_4
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 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
have h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
Tactic: have h₁' : ∀ x, ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁ := by simpa using h₁ 0
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
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 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
        C * (1 + ‖x‖) ^ k
have h : ∀ (x : D),
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
Tactic: use k₁ * k₂ + k₁ * n, n ! * C₃ * (1 + C₁) ^ n