awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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)‖ * ‖x ^ (r - (↑n : ℝ))‖ ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
⊢ 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:
rw [norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin,
    iteratedDerivWithin_eq_iteratedDeriv hunique this hx, iteratedDeriv_eq_iterate,
    Real.iter_deriv_rpow_const, norm_mul]

Premises used: iteratedDerivWithin_eq_iteratedDeriv, norm_mul, iteratedDeriv_eq_iterate, Real.iter_deriv_rpow_const, norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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)‖
h₁ : ‖x ^ (r - (↑n : ℝ))‖ ≤ (1 + ‖x‖) ^ k
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ * ‖x ^ (r - (↑n : ℝ))‖ ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k

Tactic:
gcongr 1
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ n ∈ Finset.range (N + 1)

Tactic:
grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ n ∈ Finset.range (N + 1)

Tactic:
have : n ∈ Finset.range (N + 1) := by grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
this : n ∈ Finset.range (N + 1)
x_1 : ℕ
h : x_1 ∈ Finset.range (N + 1)
⊢ 0 ≤ ‖Polynomial.eval r (descPochhammer ℝ x_1)‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
this : n ∈ Finset.range (N + 1)
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖

Tactic:
apply Finset.single_le_sum (fun _ _ ↦ by positivity) this

Premises used: Finset.single_le_sum
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 1 / 2 < x

Tactic:
simpa [t] using hx
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 1 / 2 < x

Tactic:
have hx' : 1 / 2 < x := by simpa [t] using hx
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
⊢ 0 < x

Tactic:
have hx'' : 0 < x := lt_of_lt_of_le (by norm_num) hx'.le
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h : |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
⊢ |x ^ (r - (↑n : ℝ))| ≤ (1 + |x|) ^ k

Tactic:
apply (Real.abs_rpow_le_abs_rpow _ _).trans

Premises used: Real.abs_rpow_le_abs_rpow, LE.le.trans
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
pos : ∀ (h : 0 ≤ r - (↑n : ℝ)), |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
neg : ∀ (h : r - (↑n : ℝ) < 0), |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k

Tactic:
by_cases! h : 0 ≤ r - n
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
⊢ (↑k : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
⊢ r - (↑n : ℝ) ≤ (↑k : ℝ)

Tactic:
simpa using hk₁.trans (by simp)

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
⊢ r - (↑n : ℝ) ≤ (↑k : ℝ)

Tactic:
have : r - n ≤ k := by simpa using hk₁.trans (by simp)
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
this : r - (↑n : ℝ) ≤ (↑k : ℝ)
pos : |x| ^ (r - (↑n : ℝ)) ≤ HPow.hPow (β := ℝ) (1 + |x|) (↑k : ℝ)
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k

Tactic:
rw [← Real.rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
this : r - (↑n : ℝ) ≤ (↑k : ℝ)
⊢ 0 ≤ |x|

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
this : r - (↑n : ℝ) ≤ (↑k : ℝ)
⊢ |x| ≤ 1 + |x|

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
this : r - (↑n : ℝ) ≤ (↑k : ℝ)
⊢ 1 ≤ 1 + |x|

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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_1 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
this : r - (↑n : ℝ) ≤ (↑k : ℝ)
⊢ |x| ^ (r - (↑n : ℝ)) ≤ HPow.hPow (β := ℝ) (1 + |x|) (↑k : ℝ)

Tactic:
exact (Real.rpow_le_rpow (by positivity) (by simp) h).trans
      (Real.rpow_le_rpow_of_exponent_le (by simp) this)

Premises used: Real.rpow_le_rpow, LE.le.trans, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h : r - (↑n : ℝ) < 0
⊢ 0 < (↑n : ℝ) - r

Tactic:
grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h : r - (↑n : ℝ) < 0
⊢ 0 < (↑n : ℝ) - r

Tactic:
have h : 0 < n - r := by grind
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
rw : |x| ^ (r - (↑n : ℝ)) = x ^ (r - (↑n : ℝ))
⊢ |x| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))

Tactic:
rw [neg_sub]

Premises used: neg_sub
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
e_a : |x| = x
⊢ |x| ^ (r - (↑n : ℝ)) = x ^ (r - (↑n : ℝ))

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ |x| = x

Tactic:
simpa using hx''.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ 2⁻¹ < x

Tactic:
simp only [one_div, Set.mem_setOf_eq, t] at hx

Premises used: Set.mem_setOf_eq, one_div
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
hx : 2⁻¹ < x
rw : x⁻¹ ^ ((↑n : ℝ) - r) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
⊢ x ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)

Tactic:
rw [Real.rpow_neg_eq_inv_rpow]

Premises used: Real.rpow_neg_eq_inv_rpow
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
hx : 2⁻¹ < x
h₁ : x⁻¹ ≤ 2
⊢ x⁻¹ ^ ((↑n : ℝ) - r) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
hx : 2⁻¹ < x
⊢ LT.lt (α := ℝ) 0 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ
this : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
hx : 2⁻¹ < x
⊢ x⁻¹ ≤ 2

Tactic:
exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le

Premises used: Iff.mpr, LT.lt.le, inv_lt_comm₀
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
hx₁ : LT.lt (α := ℝ) 0 2
⊢ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r) = Real.exp (Real.log 2 * ((↑n : ℝ) - r))

Tactic:
rw [Real.rpow_def_of_pos]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ LT.lt (α := ℝ) 0 2

Tactic:
norm_num