English
Let a ≤ b, g be continuous on [a,b], g' ≤ φ on Ico[a,b], and g' is the derivative of g from the right. If φ is integrable on [a,b], then g(b)−g(a) ≤ ∫_{a}^{b} φ.
Русский
Пусть a ≤ b, g непрерывна на [a,b], g' не выше φ на Ico[a,b], и g' — правDerivative от g; если φ интегрируема на [a,b], то g(b)−g(a) ≤ ∫_{a}^{b} φ.
LaTeX
$$$g(b)-g(a) \\le \\int_{a}^{b} \\phi(y)\\,dy \\quad\\text{given } g'\\le \\phi\\text{ on }Ico(a,b),\\; g\\text{ дифференцируема справа }$$$
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_Ico (hab : a ≤ b) (hcont : ContinuousOn g (Icc a b))
(hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x) (φint : IntegrableOn φ (Icc a b))
(hφg : ∀ x ∈ Ico a b, g' x ≤ φ x) : g b - g a ≤ ∫ y in a..b, φ y :=
by
refine
le_of_forall_pos_le_add fun ε εpos =>
?_
-- Bound from above `g'` by a lower-semicontinuous function `G'`.
rcases exists_lt_lowerSemicontinuous_integral_lt φ φint εpos with
⟨G', f_lt_G', G'cont, G'int, G'lt_top, hG'⟩
-- we will show by "induction" that `g t - g a ≤ ∫ u in a..t, G' u` for all `t ∈ [a, b]`.
set s := {t | g t - g a ≤ ∫ u in a..t, (G' u).toReal} ∩ Icc a b
have s_closed : IsClosed s :=
by
have : ContinuousOn (fun t => (g t - g a, ∫ u in a..t, (G' u).toReal)) (Icc a b) :=
by
rw [← uIcc_of_le hab] at G'int hcont ⊢
exact (hcont.sub continuousOn_const).prodMk (continuousOn_primitive_interval G'int)
simp only [s, inter_comm]
exact this.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
have main : Icc a b ⊆ {t | g t - g a ≤ ∫ u in a..t, (G' u).toReal} := by
-- to show that the set `s` is all `[a, b]`, it suffices to show that any point `t` in `s`
-- with `t < b` admits another point in `s` slightly to its right
-- (this is a sort of real induction).
refine
s_closed.Icc_subset_of_forall_exists_gt (by simp only [integral_same, mem_setOf_eq, sub_self, le_rfl])
fun t ht v t_lt_v => ?_
obtain ⟨y, g'_lt_y', y_lt_G'⟩ : ∃ y : ℝ, (g' t : EReal) < y ∧ (y : EReal) < G' t :=
EReal.lt_iff_exists_real_btwn.1
((EReal.coe_le_coe_iff.2 (hφg t ht.2)).trans_lt (f_lt_G' t))
-- bound from below the increase of `∫ x in a..u, G' x` on the right of `t`, using the lower
-- semicontinuity of `G'`.
have I1 : ∀ᶠ u in 𝓝[>] t, (u - t) * y ≤ ∫ w in t..u, (G' w).toReal :=
by
have B : ∀ᶠ u in 𝓝 t, (y : EReal) < G' u := G'cont.lowerSemicontinuousAt _ _ y_lt_G'
rcases mem_nhds_iff_exists_Ioo_subset.1 B with ⟨m, M, ⟨hm, hM⟩, H⟩
have : Ioo t (min M b) ∈ 𝓝[>] t := Ioo_mem_nhdsGT (lt_min hM ht.right.right)
filter_upwards [this] with u hu
have I : Icc t u ⊆ Icc a b := Icc_subset_Icc ht.2.1 (hu.2.le.trans (min_le_right _ _))
calc
(u - t) * y = ∫ _ in Icc t u, y := by
simp only [MeasureTheory.integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter,
hu.left.le, Real.volume_real_Icc_of_le, smul_eq_mul]
_ ≤ ∫ w in t..u, (G' w).toReal :=
by
rw [intervalIntegral.integral_of_le hu.1.le, ← integral_Icc_eq_integral_Ioc]
apply setIntegral_mono_ae_restrict
· simp
· exact IntegrableOn.mono_set G'int I
· have C1 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), G' x < ∞ := ae_mono (Measure.restrict_mono I le_rfl) G'lt_top
have C2 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), x ∈ Icc t u := ae_restrict_mem measurableSet_Icc
filter_upwards [C1, C2] with x G'x hx
apply EReal.coe_le_coe_iff.1
have : x ∈ Ioo m M := by
simp only [hm.trans_le hx.left, (hx.right.trans_lt hu.right).trans_le (min_le_left M b), mem_Ioo,
and_self_iff]
refine (H this).out.le.trans_eq ?_
exact (EReal.coe_toReal G'x.ne (f_lt_G' x).ne_bot).symm
have I2 : ∀ᶠ u in 𝓝[>] t, g u - g t ≤ (u - t) * y :=
by
have g'_lt_y : g' t < y := EReal.coe_lt_coe_iff.1 g'_lt_y'
filter_upwards [(hderiv t ⟨ht.2.1, ht.2.2⟩).limsup_slope_le' (notMem_Ioi.2 le_rfl) g'_lt_y,
self_mem_nhdsWithin] with u hu t_lt_u
have := mul_le_mul_of_nonneg_left hu.le (sub_pos.2 t_lt_u.out).le
rwa [← smul_eq_mul, sub_smul_slope] at this
have I3 : ∀ᶠ u in 𝓝[>] t, g u - g t ≤ ∫ w in t..u, (G' w).toReal := by
filter_upwards [I1, I2] with u hu1 hu2 using hu2.trans hu1
have I4 : ∀ᶠ u in 𝓝[>] t, u ∈ Ioc t (min v b) :=
Ioc_mem_nhdsGT <|
lt_min t_lt_v
ht.2.2
-- choose a point `x` slightly to the right of `t` which satisfies the above bound
rcases (I3.and I4).exists with
⟨x, hx, h'x⟩
-- we check that it belongs to `s`, essentially by construction
refine ⟨x, ?_, Ioc_subset_Ioc le_rfl (min_le_left _ _) h'x⟩
calc
g x - g a = g t - g a + (g x - g t) := by abel
_ ≤ (∫ w in a..t, (G' w).toReal) + ∫ w in t..x, (G' w).toReal := (add_le_add ht.1 hx)
_ = ∫ w in a..x, (G' w).toReal := by
apply integral_add_adjacent_intervals
· rw [intervalIntegrable_iff_integrableOn_Ioc_of_le ht.2.1]
exact IntegrableOn.mono_set G'int (Ioc_subset_Icc_self.trans (Icc_subset_Icc le_rfl ht.2.2.le))
· rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x.1.le]
apply IntegrableOn.mono_set G'int
exact
Ioc_subset_Icc_self.trans
(Icc_subset_Icc ht.2.1 (h'x.2.trans (min_le_right _ _)))
-- now that we know that `s` contains `[a, b]`, we get the desired result by applying this to `b`.
calc
g b - g a ≤ ∫ y in a..b, (G' y).toReal := main (right_mem_Icc.2 hab)
_ ≤ (∫ y in a..b, φ y) + ε := by
convert hG'.le <;>
· rw [intervalIntegral.integral_of_le hab]
simp only [integral_Icc_eq_integral_Ioc', Real.volume_singleton]
