English
A variant of the previous FTC type on [a,b], using a slightly different differentiability domain (Ico or Ioo) and integrability assumptions; in short, the same conclusion g(b)−g(a) ≤ ∫ φ.
Русский
Вариант предыдущей теоремы ФТК на интервале [a,b] с немного иным множеством дифференцирования; заключение то же: g(b)−g(a) ≤ ∫ φ.
LaTeX
$$$g(b)-g(a) \\le \\int_{a}^{b} φ(y) dy \\; (при соответствующих условиях дифференцирования и интегрируемости).$$$
Lean4
/-- Hard part of FTC-2 for integrable derivatives, real-valued functions: one has
`g b - g a ≤ ∫ y in a..b, g' y` when `g'` is integrable.
Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`.
We give the slightly more general version that `g b - g a ≤ ∫ y in a..b, φ y` when `g' ≤ φ` and
`φ` is integrable (even if `g'` is not known to be integrable).
Version assuming that `g` is differentiable on `(a, b)`. -/
theorem sub_le_integral_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b))
(hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b))
(hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x) : g b - g a ≤ ∫ y in a..b, φ y := by
-- This follows from the version on a closed-open interval (applied to `[t, b)` for `t` close to
-- `a`) and a continuity argument.
obtain rfl | a_lt_b := hab.eq_or_lt
· simp
set s := {t | g b - g t ≤ ∫ u in t..b, φ u} ∩ Icc a b
have s_closed : IsClosed s :=
by
have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) :=
by
rw [← uIcc_of_le hab] at hcont φint ⊢
exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
simp only [s, inter_comm]
exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod
have A : closure (Ioc a b) ⊆ s := by
apply s_closed.closure_subset_iff.2
intro t ht
refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩
exact
sub_le_integral_of_hasDeriv_right_of_le_Ico ht.2 (hcont.mono (Icc_subset_Icc ht.1.le le_rfl))
(fun x hx => hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩) (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx =>
hφg x ⟨ht.1.trans_le hx.1, hx.2⟩
rw [closure_Ioc a_lt_b.ne] at A
exact (A (left_mem_Icc.2 hab)).1
