case refine_1
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
⊢ IntegrableOn g' (Ioc a (id x))

case refine_2
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ (fun k => g k - g a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖
case refine_2
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
apply Tendsto.congr' _ (hg.sub_const _)
case h
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ (fun k => g k - g a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖
filter_upwards [Ioi_mem_atTop a] with x hx
case h
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
case h
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
have h'x : a ≤ id x := le_of_lt hx
no goals
case h
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
calc
  g x - g a = ∫ y in a..id x, g' y := by
    symm
    apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x
      (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
    rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
    exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
      (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1
  _ = ∫ y in a..id x, ‖g' y‖ := by
    simp_rw [intervalIntegral.integral_of_le h'x]
    refine' set_integral_congr measurableSet_Ioc fun y hy => _
    dsimp
    rw [abs_of_nonneg]
    exact g'pos _ hy.1
no goals
case refine_1
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
⊢ IntegrableOn g' (Ioc a (id x))
exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
  (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (y : ℝ) in a..id x, g' y) = g x - g a
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (y : ℝ) in a..id x, g' y
symm
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable (fun y => g' y) volume a (id x)
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (y : ℝ) in a..id x, g' y) = g x - g a
apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x
  (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (fun y => g' y) (Ioc a (id x))
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable (fun y => g' y) volume a (id x)
rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
no goals
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (fun y => g' y) (Ioc a (id x))
exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
  (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (x : ℝ) in Ioc a (id x), g' x) = ∫ (x : ℝ) in Ioc a (id x), ‖g' x‖
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (y : ℝ) in a..id x, g' y) = ∫ (y : ℝ) in a..id x, ‖g' y‖
simp_rw [intervalIntegral.integral_of_le h'x]
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = ‖g' y‖
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (x : ℝ) in Ioc a (id x), g' x) = ∫ (x : ℝ) in Ioc a (id x), ‖g' x‖
refine' set_integral_congr measurableSet_Ioc fun y hy => _
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = abs (g' y)
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = ‖g' y‖
dsimp
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ 0 ≤ g' y
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = abs (g' y)
rw [abs_of_nonneg]
no goals
E : Type ?u.153019
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ 0 ≤ g' y
exact g'pos _ hy.1