awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
apply :
  @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
⊢ IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume

Tactic:
apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)

Premises used: MeasureTheory.Integrable.mono_measure, Set.Ico_subset_Icc_self, MeasureTheory.Measure.restrict_mono_set
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
hφ : @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
hf₁ :
  MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
⊢ @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
apply Integrable.mul_of_top_left

Premises used: MeasureTheory.Integrable.mul_of_top_left
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
⊢ @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
hf.integrableOn_isCompact isCompact_Icc

Premises used: AntitoneOn.integrableOn_isCompact, MeasureTheory.IntegrableOn, CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
⊢ @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
exact hf.integrableOn_isCompact isCompact_Icc

Premises used: AntitoneOn.integrableOn_isCompact, CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
hf₁ : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ g (x - 1)) (Icc (↑a : ℝ) (↑b : ℝ))
⊢ MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
apply MonotoneOn.memLp_isCompact isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MonotoneOn.memLp_isCompact
-- Module: Mathlib.Analysis.SumIntegralComparisons
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)
hf₃ : x - 1 ≤ y - 1
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) x) ((fun (x : ℝ) ↦ g (x - 1)) y)

Tactic:
apply hg
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simpa using hy
-- Module: Mathlib.Analysis.SumIntegralComparisons
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
⊢ x - 1 ≤ y - 1

Tactic:
simpa using hxy
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
⊢ 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
⊢ 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
have hk : (0 : ℝ) < ↑k + 1 := by positivity
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ (@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
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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)
rw : (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≠ 0
⊢ Ne (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      a ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * a)))
    0

Tactic:
rw [key]
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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)
⊢ (1 / c) ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * Gamma (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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)
⊢ 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)
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
rw :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦ x ^ k * rexp (-(c * x))) ≤
    (↑k ! : ℝ) / c ^ (k + 1)
⊢ ∫ (x : ℝ) in 0..M, x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)

Tactic:
rw [intervalIntegral.integral_of_le hM]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
⊢ 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:
simp [add_sub_cancel_right, rpow_natCast]

Premises used: add_sub_cancel_right, Real.rpow_natCast
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
apply :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))
⊢ 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:
apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE

Premises used: MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, Set.Ioc_subset_Ioi_self
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
h :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    0 x ≤ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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 : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 x ≤ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))

Tactic:
mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)

Premises used: mul_nonneg, LT.lt.le, Real.exp_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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 : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 x ≤ x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))

Tactic:
exact mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)

Premises used: mul_nonneg, LT.lt.le, Real.exp_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
simp_rw : (↑k ! : ℝ) * (c ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ = (↑k ! : ℝ) * (HPow.hPow (β := ℝ) c (↑(k + 1) : ℝ))⁻¹
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) =
    (↑k ! : ℝ) / 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]

Premises used: Real.inv_rpow, LT.lt.le, div_eq_mul_inv, mul_comm, Real.Gamma_nat_eq_factorial, one_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑k ! : ℝ) * (c ^ (k + 1))⁻¹ = (↑k ! : ℝ) * (c ^ (k + 1))⁻¹
⊢ (↑k ! : ℝ) * (c ^ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ = (↑k ! : ℝ) * (HPow.hPow (β := ℝ) c (↑(k + 1) : ℝ))⁻¹

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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)))
calc₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 - 1) * rexp (-(c * x))) =
    (↑k ! : ℝ) / c ^ (k + 1)
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc 0 M)) fun (x : ℝ) ↦ x ^ k * 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

Premises used: Set.Ioc, Set.Ioi, HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
gpos : 0 ≤ rexp (-(c * 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))))

Tactic:
apply sum_mul_Ico_le_integral_of_monotone_antitone
      (f := fun x ↦ x ^ k) (g := fun x ↦ rexp (- (c * x)))

Premises used: sum_mul_Ico_le_integral_of_monotone_antitone
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ M

Tactic:
Nat.zero_le M

Premises used: Nat.zero_le
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ M

Tactic:
exact Nat.zero_le M

Premises used: Nat.zero_le
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑0 : ℝ) (↑M : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑0 : ℝ) (↑M : ℝ)) y
hxy : x ≤ y
⊢ 0 ≤ x

Tactic:
simpa using hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑0 : ℝ) (↑M : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑0 : ℝ) (↑M : ℝ)) y
hxy : x ≤ y
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ x ^ k) x) ((fun (x : ℝ) ↦ x ^ k) y)

Tactic:
apply pow_le_pow_left₀ (by simpa using hx.1) hxy

Premises used: pow_le_pow_left₀
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
hg : -(c * y) ≤ -(c * x)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ rexp (-(c * x))) y) ((fun (x : ℝ) ↦ rexp (-(c * x))) x)

Tactic:
apply exp_monotone

Premises used: Real.exp_monotone
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
hg : c * x ≤ c * y
⊢ -(c * y) ≤ -(c * x)

Tactic:
simp only [neg_le_neg_iff]

Premises used: neg_le_neg_iff
-- Module: Mathlib.Analysis.SumIntegralExpDecay
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
hg : 0 ≤ c
⊢ c * x ≤ c * y

Tactic:
gcongr
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) k

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * HSub.hSub (α := ℝ) (↑M : ℝ) 1))

Tactic:
apply exp_nonneg

Premises used: Real.exp_nonneg
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
simp : ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (c - c * x) ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
⊢ ∫ (x : ℝ) in (↑0 : ℝ)..(↑M : ℝ), x ^ k * rexp (-(c * (x - 1))) ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c

Tactic:
simp only [mul_sub, mul_one, neg_sub, CharP.cast_eq_zero]

Premises used: CharP.cast_eq_zero, neg_sub, mul_sub, mul_one
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
simp : ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
⊢ ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (c - c * x) ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c

Tactic:
simp only [sub_eq_add_neg, Real.exp_add, mul_comm (rexp c), ← mul_assoc]

Premises used: mul_assoc, sub_eq_add_neg, Real.exp, mul_comm, Real.exp_add
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
rw : (∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x))) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c
⊢ ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c

Tactic:
rw [intervalIntegral.integral_mul_const]

Premises used: intervalIntegral.integral_mul_const
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
hbc : ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)
⊢ (∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x))) * rexp c ≤ (↑k ! : ℝ) / c ^ (k + 1) * rexp c

Tactic:
gcongr
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ LE.le (α := ℝ) 0 (↑M : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..(↑M : ℝ), x ^ k * rexp (-(c * x)) ≤ (↑k ! : ℝ) / c ^ (k + 1)

Tactic:
exact intervalIntegral_pow_mul_exp_neg_le (by simp) hc

Premises used: intervalIntegral_pow_mul_exp_neg_le
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ (↑k ! : ℝ) / c ^ (k + 1) * rexp c = rexp c * (↑k ! : ℝ) / c ^ (k + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∑ i ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑i : ℝ) k * rexp (-(c * (↑i : ℝ))) ≤ rexp c * (↑k ! : ℝ) / c ^ (k + 1)

Tactic:
sum_Ico_pow_mul_exp_neg_le (M := M + 1) hc

Premises used: sum_Ico_pow_mul_exp_neg_le, Finset.Icc, Finset.Iic
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
rw : rexp (log 2 * -(c * (↑i : ℝ)))
| HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ)))

Tactic:
rw [← exp_log zero_lt_two, ← exp_mul]

Premises used: Real.exp_mul, Real.exp_log, zero_lt_two
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
conv_lhs : rexp (log 2 * -(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
⊢ HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))

Tactic:
conv_lhs => rw [← exp_log zero_lt_two, ← exp_mul]

Premises used: Real.exp_mul, Real.exp_log, zero_lt_two
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
e_x : log 2 * -(c * (↑i : ℝ)) = -(log 2 * c) * (↑i : ℝ)
⊢ rexp (log 2 * -(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))

Tactic:
congr 1
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
i : ℕ
⊢ log 2 * -(c * (↑i : ℝ)) = -(log 2 * c) * (↑i : ℝ)

Tactic:
ring