awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) x) ((fun (x : ℝ) ↦ g (x - 1)) y)
have hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) x) ((fun (x : ℝ) ↦ g (x - 1)) y)
have hf₂ : y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hf₂ : y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) x) ((fun (x : ℝ) ↦ g (x - 1)) y)
have hf₃ : x - 1 ≤ y - 1
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (hypothesis)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)
have hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
Tactic: have hk : (0 : ℝ) < ↑k + 1 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (hypothesis)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)
have key : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
  (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
Tactic: have key := integral_rpow_mul_exp_neg_mul_Ioi hk hc
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
⊢ Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      a ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * a)))
    0
have rw : (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≠ 0
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (hypothesis)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)
have hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
Tactic: have hint : IntegrableOn (fun x ↦ x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x))) (Ioi 0) :=
    .of_integral_ne_zero (by rw [key]; positivity)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)
have rw : (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦ x ^ k * rexp (-(c * x))) ≤
  (↑k ! : ℝ) / c ^ (k + 1)
Tactic: rw [intervalIntegral.integral_of_le hM]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
have apply : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
  x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))
Tactic: apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), 0 x ≤ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) =
    (↑k ! : ℝ) / c ^ (k + 1)
have simp_rw : (↑k ! : ℝ) * (c ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ = (↑k ! : ℝ) * (HPow.hPow (β := ℝ) c (↑(k + 1) : ℝ))⁻¹
Tactic: simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ (↑k ! : ℝ) * (c ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ = (↑k ! : ℝ) * (HPow.hPow (β := ℝ) c (↑(k + 1) : ℝ))⁻¹
have norm_cast : (↑k ! : ℝ) * (c ^ (k + 1))⁻¹ = (↑k ! : ℝ) * (c ^ (k + 1))⁻¹
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦ x ^ k * rexp (-(c * x))) ≤
    (↑k ! : ℝ) / c ^ (k + 1)
have calc : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
    x ^ k * rexp (-(c * x)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
Tactic: calc ∫ x in Ioc (0 : ℝ) M, x ^ k * rexp (-(c * x))
    _ = ∫ x in Ioc (0 : ℝ) M, x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        simp [add_sub_cancel_right, rpow_natCast]
    _ ≤ ∫ x in Ioi (0 : ℝ), x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE
        filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
        exact mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)
    _ = k ! / c ^ (k + 1) := by
        simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]
        norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
calc :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
      x ^ k * rexp (-(c * x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦ x ^ k * rexp (-(c * x))) ≤
    (↑k ! : ℝ) / c ^ (k + 1)
have calc₁ : LE.le (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
Tactic: calc ∫ x in Ioc (0 : ℝ) M, x ^ k * rexp (-(c * x))
    _ = ∫ x in Ioc (0 : ℝ) M, x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        simp [add_sub_cancel_right, rpow_natCast]
    _ ≤ ∫ x in Ioi (0 : ℝ), x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE
        filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
        exact mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)
    _ = k ! / c ^ (k + 1) := by
        simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]
        norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
key :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * t))) =
    (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
calc :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
      x ^ k * rexp (-(c * x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
calc₁ :
  LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x)))
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦ x ^ k * rexp (-(c * x))) ≤
    (↑k ! : ℝ) / c ^ (k + 1)
have calc₂ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) =
  (↑k ! : ℝ) / c ^ (k + 1)
Tactic: calc ∫ x in Ioc (0 : ℝ) M, x ^ k * rexp (-(c * x))
    _ = ∫ x in Ioc (0 : ℝ) M, x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        simp [add_sub_cancel_right, rpow_natCast]
    _ ≤ ∫ x in Ioi (0 : ℝ), x ^ ((↑k + 1 : ℝ) - 1) * rexp (-(c * x)) := by
        apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE
        filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
        exact mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)
    _ = k ! / c ^ (k + 1) := by
        simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]
        norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico 0 M, HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-(c * (↑i : ℝ))))
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))))
have hab : 0 ≤ M
Tactic: apply sum_mul_Ico_le_integral_of_monotone_antitone
      (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
hab : 0 ≤ M
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico 0 M, HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-(c * (↑i : ℝ))))
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))))
have hf : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (Icc (↑0 : ℝ) (↑M : ℝ))
Tactic: apply sum_mul_Ico_le_integral_of_monotone_antitone
      (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
hab : 0 ≤ M
hf : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (Icc (↑0 : ℝ) (↑M : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico 0 M, HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-(c * (↑i : ℝ))))
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))))
have hg : AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ rexp (-(c * x)))
  (Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1))
Tactic: apply sum_mul_Ico_le_integral_of_monotone_antitone
      (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
hab : 0 ≤ M
hf : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (Icc (↑0 : ℝ) (↑M : ℝ))
hg :
  AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ rexp (-(c * x)))
    (Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico 0 M, HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-(c * (↑i : ℝ))))
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))))
have fpos : 0 ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) k
Tactic: apply sum_mul_Ico_le_integral_of_monotone_antitone
      (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
hab : 0 ≤ M
hf : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (Icc (↑0 : ℝ) (↑M : ℝ))
hg :
  AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ rexp (-(c * x)))
    (Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1))
fpos : 0 ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) k
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico 0 M, HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-(c * (↑i : ℝ))))
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))))
have gpos : 0 ≤ rexp (-(c * HSub.hSub (α := ℝ) (↑M : ℝ) 1))
Tactic: apply sum_mul_Ico_le_integral_of_monotone_antitone
      (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1)
y : ℝ
hy : y ∈ Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1)
hxy : x ≤ y
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ rexp (-(c * x))) y) ((fun (x : ℝ) ↦ rexp (-(c * x))) x)
have hg : -(c * y) ≤ -(c * x)
Tactic: apply exp_monotone
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1)
y : ℝ
hy : y ∈ Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1)
hxy : x ≤ y
⊢ -(c * y) ≤ -(c * x)
have hg : c * x ≤ c * y
Tactic: simp only [neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1)
y : ℝ
hy : y ∈ Icc (HSub.hSub (α := ℝ) (↑0 : ℝ) 1) (HSub.hSub (α := ℝ) (↑M : ℝ) 1)
hxy : x ≤ y
⊢ c * x ≤ c * y
have hg : 0 ≤ c
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))) ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
have simp : ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (c - c * x) ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
Tactic: simp only [mul_sub, mul_one, neg_sub, CharP.cast_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (c - c * x) ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
have simp : ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
Tactic: simp only [sub_eq_add_neg, Real.exp_add, mul_comm (rexp c), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
have rw : (∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x))) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
Tactic: rw [intervalIntegral.integral_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ (∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x))) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
have hbc : ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
| HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ)))
have rw : rexp (log 2 * -(c * (↑i : ℝ)))
Tactic: rw [← exp_log zero_lt_two, ← exp_mul]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
⊢ HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
have conv_lhs : rexp (log 2 * -(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
Tactic: conv_lhs => rw [← exp_log zero_lt_two, ← exp_mul]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
⊢ rexp (log 2 * -(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
have e_x : log 2 * -(c * (↑i : ℝ)) = -(log 2 * c) * (↑i : ℝ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (hypothesis)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∑ i ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑i : ℝ) k * HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) ≤
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
have A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
Tactic: have A (i : ℕ) : (2 : ℝ) ^ (- (c * i)) = rexp (- (Real.log 2 * c) * i) := by
    conv_lhs => rw [← exp_log zero_lt_two, ← exp_mul]
    congr 1
    ring
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
⊢ ∑ i ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑i : ℝ) k * HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) ≤
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
have simp : ∑ x ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑x : ℝ) k * rexp (-(log 2 * c * (↑x : ℝ))) ≤
  HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
Tactic: simp only [A, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
⊢ ∑ x ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑x : ℝ) k * rexp (-(log 2 * c * (↑x : ℝ))) ≤
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
have apply : rexp (log 2 * c) * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
Tactic: apply (sum_Iic_pow_mul_exp_neg_le (by positivity)).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
⊢ rexp (log 2 * c) * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
have rw : rexp (log 2) ^ c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
Tactic: rw [exp_mul, exp_log zero_lt_two]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralExpDecay (goal)
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
rw : rexp (log 2) ^ c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
⊢ rexp (log 2 * c) * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
have rw₁ : HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) =
  HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
Tactic: rw [exp_mul, exp_log zero_lt_two]
-- Lean 4 proof step from Mathlib.Analysis.SumOverResidueClass (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
m : ℕ
inst_1 : NeZero m
f : ℕ → R
⊢ f = ∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f
have h : ∀ (n : ℕ), f n = (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f) n
Tactic: ext n