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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
a : Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)
⊢ Real.exp (Real.log 2 * ((↑n : ℝ) - r)) ≤ Real.exp (Real.log (3 / 2) * (↑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
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
apply : Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log 2 * ((↑N : ℝ) - r)
⊢ Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log (3 / 2) * (↑k : ℝ)

Tactic:
apply le_trans _ hk₂

Premises used: 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_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
ha : 0 ≤ Real.log 2
⊢ Real.log 2 * ((↑n : ℝ) - r) ≤ Real.log 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 : ℝ
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₁ : 0 < 3 / 2
⊢ Real.exp (Real.log (3 / 2) * (↑k : ℝ)) ≤ (3 / 2) ^ k

Tactic:
rw [← Real.rpow_natCast, Real.rpow_def_of_pos]

Premises used: Real.rpow_def_of_pos, 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 : ContDiffAt ℝ (F := ℝ) (↑n : ℕ∞ω) (fun (x : ℝ) ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
⊢ 0 < 3 / 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
hx'' : 0 < x
h_1 : r - (↑n : ℝ) < 0
h : 0 < (↑n : ℝ) - r
hab : 3 / 2 ≤ 1 + |x|
⊢ (3 / 2) ^ k ≤ (1 + |x|) ^ k

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 : ℝ
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 ≤ 1 + |x|

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_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
In₅ : (3 / 2) ^ k ≤ (1 + |x|) ^ k
⊢ |x| ^ (r - (↑n : ℝ)) ≤ (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

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.exp, Nat.cast, Real.log, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
μ : Measure E
h : μ.HasTemperateGrowth
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑μ.integrablePower : ℝ))) μ

Tactic:
simpa [Measure.integrablePower, h] using h.exists_integrable.choose_spec

Premises used: Exists.choose_spec, MeasureTheory.Measure.HasTemperateGrowth.exists_integrable, MeasureTheory.Measure.integrablePower
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
μ : Measure E
h : IsFiniteMeasure μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑0 : ℝ))) μ

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
hnr : LT.lt (α := ℝ) (↑(finrank ℝ E) : ℝ) (↑(finrank ℝ E + 1) : ℝ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(finrank ℝ E + 1) : ℝ))) μ

Tactic:
apply integrable_one_add_norm

Premises used: integrable_one_add_norm
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ LT.lt (α := ℝ) (↑(finrank ℝ E) : ℝ) (↑(finrank ℝ E + 1) : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
⊢ 0 ≤ x ^ (k + l) * f

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
Goal:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
⊢ 0 ≤ C₂

Tactic:
have : 0 ≤ C₂ := le_trans (by positivity) h₂
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
⊢ 0 ≤ 1 + x

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
rw :
  HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) / HPow.hPow (α := ℝ) (β := ℝ) 2 (-(↑l : ℝ)) * (C₁ + C₂)
⊢ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)

Tactic:
rw [Real.div_rpow (by positivity) zero_le_two]

Premises used: Real.div_rpow, zero_le_two
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂
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₂)
⊢ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) =
    HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ)) / HPow.hPow (α := ℝ) (β := ℝ) 2 (-(↑l : ℝ)) * (C₁ + C₂)

Tactic:
simp [div_eq_inv_mul, ← Real.rpow_neg_one, ← Real.rpow_mul]

Premises used: Real.rpow_neg_one, div_eq_inv_mul, Real.rpow_mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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) (-1) =
    HPow.hPow (α := ℝ) 2 l * HPow.hPow (β := ℝ) ((1 + x) ^ l) (-1) * (C₁ + C₂)

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂)

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
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂)
rw : x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
⊢ x ^ k * f ≤ HPow.hPow (α := ℝ) 2 l * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + x) (-(↑l : ℝ))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂)
inr : ∀ (h'x : 1 ≤ x), x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)

Tactic:
rcases le_total x 1 with h'x | h'x

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ))
inl₁ : f ≤ C₁ + C₂
⊢ x ^ k * f ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : 1 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))
⊢ x ^ k ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))

Tactic:
apply (pow_le_one₀ hx h'x).trans

Premises used: LE.le.trans, pow_le_one₀
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
inl₂ : LE.le (α := ℝ) (-(↑l : ℝ)) 0
⊢ 1 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))

Tactic:
apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos

Premises used: Real.one_le_rpow_of_pos_of_le_one_of_nonpos
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 0 < (1 + x) / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
linarith₆ : 1 < (1 + x) / 2 → x - 1 + (HMul.hMul (α := ℝ) 2 1 - (HMul.hMul (α := ℝ) 1 1 + 1 * x)) = 0
⊢ (1 + x) / 2 ≤ 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ LE.le (α := ℝ) (-(↑l : ℝ)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
linarith₃ : C₁ + C₂ < f → f - C₁ + (0 - C₂) + (C₁ + C₂ - f) = 0
⊢ f ≤ C₁ + C₂

Tactic:
linarith
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 0 < x

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
rw : HPow.hPow (β := ℝ) x (↑k : ℝ) * f = x ^ HAdd.hAdd (α := ℝ) (-(↑l : ℝ)) (↑(k + l) : ℝ) * f
⊢ x ^ k * f = HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f)

Tactic:
rw [← Real.rpow_natCast, ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by positivity)]

Premises used: mul_assoc, Real.rpow_add, Real.rpow_natCast
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 (↑k : ℝ) * f = x ^ HAdd.hAdd (α := ℝ) (-(↑l : ℝ)) (↑(k + l) : ℝ) * f

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 0 ≤ x ^ (k + l) * f

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 0 ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ))
apply₁ : x ^ (k + l) * f ≤ C₁ + C₂
⊢ HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)

Tactic:
apply mul_le_mul _ _ (by positivity) (by positivity)

Premises used: mul_le_mul
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ 0 < (1 + x) / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
linarith₆ : x < (1 + x) / 2 → 1 - x + (2 * x - (HMul.hMul (α := ℝ) 1 1 + 1 * x)) = 0
⊢ (1 + x) / 2 ≤ x

Tactic:
linarith
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
⊢ LE.le (α := ℝ) (-(↑l : ℝ)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 : ℝ)) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ))

Tactic:
exact Real.rpow_le_rpow_of_nonpos (by positivity) (by linarith) (by simp)

Premises used: Real.rpow_le_rpow_of_nonpos
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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
linarith₃ : C₁ + C₂ < C₂ → 0 - f + (f - C₁) + (C₁ + C₂ - C₂) = 0
⊢ C₂ ≤ C₁ + C₂

Tactic:
linarith
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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 + l) * f ≤ C₁ + C₂

Tactic:
exact h₂.trans (by linarith)

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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₂ : HPow.hPow (β := ℝ) x (-(↑l : ℝ)) * (x ^ (k + l) * f) ≤ HPow.hPow (β := ℝ) ((1 + x) / 2) (-(↑l : ℝ)) * (C₁ + C₂)
⊢ x ^ k * 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)

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Distribution.TemperateGrowth
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‖) μ
h :
  ∀ᵐ (a : E) ∂μ,
    ‖‖a‖ ^ k * ‖f a‖‖ ≤
      HPow.hPow (α := ℝ) 2 μ.integrablePower * (C₁ + C₂) * HPow.hPow (β := ℝ) (1 + ‖a‖) (-(↑μ.integrablePower : ℝ))
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * ‖f x‖) μ

Tactic:
apply ((integrable_pow_neg_integrablePower μ).const_mul (2 ^ μ.integrablePower * (C₁ + C₂))).mono'

Premises used: HMul.hMul, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', MeasureTheory.Measure.integrablePower, HPow.hPow, HAdd.hAdd, OfNat.ofNat, MeasureTheory.Measure.integrable_pow_neg_integrablePower