awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ‖x ^ (r - (↑n : ℝ))‖ ≤ (1 + ‖x‖) ^ k
have hx' : 1 / 2 < x
Tactic: have hx' : 1 / 2 < x := by simpa [t] using hx
-- 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
hx' : 1 / 2 < x
⊢ ‖x ^ (r - (↑n : ℝ))‖ ≤ (1 + ‖x‖) ^ k
have hx'' : 0 < x
Tactic: have hx'' : 0 < x := lt_of_lt_of_le (by norm_num) hx'.le
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
⊢ |x ^ (r - (↑n : ℝ))| ≤ (1 + |x|) ^ k
have h : |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
Tactic: apply (Real.abs_rpow_le_abs_rpow _ _).trans
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have pos : ∀ (h : 0 ≤ r - (↑n : ℝ)), |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
Tactic: by_cases! h : 0 ≤ r - n
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
pos : ∀ (h : 0 ≤ r - (↑n : ℝ)), |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have neg : ∀ (h : r - (↑n : ℝ) < 0), |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
Tactic: by_cases! h : 0 ≤ r - n
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - (↑n : ℝ)
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have this₁ : r - (↑n : ℝ) ≤ (↑k : ℝ)
Tactic: have : r - n ≤ k := by simpa using hk₁.trans (by simp)
-- 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_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 : ℝ)) ≤ (1 + |x|) ^ k
have pos : |x| ^ (r - (↑n : ℝ)) ≤ HPow.hPow (β := ℝ) (1 + |x|) (↑k : ℝ)
Tactic: rw [← Real.rpow_natCast]
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h : r - (↑n : ℝ) < 0
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have h₁ : 0 < (↑n : ℝ) - r
Tactic: have h : 0 < n - r := by 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 : ℝ)
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| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))
have rw : |x| ^ (r - (↑n : ℝ)) = x ^ (r - (↑n : ℝ))
Tactic: rw [neg_sub]
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ |x| ^ (r - (↑n : ℝ)) = x ^ (r - (↑n : ℝ))
have e_a : |x| = x
Tactic: congr
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ x ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
have hx₁ : 2⁻¹ < x
Tactic: simp only [one_div, Set.mem_setOf_eq, t] at hx
Cleared hypotheses: hx
-- 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 : ℝ
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 ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
have rw : x⁻¹ ^ ((↑n : ℝ) - r) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
Tactic: rw [Real.rpow_neg_eq_inv_rpow]
-- 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 : ℝ
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⁻¹ ^ ((↑n : ℝ) - r) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
have h₁ : x⁻¹ ≤ 2
Tactic: gcongr
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r) = Real.exp (Real.log 2 * ((↑n : ℝ) - r))
have hx₁ : LT.lt (α := ℝ) 0 2
Tactic: rw [Real.rpow_def_of_pos]
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ Real.exp (Real.log 2 * ((↑n : ℝ) - r)) ≤ Real.exp (Real.log (3 / 2) * (↑k : ℝ))
have a : Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log (3 / 2) * (↑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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
have apply : Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log 2 * ((↑N : ℝ) - r)
Tactic: apply le_trans _ hk₂
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log 2 * ((↑N : ℝ) - r)
have ha : 0 ≤ Real.log 2
Tactic: gcongr
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ Real.exp (Real.log (3 / 2) * (↑k : ℝ)) ≤ (3 / 2) ^ k
have hx₁ : 0 < 3 / 2
Tactic: rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ (3 / 2) ^ k ≤ (1 + |x|) ^ k
have hab : 3 / 2 ≤ 1 + |x|
Tactic: gcongr
-- 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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have In : |x| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))
Tactic: calc
    /- In the case `0 < n - r`, we need the factor `Real.log 2 / (Real.log (3 / 2))` to control
    the growth near `‖x‖ = 1/2`. -/
    _ = x ^ (-(n - r)) := by
      rw [neg_sub]
      congr
      simpa using hx''.le
    _ ≤ (2 : ℝ) ^ (n - r) := by
      simp only [one_div, Set.mem_setOf_eq, t] at hx
      rw [Real.rpow_neg_eq_inv_rpow]
      gcongr
      exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le
    _ = Real.exp (Real.log 2 * (n - r)) := by
      rw [Real.rpow_def_of_pos]
      norm_num
    _ ≤ Real.exp (Real.log (3 / 2) * k) := by
      gcongr 1
      apply le_trans _ hk₂
      gcongr
    _ ≤ (3 / 2) ^ k := by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num
    _ ≤ _ := by
      gcongr
      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 : ℝ)
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
In : |x| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have In₁ : x ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
Tactic: calc
    /- In the case `0 < n - r`, we need the factor `Real.log 2 / (Real.log (3 / 2))` to control
    the growth near `‖x‖ = 1/2`. -/
    _ = x ^ (-(n - r)) := by
      rw [neg_sub]
      congr
      simpa using hx''.le
    _ ≤ (2 : ℝ) ^ (n - r) := by
      simp only [one_div, Set.mem_setOf_eq, t] at hx
      rw [Real.rpow_neg_eq_inv_rpow]
      gcongr
      exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le
    _ = Real.exp (Real.log 2 * (n - r)) := by
      rw [Real.rpow_def_of_pos]
      norm_num
    _ ≤ Real.exp (Real.log (3 / 2) * k) := by
      gcongr 1
      apply le_trans _ hk₂
      gcongr
    _ ≤ (3 / 2) ^ k := by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num
    _ ≤ _ := by
      gcongr
      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 : ℝ)
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
In : |x| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))
In₁ : x ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have In₂ : HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r) = Real.exp (Real.log 2 * ((↑n : ℝ) - r))
Tactic: calc
    /- In the case `0 < n - r`, we need the factor `Real.log 2 / (Real.log (3 / 2))` to control
    the growth near `‖x‖ = 1/2`. -/
    _ = x ^ (-(n - r)) := by
      rw [neg_sub]
      congr
      simpa using hx''.le
    _ ≤ (2 : ℝ) ^ (n - r) := by
      simp only [one_div, Set.mem_setOf_eq, t] at hx
      rw [Real.rpow_neg_eq_inv_rpow]
      gcongr
      exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le
    _ = Real.exp (Real.log 2 * (n - r)) := by
      rw [Real.rpow_def_of_pos]
      norm_num
    _ ≤ Real.exp (Real.log (3 / 2) * k) := by
      gcongr 1
      apply le_trans _ hk₂
      gcongr
    _ ≤ (3 / 2) ^ k := by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num
    _ ≤ _ := by
      gcongr
      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 : ℝ)
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
In : |x| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))
In₁ : x ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
In₂ : HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r) = Real.exp (Real.log 2 * ((↑n : ℝ) - r))
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have In₃ : Real.exp (Real.log 2 * ((↑n : ℝ) - r)) ≤ Real.exp (Real.log (3 / 2) * (↑k : ℝ))
Tactic: calc
    /- In the case `0 < n - r`, we need the factor `Real.log 2 / (Real.log (3 / 2))` to control
    the growth near `‖x‖ = 1/2`. -/
    _ = x ^ (-(n - r)) := by
      rw [neg_sub]
      congr
      simpa using hx''.le
    _ ≤ (2 : ℝ) ^ (n - r) := by
      simp only [one_div, Set.mem_setOf_eq, t] at hx
      rw [Real.rpow_neg_eq_inv_rpow]
      gcongr
      exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le
    _ = Real.exp (Real.log 2 * (n - r)) := by
      rw [Real.rpow_def_of_pos]
      norm_num
    _ ≤ Real.exp (Real.log (3 / 2) * k) := by
      gcongr 1
      apply le_trans _ hk₂
      gcongr
    _ ≤ (3 / 2) ^ k := by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num
    _ ≤ _ := by
      gcongr
      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 : ℝ)
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
In : |x| ^ (r - (↑n : ℝ)) = x ^ (-((↑n : ℝ) - r))
In₁ : x ^ (-((↑n : ℝ) - r)) ≤ HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r)
In₂ : HPow.hPow (α := ℝ) 2 ((↑n : ℝ) - r) = Real.exp (Real.log 2 * ((↑n : ℝ) - r))
In₃ : Real.exp (Real.log 2 * ((↑n : ℝ) - r)) ≤ Real.exp (Real.log (3 / 2) * (↑k : ℝ))
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have In₄ : Real.exp (Real.log (3 / 2) * (↑k : ℝ)) ≤ (3 / 2) ^ k
Tactic: calc
    /- In the case `0 < n - r`, we need the factor `Real.log 2 / (Real.log (3 / 2))` to control
    the growth near `‖x‖ = 1/2`. -/
    _ = x ^ (-(n - r)) := by
      rw [neg_sub]
      congr
      simpa using hx''.le
    _ ≤ (2 : ℝ) ^ (n - r) := by
      simp only [one_div, Set.mem_setOf_eq, t] at hx
      rw [Real.rpow_neg_eq_inv_rpow]
      gcongr
      exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le
    _ = Real.exp (Real.log 2 * (n - r)) := by
      rw [Real.rpow_def_of_pos]
      norm_num
    _ ≤ Real.exp (Real.log (3 / 2) * k) := by
      gcongr 1
      apply le_trans _ hk₂
      gcongr
    _ ≤ (3 / 2) ^ k := by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num
    _ ≤ _ := by
      gcongr
      grind