case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioc a b)

case neg
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : ¬a < b
⊢ IntegrableOn g' (Ioc a b)
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
⊢ IntegrableOn g' (Ioc a b)
by_cases hab : a < b
case neg
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : ¬a < b
⊢ IntegrableOn g' (Ioc a b)

case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioc a b)
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioc a b)

case neg
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : ¬a < b
⊢ IntegrableOn g' (Ioc a b)
swap
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioo a b)
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioc a b)
rw [integrableOn_Ioc_iff_integrableOn_Ioo]
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
⊢ IntegrableOn g' (Ioo a b)
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioo a b)
have meas_g' : AEMeasurable g' (volume.restrict (Ioo a b)) := by
  apply (aemeasurable_derivWithin_Ioi g _).congr
  refine' (ae_restrict_mem measurableSet_Ioo).mono fun x hx => _
  exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _)
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : (∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
⊢ IntegrableOn g' (Ioo a b)

case H
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
⊢ (∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
⊢ IntegrableOn g' (Ioo a b)
suffices H : (∫⁻ x in Ioo a b, ‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
case H
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
⊢ (∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
case pos
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : (∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
⊢ IntegrableOn g' (Ioo a b)

case H
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
⊢ (∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
exact ⟨meas_g'.aestronglyMeasurable, H.trans_lt ENNReal.ofReal_lt_top⟩
case H
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
⊢ False
case H
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
⊢ (∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a)
by_contra' H
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
⊢ False
case H
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
⊢ False
obtain ⟨f, fle, fint, hf⟩ :
  ∃ f : SimpleFunc ℝ ℝ≥0,
    (∀ x, f x ≤ ‖g' x‖₊) ∧
      (∫⁻ x : ℝ in Ioo a b, f x) < ∞ ∧ ENNReal.ofReal (g b - g a) < ∫⁻ x : ℝ in Ioo a b, f x :=
  exists_lt_lintegral_simpleFunc_of_lt_lintegral H
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
⊢ False
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
⊢ False
let F : ℝ → ℝ := (↑) ∘ f
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
intF : IntegrableOn F (Ioo a b)
⊢ False
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
⊢ False
have intF : IntegrableOn F (Ioo a b) := by
  refine' ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, _⟩
  simpa only [HasFiniteIntegral, comp_apply, NNReal.nnnorm_eq] using fint
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ False
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
intF : IntegrableOn F (Ioo a b)
⊢ False
have A : (∫⁻ x : ℝ in Ioo a b, f x) = ENNReal.ofReal (∫ x in Ioo a b, F x) :=
  lintegral_coe_eq_integral _ intF
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ False
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ False
rw [A] at hf
no goals
case H.intro.intro.intro
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
B : (∫ (x : ℝ) in Ioo a b, F x) ≤ g b - g a
⊢ False
exact lt_irrefl _ (hf.trans_le (ENNReal.ofReal_le_ofReal B))
no goals
case neg
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : ¬a < b
⊢ IntegrableOn g' (Ioc a b)
simp [Ioc_eq_empty hab]
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ (fun x => derivWithin g (Ioi x) x) =ᵐ[Measure.restrict volume (Ioo a b)] g'
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ AEMeasurable g'
apply (aemeasurable_derivWithin_Ioi g _).congr
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ (fun x => derivWithin g (Ioi x) x) x = g' x
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
⊢ (fun x => derivWithin g (Ioi x) x) =ᵐ[Measure.restrict volume (Ioo a b)] g'
refine' (ae_restrict_mem measurableSet_Ioo).mono fun x hx => _
no goals
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ (fun x => derivWithin g (Ioi x) x) x = g' x
exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _)
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
⊢ HasFiniteIntegral F
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
⊢ IntegrableOn F (Ioo a b)
refine' ⟨f.measurable.coe_nnreal_real.aestronglyMeasurable, _⟩
no goals
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
⊢ HasFiniteIntegral F
simpa only [HasFiniteIntegral, comp_apply, NNReal.nnnorm_eq] using fint
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ (∫ (x : ℝ) in a..b, F x) ≤ g b - g a
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ (∫ (x : ℝ) in Ioo a b, F x) ≤ g b - g a
rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le hab.le]
case refine_1
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ IntegrableOn (fun x => F x) (Icc a b)

case refine_2
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
x : ℝ
hx : x ∈ Ioo a b
⊢ F x ≤ g' x
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ (∫ (x : ℝ) in a..b, F x) ≤ g b - g a
refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_
no goals
case refine_1
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ IntegrableOn (fun x => F x) (Icc a b)
rwa [integrableOn_Icc_iff_integrableOn_Ioo]
case h.e'_4
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
x : ℝ
hx : x ∈ Ioo a b
⊢ g' x = ↑‖g' x‖₊
case refine_2
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
x : ℝ
hx : x ∈ Ioo a b
⊢ F x ≤ g' x
convert NNReal.coe_le_coe.2 (fle x)
no goals
case h.e'_4
ι : Type ?u.1865205
𝕜 : Type ?u.1865208
E : Type ?u.1865211
F✝ : Type ?u.1865214
A✝ : Type ?u.1865217
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g φ : ℝ → ℝ
f✝ f' : ℝ → E
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ (x : ℝ), x ∈ Ioo a b → 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g'
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊
fint : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) < ⊤
F : ℝ → ℝ := NNReal.toReal ∘ ↑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b)
A : (∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
x : ℝ
hx : x ∈ Ioo a b
⊢ g' x = ↑‖g' x‖₊
simp only [Real.norm_of_nonneg (g'pos x hx), coe_nnnorm]