awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ))
In₄ : Real.exp (Real.log (3 / 2) * (↑k : ℝ)) ≤ (3 / 2) ^ k
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (1 + |x|) ^ k
have In₅ : (3 / 2) ^ k ≤ (1 + |x|) ^ 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:
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : BorelSpace E
μ : Measure E
h : μ.IsAddHaarMeasure
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(finrank ℝ E + 1) : ℝ))) μ
have hnr : LT.lt (α := ℝ) (↑(finrank ℝ E) : ℝ) (↑(finrank ℝ E + 1) : ℝ)
Tactic: apply integrable_one_add_norm
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
⊢ x ^ k * f ≤ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ))
have this : 0 ≤ C₂
Tactic: have : 0 ≤ C₂ := le_trans (by positivity) h₂
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this : 0 ≤ C₂
⊢ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have rw : HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
  HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) / HPow.hPow (α := ℝ) (β := ℝ) 2 (-(↑l : ℝ)) * (C₁ + C₂)
Tactic: rw [Real.div_rpow (by positivity) zero_le_two]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this : 0 ≤ C₂
⊢ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) / HPow.hPow (α := ℝ) (β := ℝ) 2 (-(↑l : ℝ)) * (C₁ + C₂)
have simp : HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) ((1 + x) ^ l) (-1) =
  HPow.hPow (α := ℝ) 2 l * HPow.hPow (β := ℝ) ((1 + x) ^ l) (-1) * (C₁ + C₂)
Tactic: simp [div_eq_inv_mul, ← Real.rpow_neg_one, ← Real.rpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this : 0 ≤ C₂
⊢ x ^ k * f ≤ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ))
have this₁ : HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
  HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
Tactic: have : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (- (l : ℝ)) = ((1 + x) / 2) ^ (-(l : ℝ)) * (C₁ + C₂) := by
    rw [Real.div_rpow (by positivity) zero_le_two]
    simp [div_eq_inv_mul, ← Real.rpow_neg_one, ← Real.rpow_mul]
    ring
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
⊢ x ^ k * f ≤ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ))
have rw : x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have inl : ∀ (h'x : x ≤ 1), x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
Tactic: rcases le_total x 1 with h'x | h'x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
inl : ∀ (h'x : x ≤ 1), x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have inr : ∀ (h'x : 1 ≤ x), x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
Tactic: rcases le_total x 1 with h'x | h'x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have inl : x ^ k ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
inl : x ^ k ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have inl₁ : f ≤ C₁ + C₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
⊢ x ^ k ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
have inl : 1 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
Tactic: apply (pow_le_one₀ hx h'x).trans
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
⊢ 1 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
have inl : 0 < (1 + x) / 2
Tactic: apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
inl : 0 < (1 + x) / 2
⊢ 1 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
have inl₁ : (1 + x) / 2 ≤ 1
Tactic: apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
inl : 0 < (1 + x) / 2
inl₁ : (1 + x) / 2 ≤ 1
⊢ 1 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
have inl₂ : LE.le (α := ℝ) (-(↑l : ℝ)) 0
Tactic: apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
⊢ (1 + x) / 2 ≤ 1
have linarith : 1 < (1 + x) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
linarith : 1 < (1 + x) / 2 → 2 / 2 = 1
⊢ (1 + x) / 2 ≤ 1
have linarith₁ : 1 < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
linarith : 1 < (1 + x) / 2 → 2 / 2 = 1
linarith₁ : 1 < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (1 + x) / 2 ≤ 1
have linarith₂ : 1 < (1 + x) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
linarith : 1 < (1 + x) / 2 → 2 / 2 = 1
linarith₁ : 1 < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < (1 + x) / 2 → GT.gt (α := ℝ) 2 0
⊢ (1 + x) / 2 ≤ 1
have linarith₃ : 1 < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
linarith : 1 < (1 + x) / 2 → 2 / 2 = 1
linarith₁ : 1 < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < (1 + x) / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ linarith₅ : 1 < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ (1 + x) / 2 ≤ 1
have linarith₆ : 1 < (1 + x) / 2 → x - 1 + (HMul.hMul (α := ℝ) 2 1 - (HMul.hMul (α := ℝ) 1 1 + 1 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
⊢ f ≤ C₁ + C₂
have linarith : C₁ + C₂ < f → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : x ≤ 1
linarith linarith₁ linarith₂ : C₁ + C₂ < f → HMul.hMul (α := ℝ) 1 1 = 1
⊢ f ≤ C₁ + C₂
have linarith₃ : C₁ + C₂ < f → f - C₁ + (0 - C₂) + (C₁ + C₂ - f) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f = HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f)
have rw : HPow.hPow (β := ℝ) x (↑k : ℝ) * f = x ^ HAdd.hAdd (α := ℝ) (-(↑l : ℝ)) (↑(k + l) : ℝ) * f
Tactic: rw [← Real.rpow_natCast, ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have apply : HPow.hPow (β := ℝ) x (-(↑l : ℝ)) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
Tactic: apply mul_le_mul _ _ (by positivity) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
apply : HPow.hPow (β := ℝ) x (-(↑l : ℝ)) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
⊢ HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have apply₁ : x ^ (k + l) * f ≤ C₁ + C₂
Tactic: apply mul_le_mul _ _ (by positivity) (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ (1 + x) / 2 ≤ x
have linarith : x < (1 + x) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
linarith : x < (1 + x) / 2 → 2 / 2 = 1
⊢ (1 + x) / 2 ≤ x
have linarith₁ : x < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
linarith : x < (1 + x) / 2 → 2 / 2 = 1
linarith₁ : x < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (1 + x) / 2 ≤ x
have linarith₂ : x < (1 + x) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
linarith : x < (1 + x) / 2 → 2 / 2 = 1
linarith₁ : x < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x < (1 + x) / 2 → GT.gt (α := ℝ) 2 0
⊢ (1 + x) / 2 ≤ x
have linarith₃ : x < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
linarith : x < (1 + x) / 2 → 2 / 2 = 1
linarith₁ : x < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x < (1 + x) / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ linarith₅ : x < (1 + x) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ (1 + x) / 2 ≤ x
have linarith₆ : x < (1 + x) / 2 → 1 - x + (2 * x - (HMul.hMul (α := ℝ) 1 1 + 1 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ C₂ ≤ C₁ + C₂
have linarith : C₁ + C₂ < C₂ → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
linarith linarith₁ linarith₂ : C₁ + C₂ < C₂ → HMul.hMul (α := ℝ) 1 1 = 1
⊢ C₂ ≤ C₁ + C₂
have linarith₃ : C₁ + C₂ < C₂ → 0 - f + (f - C₁) + (C₁ + C₂ - C₂) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have x₁ : x ^ k * f = HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f)
Tactic: calc
    x ^ k * f = x ^ (-(l : ℝ)) * (x ^ (k + l) * f) := by
      rw [← Real.rpow_natCast, ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by positivity)]
      simp
    _ ≤ ((1 + x) / 2) ^ (-(l : ℝ)) * (C₁ + C₂) := by
      apply mul_le_mul _ _ (by positivity) (by positivity)
      · exact Real.rpow_le_rpow_of_nonpos (by positivity) (by linarith) (by simp)
      · exact h₂.trans (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this_1 : 0 ≤ C₂
this :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
h'x : 1 ≤ x
x₁ : x ^ k * f = HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f)
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
have x₂ : HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
Tactic: calc
    x ^ k * f = x ^ (-(l : ℝ)) * (x ^ (k + l) * f) := by
      rw [← Real.rpow_natCast, ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by positivity)]
      simp
    _ ≤ ((1 + x) / 2) ^ (-(l : ℝ)) * (C₁ + C₂) := by
      apply mul_le_mul _ _ (by positivity) (by positivity)
      · exact Real.rpow_le_rpow_of_nonpos (by positivity) (by linarith) (by simp)
      · exact h₂.trans (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ
have hf₁ : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ
Tactic: apply ((integrable_pow_neg_integrablePower μ).const_mul (2 ^ μ.integrablePower * (C₁ + C₂))).mono'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
hf₁ : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ
have h : ∀ᵐ (a : E) ∂μ,
  ‖‖a‖ ^ k * ‖f a‖‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ))
Tactic: apply ((integrable_pow_neg_integrablePower μ).const_mul (2 ^ μ.integrablePower * (C₁ + C₂))).mono'
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ ∀ᵐ (a : E) ∂μ,
    ‖‖a‖ ^ k * ‖f a‖‖ ≤
      HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ))
have h : ∀ (v : E),
  ‖‖v‖ ^ k * ‖f v‖‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))
Tactic: filter_upwards with v
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : E
⊢ ‖‖v‖ ^ k * ‖f v‖‖ ≤
    HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))
have h : ‖v‖ ^ k * ‖f v‖ ≤
  HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖v‖) (-(↑μ.integrablePower : ℝ))
Tactic: simp only [norm_mul, norm_pow, norm_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 : MeasurableSpace E
inst_2 : NormedAddCommGroup F
μ : Measure E
inst_3 : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤
    (HPow.hPow (α := ℝ) 2 μ.integrablePower * ∫ (x : E), HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑μ.integrablePower : ℝ)) ∂μ) *
      (C₁ + C₂)
have rw : LE.le (α := ℝ) (∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ)
  (∫ (a : E),
    HPow.hPow (α := ℝ) 2 μ.integrablePower * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ)) * (C₁ + C₂) ∂μ)
Tactic: rw [← integral_const_mul, ← integral_mul_const]