[GOAL]
a b : ℝ
h : 0 < b
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
[PROOFSTEP]
have : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b)) :=
  by
  refine' Tendsto.div_const (Tendsto.neg _) _
  exact tendsto_exp_atBot.comp (tendsto_id.neg_const_mul_atTop (Right.neg_neg_iff.2 h))
[GOAL]
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
[PROOFSTEP]
refine' Tendsto.div_const (Tendsto.neg _) _
[GOAL]
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => exp (-b * x)) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_exp_atBot.comp (tendsto_id.neg_const_mul_atTop (Right.neg_neg_iff.2 h))
[GOAL]
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
[PROOFSTEP]
refine' integrableOn_Ioi_deriv_of_nonneg' (fun x _ => _) (fun x _ => (exp_pos _).le) this
[GOAL]
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x => -exp (-b * x) / b) (exp (-b * x)) x
[PROOFSTEP]
simpa [h.ne'] using ((hasDerivAt_id x).const_mul b).neg.exp.neg.div_const b
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
cases' h2.isBigOWith with c h3
[GOAL]
case intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c : ℝ
h3 : Asymptotics.IsBigOWith c atTop f fun x => exp (-b * x)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
rw [Asymptotics.isBigOWith_iff, eventually_atTop] at h3 
[GOAL]
case intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c : ℝ
h3 : ∃ a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
cases' h3 with r bdr
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
let v := max a r
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
have int_left : IntegrableOn f (Ioc a v) :=
  by
  rw [← intervalIntegrable_iff_integrable_Ioc_of_le (le_max_left a r)]
  have u : Icc a v ⊆ Ici a := Icc_subset_Ici_self
  exact (h1.mono u).intervalIntegrable_of_Icc (le_max_left a r)
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
⊢ IntegrableOn f (Ioc a v)
[PROOFSTEP]
rw [← intervalIntegrable_iff_integrable_Ioc_of_le (le_max_left a r)]
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
⊢ IntervalIntegrable f volume a (max a r)
[PROOFSTEP]
have u : Icc a v ⊆ Ici a := Icc_subset_Ici_self
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
u : Icc a v ⊆ Ici a
⊢ IntervalIntegrable f volume a (max a r)
[PROOFSTEP]
exact (h1.mono u).intervalIntegrable_of_Icc (le_max_left a r)
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
suffices IntegrableOn f (Ioi v) by
  have t := integrableOn_union.mpr ⟨int_left, this⟩
  simpa only [Ioc_union_Ioi_eq_Ioi, le_max_iff, le_refl, true_or_iff] using t
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : IntegrableOn f (Ioi v)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
have t := integrableOn_union.mpr ⟨int_left, this⟩
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : IntegrableOn f (Ioi v)
t : IntegrableOn f (Ioc a v ∪ Ioi v)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
simpa only [Ioc_union_Ioi_eq_Ioi, le_max_iff, le_refl, true_or_iff] using t
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ IntegrableOn f (Ioi v)
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.left
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ AEStronglyMeasurable f (Measure.restrict volume (Ioi v))
[PROOFSTEP]
exact (h1.mono <| Ioi_subset_Ici <| le_max_left a r).aestronglyMeasurable measurableSet_Ioi
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ HasFiniteIntegral f
[PROOFSTEP]
have : HasFiniteIntegral (fun x : ℝ => c * exp (-b * x)) (volume.restrict (Ioi v)) :=
  (exp_neg_integrableOn_Ioi v h0).hasFiniteIntegral.const_mul c
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
⊢ HasFiniteIntegral f
[PROOFSTEP]
apply this.mono
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi v), ‖f a‖ ≤ ‖c * exp (-b * a)‖
[PROOFSTEP]
refine' (ae_restrict_iff' measurableSet_Ioi).mpr _
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi v → ‖f x‖ ≤ ‖c * exp (-b * x)‖
[PROOFSTEP]
refine' ae_of_all _ fun x h1x => _
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : x ∈ Ioi v
⊢ ‖f x‖ ≤ ‖c * exp (-b * x)‖
[PROOFSTEP]
rw [norm_mul, norm_eq_abs]
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : x ∈ Ioi v
⊢ |f x| ≤ ‖c‖ * ‖exp (-b * x)‖
[PROOFSTEP]
rw [mem_Ioi] at h1x 
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : v < x
⊢ |f x| ≤ ‖c‖ * ‖exp (-b * x)‖
[PROOFSTEP]
specialize bdr x ((le_max_right a r).trans h1x.le)
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : v < x
bdr : ‖f x‖ ≤ c * ‖exp (-b * x)‖
⊢ |f x| ≤ ‖c‖ * ‖exp (-b * x)‖
[PROOFSTEP]
exact bdr.trans (mul_le_mul_of_nonneg_right (le_abs_self c) (norm_nonneg _))
