awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
𝕜 : Type u_2
D : Type u_4
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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ IsBigO (E := ℝ) (F := ℝ) ⊤
    (fun (x : D) ↦
      (↑(n.choose i) : ℝ) *
        (norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)))
    fun (x : D) ↦ (1 + ‖x‖) ^ k1 * (1 + ‖x‖) ^ k2
have h : i ≤ n
Tactic: refine .const_mul_left (.mul (h1 i ?_).norm_left (h2 (n - i) ?_).norm_left) _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
𝕜 : Type u_2
D : Type u_4
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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 G
inst_12 : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin n_1) ↦ D) E) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 f) fun (x : D) ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 :
  ∀ n_1 ≤ n,
    IsBigO (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n_1) ↦ D) F) (F := ℝ) ⊤
      (iteratedFDeriv ℝ n_1 g) fun (x : D) ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n (fun (x : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)
i : ℕ
hi : i ∈ Finset.range (n + 1)
h : i ≤ n
⊢ IsBigO (E := ℝ) (F := ℝ) ⊤
    (fun (x : D) ↦
      (↑(n.choose i) : ℝ) *
        (norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E) (iteratedFDeriv ℝ i f x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)))
    fun (x : D) ↦ (1 + ‖x‖) ^ k1 * (1 + ‖x‖) ^ k2
have h₁ : n - i ≤ n
Tactic: refine .const_mul_left (.mul (h1 i ?_).norm_left (h2 (n - i) ?_).norm_left) _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ HasTemperateGrowth.{u_5, u_5} (E := E) _root_.id
have h'f : HasTemperateGrowth.{u_5, u_5} (E := E) (F := E →L[ℝ] E) (fderiv ℝ _root_.id)
Tactic: apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h'f : HasTemperateGrowth.{u_5, u_5} (E := E) (F := E →L[ℝ] E) (fderiv ℝ _root_.id)
⊢ HasTemperateGrowth.{u_5, u_5} (E := E) _root_.id
have hf : Differentiable.{0, u_5, u_5} ℝ (E := E) _root_.id
Tactic: apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h'f : HasTemperateGrowth.{u_5, u_5} (E := E) (F := E →L[ℝ] E) (fderiv ℝ _root_.id)
hf : Differentiable.{0, u_5, u_5} ℝ (E := E) _root_.id
⊢ HasTemperateGrowth.{u_5, u_5} (E := E) _root_.id
have h : ∀ (x : E), ‖_root_.id x‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 1
Tactic: apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ HasTemperateGrowth.{u_5, u_5} (E := E) (F := E →L[ℝ] E) (fderiv ℝ _root_.id)
have h : ∀ (x : E), Eq (α := E →L[ℝ] E) (fderiv ℝ _root_.id x) (ContinuousLinearMap.id ℝ E)
Tactic: convert Function.HasTemperateGrowth.const (ContinuousLinearMap.id ℝ E)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ (k + 1))
have succ : HasTemperateGrowth (f ^ k * f)
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
⊢ HasTemperateGrowth (f ^ k)
have zero : HasTemperateGrowth (HPow.hPow (β := ℕ) f 0)
Tactic: induction k with
  | zero => simpa only [pow_zero] using HasTemperateGrowth.const 1
  | succ k IH => rw [pow_succ]; fun_prop
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
R : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedRing R
inst_3 : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
zero : HasTemperateGrowth (HPow.hPow (β := ℕ) f 0)
⊢ HasTemperateGrowth (f ^ k)
have succ : ∀ (k : ℕ) (IH : HasTemperateGrowth (f ^ k)), HasTemperateGrowth (f ^ (k + 1))
Tactic: induction k with
  | zero => simpa only [pow_zero] using HasTemperateGrowth.const 1
  | succ k IH => rw [pow_succ]; fun_prop
Cleared hypotheses: k
-- 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 →L[ℝ] F
⊢ HasTemperateGrowth.{u_5, u_6} (E := E) (F := F) (⇑f : (a : E) → F)
have apply : HasTemperateGrowth (E := E) (F := E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F))
Tactic: apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (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 →L[ℝ] F
apply : HasTemperateGrowth (E := E) (F := E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F))
⊢ HasTemperateGrowth.{u_5, u_6} (E := E) (F := F) (⇑f : (a : E) → F)
have apply₁ : ∀ (x : E), norm.{u_6} (E := F) ((f : (a : E) → F) x : F) ≤ ‖f‖ * HPow.hPow (β := ℕ) (1 + ‖x‖) 1
Tactic: apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (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 →L[ℝ] F
⊢ Eq (α := (x : E) → E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F)) fun (x : E) ↦ f
have h : ∀ (v : E), fderiv ℝ (⇑f : (a : E) → F) v = f
Tactic: ext1 v
-- 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 →L[ℝ] F
⊢ HasTemperateGrowth (E := E) (F := E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F))
have this : Eq (α := (x : E) → E →L[ℝ] F) (fderiv ℝ (⇑f : (a : E) → F)) fun (x : E) ↦ f
Tactic: have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
have h'f : HasTemperateGrowth.{u_8, u_8} (E := H) (F := H →L[ℝ] ℝ) (fderiv ℝ fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: apply _root_.Function.HasTemperateGrowth.of_fderiv (C := 1) (k := 2)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
h'f : HasTemperateGrowth.{u_8, u_8} (E := H) (F := H →L[ℝ] ℝ) (fderiv ℝ fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
have hf : Differentiable ℝ (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: apply _root_.Function.HasTemperateGrowth.of_fderiv (C := 1) (k := 2)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
h'f : HasTemperateGrowth.{u_8, u_8} (E := H) (F := H →L[ℝ] ℝ) (fderiv ℝ fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
hf : Differentiable ℝ (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2
have h : ∀ (x : H), ‖HPow.hPow (β := ℕ) ‖x‖ 2‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 2
Tactic: apply _root_.Function.HasTemperateGrowth.of_fderiv (C := 1) (k := 2)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
⊢ HasTemperateGrowth.{u_8, u_8} (E := H) (F := H →L[ℝ] ℝ) (fderiv ℝ fun (x : H) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
have h'f : HasTemperateGrowth (HSMul.hSMul (α := ℕ) (β := (a : H) → H →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : H) → H →L[ℝ] ℝ))
Tactic: rw [fderiv_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
x : H
⊢ ‖HPow.hPow (β := ℕ) ‖x‖ 2‖ ≤ 1 * HPow.hPow (β := ℕ) (1 + ‖x‖) 2
have h : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 1 2 + HMul.hMul (α := ℝ) 2 1 * ‖x‖ + HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [norm_pow, norm_norm, one_mul, add_pow_two]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
y : H
⊢ (fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) y ∈ t
have simp : 1 / 2 < 1 + HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: simp only [Set.mem_setOf_eq, t]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ r
have ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
Tactic: have ht : Set.range (fun (x : H) ↦ (1 + ‖x‖ ^ 2)) ⊆ t := by
    rintro - ⟨y, rfl⟩
    simp only [Set.mem_setOf_eq, t]
    exact lt_add_of_lt_add_left (c := 0) (by norm_num) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ r
have hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
Tactic: have hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t :=
    contDiffOn_fun_id.rpow_const_of_ne fun x hx ↦ (lt_trans (by norm_num) hx).ne'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ r
have hunique : UniqueDiffOn ℝ t
Tactic: have hunique : UniqueDiffOn ℝ t := (isOpen_lt' (1 / 2)).uniqueDiffOn
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
⊢ HasTemperateGrowth (F := ℝ) fun (x : H) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ r
have apply : ∀ (N : ℕ),
  ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k
Tactic: apply HasTemperateGrowth.comp' ht hunique hdiff _ (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N : ℕ
⊢ ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k
have obtain : ∀ (k : ℕ) (hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)),
  ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k
Tactic: obtain ⟨k, hk⟩ := exists_nat_ge (max r <| (N - r) * Real.log 2 / (Real.log (3 / 2)))
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
⊢ ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k
have hk₁ : r ≤ (↑k : ℝ)
Tactic: have hk₁ : r ≤ k := le_sup_left.trans hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
⊢ Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
have this : ((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2) ≤ (↑k : ℝ)
Tactic: have := le_sup_right.trans hk
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
this : ((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2) ≤ (↑k : ℝ)
⊢ Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
have this₁ : ((↑N : ℝ) - r) * Real.log 2 ≤ Real.log (3 / 2) * (↑k : ℝ)
Tactic: field_simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
⊢ ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k
have hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
Tactic: have hk₂ : Real.log 2 * (N - r) ≤ (Real.log (3 / 2)) * k := by
    have := le_sup_right.trans hk
    field_simp at this
    grind
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
⊢ ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
    ∀ n ≤ N,
      ∀ x ∈ t,
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
            (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
          C * (1 + ‖x‖) ^ k
have h : ∀ n ≤ N,
  ∀ x ∈ t,
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ)
        (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
      (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
Tactic: use k, ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖, by positivity
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ) (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
have this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
Tactic: have : ContDiffAt ℝ n (fun x ↦ x ^ r) x :=
    Real.contDiffAt_rpow_const <| Or.inl (lt_trans (by norm_num) hx).ne'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) ℝ) (iteratedFDerivWithin ℝ n (fun (x : ℝ) ↦ x ^ r) t x) ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
have h : ‖Polynomial.eval r (descPochhammer ℝ n)‖ * ‖x ^ (r - (↑n : ℝ))‖ ≤
  (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
Tactic: rw [norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin,
    iteratedDerivWithin_eq_iteratedDeriv hunique this hx, iteratedDeriv_eq_iterate,
    Real.iter_deriv_rpow_const, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ * ‖x ^ (r - (↑n : ℝ))‖ ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
have h : ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖
Tactic: gcongr 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
h : ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ * ‖x ^ (r - (↑n : ℝ))‖ ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
have h₁ : ‖x ^ (r - (↑n : ℝ))‖ ≤ (1 + ‖x‖) ^ k
Tactic: gcongr 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
H : Type u_8
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y : ℝ | 1 / 2 < y}
ht : (Set.range fun (x : H) ↦ 1 + HPow.hPow (β := ℕ) ‖x‖ 2) ⊆ t
hdiff : ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ) ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r (((↑N : ℝ) - r) * Real.log 2 / Real.log (3 / 2)) ≤ (↑k : ℝ)
hk₁ : r ≤ (↑k : ℝ)
hk₂ : Real.log 2 * ((↑N : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖
have this₁ : n ∈ Finset.range (N + 1)
Tactic: have : n ∈ Finset.range (N + 1) := by grind