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)
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
⊢ IntegrableOn f (Ioi a)
cases' h2.isBigOWith with c h3
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)
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)
rw [Asymptotics.isBigOWith_iff, eventually_atTop] at h3
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)
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)
cases' h3 with r bdr
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)
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)
let v := max a r
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)
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)
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)
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)
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)
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
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))

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
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)
constructor
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
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
have : HasFiniteIntegral (fun x : ℝ => c * exp (-b * x)) (volume.restrict (Ioi v)) :=
  (exp_neg_integrableOn_Ioi v h0).hasFiniteIntegral.const_mul c
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)‖
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
apply this.mono
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)‖
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)‖
refine' (ae_restrict_iff' measurableSet_Ioi).mpr _
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)‖
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)‖
refine' ae_of_all _ fun x h1x => _
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
⊢ abs (f x) ≤ ‖c‖ * ‖exp (-b * x)‖
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)‖
rw [norm_mul, norm_eq_abs]
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
⊢ abs (f x) ≤ ‖c‖ * ‖exp (-b * x)‖
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
⊢ abs (f x) ≤ ‖c‖ * ‖exp (-b * x)‖
rw [mem_Ioi] at h1x
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)‖
⊢ abs (f x) ≤ ‖c‖ * ‖exp (-b * x)‖
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
⊢ abs (f x) ≤ ‖c‖ * ‖exp (-b * x)‖
specialize bdr x ((le_max_right a r).trans h1x.le)
no goals
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)‖
⊢ abs (f x) ≤ ‖c‖ * ‖exp (-b * x)‖
exact bdr.trans (mul_le_mul_of_nonneg_right (le_abs_self c) (norm_nonneg _))
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)
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)
rw [← intervalIntegrable_iff_integrable_Ioc_of_le (le_max_left a r)]
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)
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)
have u : Icc a v ⊆ Ici a := Icc_subset_Ici_self
no goals
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)
exact (h1.mono u).intervalIntegrable_of_Icc (le_max_left a r)
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)
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)
have t := integrableOn_union.mpr ⟨int_left, this⟩
no goals
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)
simpa only [Ioc_union_Ioi_eq_Ioi, le_max_iff, le_refl, true_or_iff] using t
no goals
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))
exact (h1.mono <| Ioi_subset_Ici <| le_max_left a r).aestronglyMeasurable measurableSet_Ioi