From d8cde2aaf634884a9a3f8db4873c52b301880aa3 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 21 Aug 2020 10:07:44 +0000 Subject: [PATCH] feat(measure_theory/interval_integral): more versions of FTC-1 (#3709) Left/right derivative, strict derivative, differentiability in both endpoints. Other changes: * rename `filter.tendsto_le_left` and `filter.tendsto_le_right` to `filter.tendsto.mono_left` and `filter.tendsto.mono_right`, swap arguments; * rename `order_top.tendsto_at_top` to `order_top.tendsto_at_top_nhds`; * introduce `tendsto_Ixx_class` instead of `is_interval_generated`. Co-authored-by: sgouezel --- src/analysis/calculus/extend_deriv.lean | 4 +- src/analysis/calculus/fderiv.lean | 4 +- src/analysis/calculus/tangent_cone.lean | 13 +- src/analysis/specific_limits.lean | 2 +- src/measure_theory/borel_space.lean | 16 + src/measure_theory/interval_integral.lean | 971 ++++++++++++++++++++-- src/measure_theory/l1_space.lean | 2 +- src/measure_theory/measurable_space.lean | 6 + src/measure_theory/measure_space.lean | 19 +- src/measure_theory/set_integral.lean | 9 +- src/order/filter/basic.lean | 23 +- src/order/filter/interval.lean | 259 +++--- src/topology/algebra/infinite_sum.lean | 2 +- src/topology/algebra/ordered.lean | 48 +- src/topology/basic.lean | 6 +- src/topology/continuous_on.lean | 18 +- 16 files changed, 1177 insertions(+), 225 deletions(-) diff --git a/src/analysis/calculus/extend_deriv.lean b/src/analysis/calculus/extend_deriv.lean index 437ead513a0d9..f29f87d24d725 100644 --- a/src/analysis/calculus/extend_deriv.lean +++ b/src/analysis/calculus/extend_deriv.lean @@ -125,7 +125,7 @@ begin have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)), { simp [deriv_fderiv.symm], refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _, - exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Ioi_self) f_lim' }, + exact tendsto_nhds_within_mono_left Ioo_subset_Ioi_self f_lim' }, -- now we can apply `has_fderiv_at_boundary_of_differentiable` have : has_deriv_within_at f e (Icc a b) a, { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure], @@ -162,7 +162,7 @@ begin have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)), { simp [deriv_fderiv.symm], refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _, - exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Iio_self) f_lim' }, + exact tendsto_nhds_within_mono_left Ioo_subset_Iio_self f_lim' }, -- now we can apply `has_fderiv_at_boundary_of_differentiable` have : has_deriv_within_at f e (Icc b a) a, { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure], diff --git a/src/analysis/calculus/fderiv.lean b/src/analysis/calculus/fderiv.lean index 91e03a0b3a916..efa7a45e88d15 100644 --- a/src/analysis/calculus/fderiv.lean +++ b/src/analysis/calculus/fderiv.lean @@ -537,7 +537,7 @@ theorem has_fderiv_at_filter.tendsto_nhds tendsto f L (𝓝 (f x)) := begin have : tendsto (λ x', f x' - f x) L (𝓝 0), - { refine h.is_O_sub.trans_tendsto (tendsto_le_left hL _), + { refine h.is_O_sub.trans_tendsto (tendsto.mono_left _ hL), rw ← sub_self x, exact tendsto_id.sub tendsto_const_nhds }, have := tendsto.add this tendsto_const_nhds, rw zero_add (f x) at this, @@ -1053,7 +1053,7 @@ protected lemma has_fderiv_within_at.iterate {f : E → E} {f' : E →L[𝕜] E} begin refine hf.iterate _ hx n, convert tendsto_inf.2 ⟨hf.continuous_within_at, _⟩, - exacts [hx.symm, tendsto_le_left inf_le_right (tendsto_principal_principal.2 hs)] + exacts [hx.symm, (tendsto_principal_principal.2 hs).mono_left inf_le_right] end protected lemma has_strict_fderiv_at.iterate {f : E → E} {f' : E →L[𝕜] E} diff --git a/src/analysis/calculus/tangent_cone.lean b/src/analysis/calculus/tangent_cone.lean index 87a4b9fe75581..ed6e5a6f44f51 100644 --- a/src/analysis/calculus/tangent_cone.lean +++ b/src/analysis/calculus/tangent_cone.lean @@ -117,8 +117,7 @@ begin refine ⟨c, d, _, ctop, clim⟩, suffices : tendsto (λ n, x + d n) at_top (𝓝[t] x), from tendsto_principal.1 (tendsto_inf.1 this).2, - apply tendsto_le_right h, - refine tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩, + refine (tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩).mono_right h, simpa only [add_zero] using tendsto_const_nhds.add (tangent_cone_at.lim_zero at_top ctop clim) end @@ -246,8 +245,14 @@ end end tangent_cone section unique_diff -/- This section is devoted to properties of the predicates `unique_diff_within_at` and -`unique_diff_on`. -/ +/-! +### Properties of `unique_diff_within_at` and `unique_diff_on` + +This section is devoted to properties of the predicates `unique_diff_within_at` and `unique_diff_on`. -/ + +lemma unique_diff_on.unique_diff_within_at {s : set E} {x} (hs : unique_diff_on 𝕜 s) (h : x ∈ s) : + unique_diff_within_at 𝕜 s x := +hs x h lemma unique_diff_within_at_univ : unique_diff_within_at 𝕜 univ x := by { rw [unique_diff_within_at, tangent_cone_univ], simp } diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index c5b047be72298..72b1360fa1665 100644 --- a/src/analysis/specific_limits.lean +++ b/src/analysis/specific_limits.lean @@ -116,7 +116,7 @@ end lemma tendsto_inv_at_top_zero [discrete_linear_ordered_field α] [topological_space α] [order_topology α] : tendsto (λr:α, r⁻¹) at_top (𝓝 0) := -tendsto_le_right inf_le_left tendsto_inv_at_top_zero' +tendsto_inv_at_top_zero'.mono_right inf_le_left lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} : (∃r, tendsto (λn, (∑ i in range n, abs (f i))) at_top (𝓝 r)) → summable f diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean index a713c4ce0b317..add45c76c1d97 100644 --- a/src/measure_theory/borel_space.lean +++ b/src/measure_theory/borel_space.lean @@ -205,6 +205,14 @@ lemma is_measurable_Ici : is_measurable (Ici a) := is_closed_Ici.is_measurable lemma is_measurable_Iic : is_measurable (Iic a) := is_closed_Iic.is_measurable lemma is_measurable_Icc : is_measurable (Icc a b) := is_closed_Icc.is_measurable +instance nhds_within_Ici_is_measurably_generated : + (𝓝[Ici b] a).is_measurably_generated := +is_measurable_Ici.nhds_within_is_measurably_generated _ + +instance nhds_within_Iic_is_measurably_generated : + (𝓝[Iic b] a).is_measurably_generated := +is_measurable_Iic.nhds_within_is_measurably_generated _ + instance at_top_is_measurably_generated : (filter.at_top : filter α).is_measurably_generated := @filter.infi_is_measurably_generated _ _ _ _ $ λ a, (is_measurable_Ici : is_measurable (Ici a)).principal_is_measurably_generated @@ -224,6 +232,14 @@ lemma is_measurable_Ioo : is_measurable (Ioo a b) := is_open_Ioo.is_measurable lemma is_measurable_Ioc : is_measurable (Ioc a b) := is_measurable_Ioi.inter is_measurable_Iic lemma is_measurable_Ico : is_measurable (Ico a b) := is_measurable_Ici.inter is_measurable_Iio +instance nhds_within_Ioi_is_measurably_generated : + (𝓝[Ioi b] a).is_measurably_generated := +is_measurable_Ioi.nhds_within_is_measurably_generated _ + +instance nhds_within_Iio_is_measurably_generated : + (𝓝[Iio b] a).is_measurably_generated := +is_measurable_Iio.nhds_within_is_measurably_generated _ + end order_closed_topology lemma is_measurable_interval [decidable_linear_order α] [order_closed_topology α] {a b : α} : diff --git a/src/measure_theory/interval_integral.lean b/src/measure_theory/interval_integral.lean index 03524f5e9c0be..609eba0408c9d 100644 --- a/src/measure_theory/interval_integral.lean +++ b/src/measure_theory/interval_integral.lean @@ -11,9 +11,66 @@ import analysis.calculus.deriv # Integral over an interval In this file we define `∫ x in a..b, f x ∂μ` to be `∫ x in Ioc a b, f x ∂μ` if `a ≤ b` -and `-∫ x in Ioc b a, f x ∂μ` if `b ≤ a`. We prove a few simple properties and the first part of the -[fundamental theorem of calculus](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus), -see `integral_has_deriv_at_of_tendsto_ae`. +and `-∫ x in Ioc b a, f x ∂μ` if `b ≤ a`. We prove a few simple properties and many versions +of the first part of the +[fundamental theorem of calculus](https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus). +Recall that it states that the function `(u, v) ↦ ∫ x in u..v, f x` has derivative +`(δu, δv) ↦ δv • f b - δu • f a` at `(a, b)` provided that `f` is continuous at `a` and `b`. + +## Main statements + +### FTC-1 for Lebesgue measure + +We prove several versions of FTC-1, all in the `interval_integral` namespace. Many of them follow +the naming scheme `integral_has(_strict?)_(f?)deriv(_within?)_at(_of_tendsto_ae?)(_right|_left?)`. +They formulate FTC in terms of `has(_strict?)_(f?)deriv(_within?)_at`. +Let us explain the meaning of each part of the name: + +* `_strict` means that the theorem is about strict differentiability; +* `f` means that the theorem is about differentiability in both endpoints; incompatible with + `_right|_left`; +* `_within` means that the theorem is about one-sided derivatives, see below for details; +* `_of_tendsto_ae` means that instead of continuity the theorem assumes that `f` has a finite limit + almost surely as `x` tends to `a` and/or `b`; +* `_right` or `_left` mean that the theorem is about differentiability in the right (resp., left) + endpoint. + +We also reformulate these theorems in terms of `(f?)deriv(_within?)`. These theorems are named +`(f?)deriv(_within?)_integral(_of_tendsto_ae?)(_right|_left?)` with the same meaning of parts of the +name. + +### One-sided derivatives + +Theorem `integral_has_fderiv_within_at_of_tendsto_ae` states that `(u, v) ↦ ∫ x in u..v, f x` has a +derivative `(δu, δv) ↦ δv • cb - δu • ca` within the set `s × t` at `(a, b)` provided that `f` tends +to `ca` (resp., `cb`) almost surely at `la` (resp., `lb`), where possible values of `s`, `t`, and +corresponding filters `la`, `lb` are given in the following table. + +| `s` | `la` | `t` | `lb` | +| ------- | ---- | --- | ---- | +| `Iic a` | `𝓝[Iic a] a` | `Iic b` | `𝓝[Iic b] b` | +| `Ici a` | `𝓝[Ioi a] a` | `Ici b` | `𝓝[Ioi b] b` | +| `{a}` | `⊥` | `{b}` | `⊥` | +| `univ` | `𝓝 a` | `univ` | `𝓝 b` | + +We use a typeclass `FTC_filter` to make Lean automatically find `la`/`lb` based on `s`/`t`. This way +we can formulate one theorem instead of `16` (or `8` if we leave only non-trivial ones not covered +by `integral_has_deriv_within_at_of_tendsto_ae_(left|right)` and +`integral_has_fderiv_at_of_tendsto_ae`). Similarly, +`integral_has_deriv_within_at_of_tendsto_ae_right` works for both one-sided derivatives using the +same typeclass to find an appropriate filter. + +### FTC for a locally finite measure + +Before proving FTC for the Lebesgue measure, we prove a few statements that can be seen as FTC for +any measure. The most general of them, +`measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae`, states the following. Let `(la, la')` +be an `FTC_filter` pair of filters around `a` (i.e., `FTC_filter a la la'`) and let `(lb, lb')` be +an `FTC_filter` pair of filters around `b`. If `f` has finite limits `ca` and `cb` almost surely at +`la'` and `lb'`, respectively, then +`∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + + o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥)` as `ua` and `va` tend to `la` while +`ub` and `vb` tend to `lb`. ## Implementation notes @@ -42,7 +99,29 @@ intervals with the same endpoints for two reasons: [cumulative distribution function](https://en.wikipedia.org/wiki/Cumulative_distribution_function) of `μ`. --/ +### `FTC_filter` class + +As explained above, many theorems in this file rely on the typeclass +`FTC_filter (a : α) (l l' : filter α)` to avoid code duplication. This typeclass combines four +assumptions: + +- `pure a ≤ l`; +- `l' ≤ 𝓝 a`; +- `l'` has a basis of measurable sets; +- if `u n` and `v n` tend to `l`, then for any `s ∈ l'`, `Ioc (u n) (v n)` is eventually included + in `s`. + +This typeclass has exactly four “real” instances: `(a, pure a, ⊥)`, `(a, 𝓝[Ici a] a, 𝓝[Ioi a] a)`, +`(a, 𝓝[Iic a] a, 𝓝[Iic a] a)`, `(a, 𝓝 a, 𝓝 a)`, and two instances that are equal to the first and +last “real” instances: `(a, 𝓝[{a}] a, ⊥)` and `(a, 𝓝[univ] a, 𝓝[univ] a)`. While the difference +between `Ici a` and `Ioi a` doesn't matter for theorems about Lebesgue measure, it becomes important +in the versions of FTC about any locally finite measure if this measure has an atom at one of the +endpoints. + +## Tags + +integral, fundamental theorem of calculus + -/ noncomputable theory open topological_space (second_countable_topology) @@ -52,6 +131,10 @@ open_locale classical topological_space filter variables {α β 𝕜 E F : Type*} [decidable_linear_order α] [measurable_space α] [normed_group E] +/-! +### Integrability at an interval +-/ + /-- A function `f` is called *interval integrable* with respect to a measure `μ` on an unordered interval `a..b` if it is integrable on both intervals `(a, b]` and `(b, a]`. One of these intervals is always empty, so this property is equivalent to `f` being integrable on @@ -101,6 +184,46 @@ lemma sub (hfm : measurable f) (hfi : interval_integrable f μ a b) end interval_integrable +/-- Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'` +eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`. + +Suppose that `f : α → E` has a finite limit at `l' ⊓ μ.ae`. Then `f` is interval integrable on +`u..v` provided that both `u` and `v` tend to `l`. + +Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so +`apply tendsto.eventually_interval_integrable_ae` will generate goals `filter α` and +`tendsto_Ixx_class Ioc ?m_1 l'`. -/ +lemma filter.tendsto.eventually_interval_integrable_ae {f : α → E} {μ : measure α} + {l l' : filter α} [tendsto_Ixx_class Ioc l l'] [is_measurably_generated l'] + (hμ : μ.finite_at_filter l') {c : E} (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) + {u v : β → α} {lt : filter β} (hu : tendsto u lt l) (hv : tendsto v lt l) : + ∀ᶠ t in lt, interval_integrable f μ (u t) (v t) := +have _ := (hf.integrable_at_filter_ae hμ).eventually, +((hu.Ioc hv).eventually this).and $ (hv.Ioc hu).eventually this + +/-- Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'` +eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`. + +Suppose that `f : α → E` has a finite limit at `l`. Then `f` is interval integrable on `u..v` +provided that both `u` and `v` tend to `l`. + +Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so +`apply tendsto.eventually_interval_integrable_ae` will generate goals `filter α` and +`tendsto_Ixx_class Ioc ?m_1 l'`. -/ +lemma filter.tendsto.eventually_interval_integrable {f : α → E} {μ : measure α} + {l l' : filter α} [tendsto_Ixx_class Ioc l l'] [is_measurably_generated l'] + (hμ : μ.finite_at_filter l') {c : E} (hf : tendsto f l' (𝓝 c)) + {u v : β → α} {lt : filter β} (hu : tendsto u lt l) (hv : tendsto v lt l) : + ∀ᶠ t in lt, interval_integrable f μ (u t) (v t) := +(hf.mono_left inf_le_left).eventually_interval_integrable_ae hμ hu hv + +/-! +### Interval integral: definition and basic properties + +In this section we define `∫ x in a..b, f x ∂μ` as `∫ x in Ioc a b, f x ∂μ - ∫ x in Ioc b a, f x ∂μ` +and prove some basic properties. +-/ + variables [second_countable_topology E] [complete_space E] [normed_space ℝ E] [measurable_space E] [borel_space E] @@ -115,7 +238,9 @@ notation `∫` binders ` in ` a `..` b `, ` r:(scoped:60 f, interval_integral f namespace interval_integral -variables {a b c : α} {f g : α → E} {μ : measure α} +section + +variables {a b c d : α} {f g : α → E} {μ : measure α} lemma integral_of_le (h : a ≤ b) : ∫ x in a..b, f x ∂μ = ∫ x in Ioc a b, f x ∂μ := by simp [interval_integral, h] @@ -156,12 +281,9 @@ lemma norm_integral_le_of_norm_le_const_ae {a b C : ℝ} {f : ℝ → E} ∥∫ x in a..b, f x∥ ≤ C * abs (b - a) := begin rw [norm_integral_eq_norm_integral_Ioc], - have : volume (Ioc (min a b) (max a b)) = ennreal.of_real (abs (b - a)), - { rw [real.volume_Ioc, max_sub_min_eq_abs, ennreal.of_real] }, - rw [← ennreal.to_real_of_real (abs_nonneg _), ← this], - refine norm_set_integral_le_of_norm_le_const_ae'' _ is_measurable_Ioc h, - simp only [this, ennreal.lt_top_iff_ne_top], - exact ennreal.of_real_ne_top + convert norm_set_integral_le_of_norm_le_const_ae'' _ is_measurable_Ioc h, + { rw [real.volume_Ioc, max_sub_min_eq_abs, ennreal.to_real_of_real (abs_nonneg _)] }, + { simp only [real.volume_Ioc, ennreal.of_real_lt_top] }, end lemma norm_integral_le_of_norm_le_const {a b C : ℝ} {f : ℝ → E} @@ -184,6 +306,29 @@ begin abel end +lemma integral_sub (hfm : measurable f) (hfi : interval_integrable f μ a b) + (hgm : measurable g) (hgi : interval_integrable g μ a b) : + ∫ x in a..b, f x - g x ∂μ = ∫ x in a..b, f x ∂μ - ∫ x in a..b, g x ∂μ := +(integral_add hfm hfi hgm.neg hgi.neg).trans $ congr_arg _ integral_neg + +lemma integral_smul (r : ℝ) : ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ := +by simp only [interval_integral, integral_smul, smul_sub] + +lemma integral_const' (c : E) : + ∫ x in a..b, c ∂μ = ((μ $ Ioc a b).to_real - (μ $ Ioc b a).to_real) • c := +by simp only [interval_integral, set_integral_const, sub_smul] + +lemma integral_const {a b : ℝ} (c : E) : (∫ (x : ℝ) in a..b, c) = (b - a) • c := +by simp only [integral_const', real.volume_Ioc, ennreal.to_real_of_real', ← neg_sub b, + max_zero_sub_eq_self] + +/-! +### Integral is an additive function of the interval + +In this section we prove that `∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ` +as well as a few other identities trivially equivalent to this one. +-/ + variables [topological_space α] [opens_measurable_space α] section order_closed_topology @@ -209,66 +354,782 @@ lemma integral_add_adjacent_intervals (hfm : measurable f) (hab : interval_integ ∫ x in a..b, f x ∂μ + ∫ x in b..c, f x ∂μ = ∫ x in a..c, f x ∂μ := by rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hfm hab hbc] +lemma integral_interval_sub_left (hfm : measurable f) (hab : interval_integrable f μ a b) + (hac : interval_integrable f μ a c) : + ∫ x in a..b, f x ∂μ - ∫ x in a..c, f x ∂μ = ∫ x in c..b, f x ∂μ := +sub_eq_of_eq_add' $ eq.symm $ integral_add_adjacent_intervals hfm hac (hac.symm.trans hab) + +lemma integral_interval_add_interval_comm (hfm : measurable f) (hab : interval_integrable f μ a b) + (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ a c) : + ∫ x in a..b, f x ∂μ + ∫ x in c..d, f x ∂μ = ∫ x in a..d, f x ∂μ + ∫ x in c..b, f x ∂μ := +by rw [← integral_add_adjacent_intervals hfm hac hcd, add_assoc, add_left_comm, + integral_add_adjacent_intervals hfm hac (hac.symm.trans hab), add_comm] + +lemma integral_interval_sub_interval_comm (hfm : measurable f) (hab : interval_integrable f μ a b) + (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ a c) : + ∫ x in a..b, f x ∂μ - ∫ x in c..d, f x ∂μ = ∫ x in a..c, f x ∂μ - ∫ x in b..d, f x ∂μ := +by simp only [sub_eq_add_neg, ← integral_symm, + integral_interval_add_interval_comm hfm hab hcd.symm (hac.trans hcd)] + +lemma integral_interval_sub_interval_comm' (hfm : measurable f) (hab : interval_integrable f μ a b) + (hcd : interval_integrable f μ c d) (hac : interval_integrable f μ a c) : + ∫ x in a..b, f x ∂μ - ∫ x in c..d, f x ∂μ = ∫ x in d..b, f x ∂μ - ∫ x in c..a, f x ∂μ := +by rw [integral_interval_sub_interval_comm hfm hab hcd hac, integral_symm b d, integral_symm a c, + sub_neg_eq_add, sub_eq_neg_add] + +lemma integral_Iic_sub_Iic (hfm : measurable f) (ha : integrable_on f (Iic a) μ) + (hb : integrable_on f (Iic b) μ) : + ∫ x in Iic b, f x ∂μ - ∫ x in Iic a, f x ∂μ = ∫ x in a..b, f x ∂μ := +begin + wlog hab : a ≤ b using [a b] tactic.skip, + { rw [sub_eq_iff_eq_add', integral_of_le hab, ← integral_union (Iic_disjoint_Ioc (le_refl _)), + Iic_union_Ioc_eq_Iic hab], + exacts [is_measurable_Iic, is_measurable_Ioc, hfm, ha, hb.mono_set (λ _, and.right)] }, + { intros ha hb, + rw [integral_symm, ← this hb ha, neg_sub] } +end + +/-- If `μ` is a finite measure then `∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c`. -/ +lemma integral_const_of_cdf [finite_measure μ] (c : E) : + ∫ x in a..b, c ∂μ = ((μ (Iic b)).to_real - (μ (Iic a)).to_real) • c := +begin + simp only [sub_smul, ← set_integral_const], + refine (integral_Iic_sub_Iic measurable_const _ _).symm; + simp only [integrable_on_const, measure_lt_top, or_true] +end + end order_closed_topology -variables [order_topology α] +end + +/-! +### Fundamental theorem of calculus, part 1, for any measure + +In this section we prove a few lemmas that can be seen as versions of FTC-1 for interval integral +w.r.t. any measure. Many theorems are formulated for one or two pairs of filters related by +`FTC_filter a l l'`. This typeclass has exactly four “real” instances: `(a, pure a, ⊥)`, +`(a, 𝓝[Ici a] a, 𝓝[Ioi a] a)`, `(a, 𝓝[Iic a] a, 𝓝[Iic a] a)`, `(a, 𝓝 a, 𝓝 a)`, and two instances +that are equal to the first and last “real” instances: `(a, 𝓝[{a}] a, ⊥)` and +`(a, 𝓝[univ] a, 𝓝[univ] a)`. We use this approach to avoid repeating arguments in many very similar +cases. Lean can automatically find both `a` and `l'` based on `l`. + +The most general theorem `measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae` can be seen +as a generalization of lemma `integral_has_strict_fderiv_at` below which states strict +differentiability of `∫ x in u..v, f x` in `(u, v)` at `(a, b)` for a measurable function `f` that +is integrable on `a..b` and is continuous at `a` and `b`. The lemma is generalized in three +directions: first, `measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae` deals with any +locally finite measure `μ`; second, it works for one-sided limits/derivatives; third, it assumes +only that `f` has finite limits almost surely at `a` and `b`. + +Namely, let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of +`FTC_filter`s around `a`; let `(lb, lb')` be a pair of `FTC_filter`s around `b`. Suppose that `f` +has finite limits `ca` and `cb` at `la' ⊓ μ.ae` and `lb' ⊓ μ.ae`, respectively. Then +`∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + + o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥)` +as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`. + +This theorem is formulated with integral of constants instead of measures in the right hand sides +for two reasons: first, this way we avoid `min`/`max` in the statements; second, often it is +possible to write better `simp` lemmas for these integrals, see `integral_const` and +`integral_const_of_cdf`. + +In the next subsection we apply this theorem to prove various theorems about differentiability +of the integral w.r.t. Lebesgue measure. -/ + +/-- An auxiliary typeclass for the Fundamental theorem of calculus, part 1. It is used to formulate +theorems that work simultaneously for left and right one-sided derivatives of `∫ x in u..v, f x`. +There are four instances: `(a, pure a, ⊥)`, `(a, 𝓝[Ici a], 𝓝[Ioi a])`, +`(a, 𝓝[Iic a], 𝓝[Iic a])`, and `(a, 𝓝 a, 𝓝 a)`. -/ +class FTC_filter {β : Type*} [linear_order β] [measurable_space β] [topological_space β] + (a : out_param β) (outer : filter β) (inner : out_param $ filter β) + extends tendsto_Ixx_class Ioc outer inner : Prop := +(pure_le : pure a ≤ outer) +(le_nhds : inner ≤ 𝓝 a) +[meas_gen : is_measurably_generated inner] + +/- The `dangerous_instance` linter doesn't take `out_param`s into account, so it thinks that +`FTC_filter.to_tendsto_Ixx_class` is dangerous. Disable this linter using `nolint`. +-/ +attribute [nolint dangerous_instance] FTC_filter.to_tendsto_Ixx_class + +namespace FTC_filter + +variables [linear_order β] [measurable_space β] [topological_space β] + +instance pure (a : β) : FTC_filter a (pure a) ⊥ := +{ pure_le := le_refl _, + le_nhds := bot_le } + +instance nhds_within_singleton (a : β) : FTC_filter a (𝓝[{a}] a) ⊥ := +by { rw [nhds_within, principal_singleton, inf_eq_right.2 (pure_le_nhds a)], apply_instance } + +lemma finite_at_inner {a : β} (l : filter β) {l'} [h : FTC_filter a l l'] + {μ : measure β} [locally_finite_measure μ] : + μ.finite_at_filter l' := +(μ.finite_at_nhds a).filter_mono h.le_nhds + +variables [opens_measurable_space β] [order_topology β] + +instance nhds (a : β) : FTC_filter a (𝓝 a) (𝓝 a) := +{ pure_le := pure_le_nhds a, + le_nhds := le_refl _ } + +instance nhds_univ (a : β) : FTC_filter a (𝓝[univ] a) (𝓝 a) := +by { rw nhds_within_univ, apply_instance } + +instance nhds_left (a : β) : FTC_filter a (𝓝[Iic a] a) (𝓝[Iic a] a) := +{ pure_le := pure_le_nhds_within right_mem_Iic, + le_nhds := inf_le_left } + +instance nhds_right (a : β) : FTC_filter a (𝓝[Ici a] a) (𝓝[Ioi a] a) := +{ pure_le := pure_le_nhds_within left_mem_Ici, + le_nhds := inf_le_left } + +end FTC_filter open asymptotics -lemma integral_sub_linear_is_o_of_tendsto_ae [locally_finite_measure μ] {f : α → E} {a : α} {c : E} - (hfm : measurable f) (ha : tendsto f (𝓝 a ⊓ μ.ae) (𝓝 c)) : - is_o (λ b, ∫ x in a..b, f x ∂μ - ((μ (Ioc a b)).to_real - (μ (Ioc b a)).to_real) • c) - (λ b, (μ (Ioc (min a b) (max a b))).to_real) (𝓝 a) := +section + +variables {f : α → E} {a b : α} {c ca cb : E} {l l' la la' lb lb' : filter α} {lt : filter β} + {μ : measure α} {u v ua va ub vb : β → α} + +/-- Fundamental theorem of calculus-1, local version for any measure. +Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. +If `f` has a finite limit `c` at `l' ⊓ μ.ae`, where `μ` is a measure +finite at `l'`, then `∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ)` as both +`u` and `v` tend to `l`. + +See also `measure_integral_sub_linear_is_o_of_tendsto_ae` for a version assuming +`[FTC_filter a l l']` and `[locally_finite_measure μ]`. If `l` is one of `𝓝[Ici a] a`, +`𝓝[Iic a] a`, `𝓝 a`, then it's easier to apply the non-primed version. +The primed version also works, e.g., for `l = l' = at_top`. + +We use integrals of constants instead of measures because this way it is easier to formulate +a statement that works in both cases `u ≤ v` and `v ≤ u`. -/ +lemma measure_integral_sub_linear_is_o_of_tendsto_ae' + [is_measurably_generated l'] [tendsto_Ixx_class Ioc l l'] + (hfm : measurable f) (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') + (hu : tendsto u lt l) (hv : tendsto v lt l) : + is_o (λ t, ∫ x in u t..v t, f x ∂μ - ∫ x in u t..v t, c ∂μ) + (λ t, ∫ x in u t..v t, (1:ℝ) ∂μ) lt := begin - have A : is_o (λ b, ∫ x in Ioc a b, f x ∂μ - (μ $ Ioc a b).to_real • c) - (λ b, (μ $ Ioc a b).to_real) (𝓝 a), - { refine (ha.integral_sub_linear_is_o_ae hfm (μ.finite_at_nhds _)).comp_tendsto _, - exact tendsto_const_nhds.Ioc tendsto_id }, - have B : is_o (λ b, ∫ x in Ioc b a, f x ∂μ - (μ $ Ioc b a).to_real • c) - (λ b, (μ $ Ioc b a).to_real) (𝓝 a), - { refine (ha.integral_sub_linear_is_o_ae hfm (μ.finite_at_nhds _)).comp_tendsto _, - exact tendsto_id.Ioc tendsto_const_nhds }, - change is_o _ _ _, + have A := (hf.integral_sub_linear_is_o_ae hfm hl).comp_tendsto (hu.Ioc hv), + have B := (hf.integral_sub_linear_is_o_ae hfm hl).comp_tendsto (hv.Ioc hu), + simp only [integral_const'], convert (A.trans_le _).sub (B.trans_le _), - { ext b, - simp only [interval_integral, sub_smul], + { ext t, + simp_rw [(∘), interval_integral, sub_smul], abel }, - { intro b, - cases le_total a b with hab hab; simp [hab] }, - { intro b, - cases le_total a b with hab hab; simp [hab] } + all_goals { intro t, cases le_total (u t) (v t) with huv huv; simp [huv] } +end + +/-- Fundamental theorem of calculus-1, local version for any measure. +Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. +If `f` has a finite limit `c` at `l ⊓ μ.ae`, where `μ` is a measure +finite at `l`, then `∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v))` as both +`u` and `v` tend to `l` so that `u ≤ v`. + +See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_le` for a version assuming +`[FTC_filter a l l']` and `[locally_finite_measure μ]`. If `l` is one of `𝓝[Ici a] a`, +`𝓝[Iic a] a`, `𝓝 a`, then it's easier to apply the non-primed version. +The primed version also works, e.g., for `l = l' = at_top`. -/ +lemma measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' + [is_measurably_generated l'] [tendsto_Ixx_class Ioc l l'] + (hfm : measurable f) (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') + (hu : tendsto u lt l) (hv : tendsto v lt l) (huv : u ≤ᶠ[lt] v) : + is_o (λ t, ∫ x in u t..v t, f x ∂μ - (μ (Ioc (u t) (v t))).to_real • c) + (λ t, (μ $ Ioc (u t) (v t)).to_real) lt := +(measure_integral_sub_linear_is_o_of_tendsto_ae' hfm hf hl hu hv).congr' + (huv.mono $ λ x hx, by simp [integral_const', hx]) + (huv.mono $ λ x hx, by simp [integral_const', hx]) + +/-- Fundamental theorem of calculus-1, local version for any measure. +Let filters `l` and `l'` be related by `tendsto_Ixx_class Ioc`. +If `f` has a finite limit `c` at `l ⊓ μ.ae`, where `μ` is a measure +finite at `l`, then `∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u))` as both +`u` and `v` tend to `l` so that `v ≤ u`. + +See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge` for a version assuming +`[FTC_filter a l l']` and `[locally_finite_measure μ]`. If `l` is one of `𝓝[Ici a] a`, +`𝓝[Iic a] a`, `𝓝 a`, then it's easier to apply the non-primed version. +The primed version also works, e.g., for `l = l' = at_top`. -/ +lemma measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge' + [is_measurably_generated l'] [tendsto_Ixx_class Ioc l l'] + (hfm : measurable f) (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) (hl : μ.finite_at_filter l') + (hu : tendsto u lt l) (hv : tendsto v lt l) (huv : v ≤ᶠ[lt] u) : + is_o (λ t, ∫ x in u t..v t, f x ∂μ + (μ (Ioc (v t) (u t))).to_real • c) + (λ t, (μ $ Ioc (v t) (u t)).to_real) lt := +(measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' hfm hf hl hv hu huv).neg_left.congr_left $ + λ t, by simp [integral_symm (u t), add_comm] + +variables [topological_space α] + +section + +variables [locally_finite_measure μ] [FTC_filter a l l'] + +include a + +local attribute [instance] FTC_filter.meas_gen + +/-- Fundamental theorem of calculus-1, local version for any measure. +Let filters `l` and `l'` be related by `[FTC_filter a l l']`; let `μ` be a locally finite measure. +If `f` has a finite limit `c` at `l' ⊓ μ.ae`, then +`∫ x in u..v, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ)` as both `u` and `v` tend to `l`. + +See also `measure_integral_sub_linear_is_o_of_tendsto_ae'` for a version that also works, e.g., for +`l = l' = at_top`. + +We use integrals of constants instead of measures because this way it is easier to formulate +a statement that works in both cases `u ≤ v` and `v ≤ u`. -/ +lemma measure_integral_sub_linear_is_o_of_tendsto_ae (hfm : measurable f) + (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) (hu : tendsto u lt l) (hv : tendsto v lt l) : + is_o (λ t, ∫ x in u t..v t, f x ∂μ - ∫ x in u t..v t, c ∂μ) + (λ t, ∫ x in u t..v t, (1:ℝ) ∂μ) lt := +measure_integral_sub_linear_is_o_of_tendsto_ae' hfm hf (FTC_filter.finite_at_inner l) hu hv + +/-- Fundamental theorem of calculus-1, local version for any measure. +Let filters `l` and `l'` be related by `[FTC_filter a l l']`; let `μ` be a locally finite measure. +If `f` has a finite limit `c` at `l' ⊓ μ.ae`, then +`∫ x in u..v, f x ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v))` as both `u` and `v` tend to `l`. + +See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_le'` for a version that also works, +e.g., for `l = l' = at_top`. -/ +lemma measure_integral_sub_linear_is_o_of_tendsto_ae_of_le + (hfm : measurable f) (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) + (hu : tendsto u lt l) (hv : tendsto v lt l) (huv : u ≤ᶠ[lt] v) : + is_o (λ t, ∫ x in u t..v t, f x ∂μ - (μ (Ioc (u t) (v t))).to_real • c) + (λ t, (μ $ Ioc (u t) (v t)).to_real) lt := +measure_integral_sub_linear_is_o_of_tendsto_ae_of_le' hfm hf (FTC_filter.finite_at_inner l) hu hv huv + +/-- Fundamental theorem of calculus-1, local version for any measure. +Let filters `l` and `l'` be related by `[FTC_filter a l l']`; let `μ` be a locally finite measure. +If `f` has a finite limit `c` at `l' ⊓ μ.ae`, then +`∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u))` as both `u` and `v` tend to `l`. + +See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge'` for a version that also works, +e.g., for `l = l' = at_top`. -/ +lemma measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge + (hfm : measurable f) (hf : tendsto f (l' ⊓ μ.ae) (𝓝 c)) + (hu : tendsto u lt l) (hv : tendsto v lt l) (huv : v ≤ᶠ[lt] u) : + is_o (λ t, ∫ x in u t..v t, f x ∂μ + (μ (Ioc (v t) (u t))).to_real • c) + (λ t, (μ $ Ioc (v t) (u t)).to_real) lt := +measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge' hfm hf (FTC_filter.finite_at_inner l) hu hv huv + end -lemma integral_same_has_deriv_at_of_tendsto_ae {f : ℝ → E} {a : ℝ} {c : E} (hfm : measurable f) - (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : - has_deriv_at (λ b, ∫ x in a..b, f x) c a := +variables [order_topology α] [borel_space α] + +local attribute [instance] FTC_filter.meas_gen + +variables [FTC_filter a la la'] [FTC_filter b lb lb'] [locally_finite_measure μ] + +/-- Fundamental theorem of calculus-1, strict derivative in both limits for a locally finite +measure. + +Let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of `FTC_filter`s +around `a`; let `(lb, lb')` be a pair of `FTC_filter`s around `b`. Suppose that `f` has finite +limits `ca` and `cb` at `la' ⊓ μ.ae` and `lb' ⊓ μ.ae`, respectively. +Then `∫ x in va..vb, f x ∂μ - ∫ x in ua..ub, f x ∂μ = + ∫ x in ub..vb, cb ∂μ - ∫ x in ua..va, ca ∂μ + + o(∥∫ x in ua..va, (1:ℝ) ∂μ∥ + ∥∫ x in ub..vb, (1:ℝ) ∂μ∥)` +as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`. +-/ +lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae + (hfm : measurable f) (hab : interval_integrable f μ a b) + (ha_lim : tendsto f (la' ⊓ μ.ae) (𝓝 ca)) (hb_lim : tendsto f (lb' ⊓ μ.ae) (𝓝 cb)) + (hua : tendsto ua lt la) (hva : tendsto va lt la) + (hub : tendsto ub lt lb) (hvb : tendsto vb lt lb) : + is_o (λ t, (∫ x in va t..vb t, f x ∂μ) - (∫ x in ua t..ub t, f x ∂μ) - + (∫ x in ub t..vb t, cb ∂μ - ∫ x in ua t..va t, ca ∂μ)) + (λ t, ∥∫ x in ua t..va t, (1:ℝ) ∂μ∥ + ∥∫ x in ub t..vb t, (1:ℝ) ∂μ∥) lt := begin - change is_o _ _ _, - rw [← is_o_norm_right], - convert integral_sub_linear_is_o_of_tendsto_ae hfm ha, - { ext b, - dsimp, - simp only [integral_same, sub_zero, real.volume_Ioc, ennreal.to_real_of_real'], - congr' 2, - rw [← neg_sub b, max_zero_sub_eq_self] }, - { ext b, - rw [real.volume_Ioc, ennreal.to_real_of_real, max_sub_min_eq_abs, real.norm_eq_abs], - exact sub_nonneg.2 min_le_max } + refine + ((measure_integral_sub_linear_is_o_of_tendsto_ae hfm ha_lim hua hva).neg_left.add_add + (measure_integral_sub_linear_is_o_of_tendsto_ae hfm hb_lim hub hvb)).congr' + _ (eventually_eq.refl _ _), + have A : ∀ᶠ t in lt, interval_integrable f μ (ua t) (va t) := + ha_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner la) hua hva, + have A' : ∀ᶠ t in lt, interval_integrable f μ a (ua t) := + ha_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner la) + (tendsto_const_pure.mono_right FTC_filter.pure_le) hua, + have B : ∀ᶠ t in lt, interval_integrable f μ (ub t) (vb t) := + hb_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner lb) hub hvb, + have B' : ∀ᶠ t in lt, interval_integrable f μ b (ub t) := + hb_lim.eventually_interval_integrable_ae (FTC_filter.finite_at_inner lb) + (tendsto_const_pure.mono_right FTC_filter.pure_le) hub, + filter_upwards [A, A', B, B'], simp only [mem_set_of_eq], + intros t ua_va a_ua ub_vb b_ub, + rw [← integral_interval_sub_interval_comm' hfm], + { dsimp only [], abel }, + exacts [ub_vb, ua_va, b_ub.symm.trans $ hab.symm.trans a_ua] +end + +/-- Fundamental theorem of calculus-1, strict derivative in right endpoint for a locally finite +measure. + +Let `f` be a measurable function integrable on `a..b`. Let `(lb, lb')` be a pair of `FTC_filter`s +around `b`. Suppose that `f` has a finite limit `c` at `lb' ⊓ μ.ae`. + +Then `∫ x in a..v, f x ∂μ - ∫ x in a..u, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)` +as `u` and `v` tend to `lb`. +-/ +lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right + (hfm : measurable f) (hab : interval_integrable f μ a b) + (hf : tendsto f (lb' ⊓ μ.ae) (𝓝 c)) (hu : tendsto u lt lb) (hv : tendsto v lt lb) : + is_o (λ t, ∫ x in a..v t, f x ∂μ - ∫ x in a..u t, f x ∂μ - ∫ x in u t..v t, c ∂μ) + (λ t, ∫ x in u t..v t, (1:ℝ) ∂μ) lt := +by simpa using measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae + hfm hab ((tendsto_bot : tendsto _ ⊥ (𝓝 0)).mono_left inf_le_left) + hf (tendsto_const_pure : tendsto _ _ (pure a)) tendsto_const_pure hu hv + +/-- Fundamental theorem of calculus-1, strict derivative in left endpoint for a locally finite +measure. + +Let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of `FTC_filter`s +around `a`. Suppose that `f` has a finite limit `c` at `la' ⊓ μ.ae`. + +Then `∫ x in v..b, f x ∂μ - ∫ x in u..b, f x ∂μ = -∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)` +as `u` and `v` tend to `la`. +-/ +lemma measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left + (hfm : measurable f) (hab : interval_integrable f μ a b) + (hf : tendsto f (la' ⊓ μ.ae) (𝓝 c)) (hu : tendsto u lt la) (hv : tendsto v lt la) : + is_o (λ t, ∫ x in v t..b, f x ∂μ - ∫ x in u t..b, f x ∂μ + ∫ x in u t..v t, c ∂μ) + (λ t, ∫ x in u t..v t, (1:ℝ) ∂μ) lt := +by simpa using measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae + hfm hab hf ((tendsto_bot : tendsto _ ⊥ (𝓝 0)).mono_left inf_le_left) + hu hv (tendsto_const_pure : tendsto _ _ (pure b)) tendsto_const_pure + end -lemma integral_has_deriv_at_of_tendsto_ae {f : ℝ → E} {a b : ℝ} {c : E} (hfm : measurable f) +/-! +### Fundamental theorem of calculus-1 for Lebesgue measure + +In this section we restate theorems from the previous section for Lebesgue measure. +In particular, we prove that `∫ x in u..v, f x` is strictly differentiable in `(u, v)` +at `(a, b)` provided that `f` is integrable on `a..b` and is continuous at `a` and `b`. +-/ + +variables {f : ℝ → E} {c ca cb : E} {l l' la la' lb lb' : filter ℝ} {lt : filter β} + {a b z : ℝ} {u v ua ub va vb : β → ℝ} [FTC_filter a la la'] [FTC_filter b lb lb'] + +/-! +#### Auxiliary `is_o` statements + +In this section we prove several lemmas that can be interpreted as strict differentiability of +`(u, v) ↦ ∫ x in u..v, f x ∂μ` in `u` and/or `v` at a filter. The statements use `is_o` because +we have no definition of `has_strict_(f)deriv_at_filter` in the library. +-/ + +/-- Fundamental theorem of calculus-1, local version. If `f` has a finite limit `c` almost surely at +`l'`, where `(l, l')` is an `FTC_filter` pair around `a`, then +`∫ x in u..v, f x ∂μ = (v - u) • c + o (v - u)` as both `u` and `v` tend to `l`. -/ +lemma integral_sub_linear_is_o_of_tendsto_ae [FTC_filter a l l'] + (hfm : measurable f) (hf : tendsto f (l' ⊓ volume.ae) (𝓝 c)) + {u v : β → ℝ} (hu : tendsto u lt l) (hv : tendsto v lt l) : + is_o (λ t, (∫ x in u t..v t, f x) - (v t - u t) • c) (v - u) lt := +by simpa [integral_const] using measure_integral_sub_linear_is_o_of_tendsto_ae hfm hf hu hv + +/-- Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints. +If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `FTC_filter` pair around +`a`, and `(lb, lb')` is an `FTC_filter` pair around `b`, and `f` has finite limits `ca` and `cb` +almost surely at `la'` and `lb'`, respectively, then +`(∫ x in va..vb, f x) - ∫ x in ua..ub, f x = (vb - ub) • cb - (va - ua) • ca + + o(∥va - ua∥ + ∥vb - ub∥)` as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`. + +This lemma could've been formulated using `has_strict_fderiv_at_filter` if we had this +definition. -/ +lemma integral_sub_integral_sub_linear_is_o_of_tendsto_ae + (hfm : measurable f) (hab : interval_integrable f volume a b) + (ha_lim : tendsto f (la' ⊓ volume.ae) (𝓝 ca)) (hb_lim : tendsto f (lb' ⊓ volume.ae) (𝓝 cb)) + (hua : tendsto ua lt la) (hva : tendsto va lt la) + (hub : tendsto ub lt lb) (hvb : tendsto vb lt lb) : + is_o (λ t, (∫ x in va t..vb t, f x) - (∫ x in ua t..ub t, f x) - + ((vb t - ub t) • cb - (va t - ua t) • ca)) (λ t, ∥va t - ua t∥ + ∥vb t - ub t∥) lt := +by simpa [integral_const] using +measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae hfm hab ha_lim hb_lim hua hva hub hvb + +/-- Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints. +If `f` is a measurable function integrable on `a..b`, `(lb, lb')` is an `FTC_filter` pair +around `b`, and `f` has a finite limit `c` almost surely at `lb'`, then +`(∫ x in a..v, f x) - ∫ x in a..u, f x = (v - u) • c + o(∥v - u∥)` as `u` and `v` tend to `lb`. + +This lemma could've been formulated using `has_strict_deriv_at_filter` if we had this definition. -/ +lemma integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right + (hfm : measurable f) (hab : interval_integrable f volume a b) + (hf : tendsto f (lb' ⊓ volume.ae) (𝓝 c)) + (hu : tendsto u lt lb) (hv : tendsto v lt lb) : + is_o (λ t, (∫ x in a..v t, f x) - (∫ x in a..u t, f x) - (v t - u t) • c) (v - u) lt := +by simpa only [integral_const, smul_eq_mul, mul_one] using + measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hfm hab hf hu hv + +/-- Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints. +If `f` is a measurable function integrable on `a..b`, `(la, la')` is an `FTC_filter` pair +around `a`, and `f` has a finite limit `c` almost surely at `la'`, then +`(∫ x in v..b, f x) - ∫ x in u..b, f x = -(v - u) • c + o(∥v - u∥)` as `u` and `v` tend to `la`. + +This lemma could've been formulated using `has_strict_deriv_at_filter` if we had this definition. -/ +lemma integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left + (hfm : measurable f) (hab : interval_integrable f volume a b) + (hf : tendsto f (la' ⊓ volume.ae) (𝓝 c)) + (hu : tendsto u lt la) (hv : tendsto v lt la) : + is_o (λ t, (∫ x in v t..b, f x) - (∫ x in u t..b, f x) + (v t - u t) • c) (v - u) lt := +by simpa only [integral_const, smul_eq_mul, mul_one] using + measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae_left hfm hab hf hu hv + +open continuous_linear_map (fst snd smul_right sub_apply smul_right_apply coe_fst' coe_snd' map_sub) + +/-! +#### Strict differentiability + +In this section we prove that for a measurable function `f` integrable on `a..b`, + +* `integral_has_strict_fderiv_at_of_tendsto_ae`: the function `(u, v) ↦ ∫ x in u..v, f x` has + derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` in the sense of strict differentiability + provided that `f` tends to `ca` and `cb` almost surely as `x` tendsto to `a` and `b`, + respectively; + +* `integral_has_strict_fderiv_at`: the function `(u, v) ↦ ∫ x in u..v, f x` has + derivative `(u, v) ↦ v • f b - u • f a` at `(a, b)` in the sense of strict differentiability + provided that `f` is continuous at `a` and `b`; + +* `integral_has_strict_deriv_at_of_tendsto_ae_right`: the function `u ↦ ∫ x in a..u, f x` has + derivative `c` at `b` in the sense of strict differentiability provided that `f` tends to `c` + almost surely as `x` tends to `b`; + +* `integral_has_strict_deriv_at_right`: the function `u ↦ ∫ x in a..u, f x` has derivative `f b` at + `b` in the sense of strict differentiability provided that `f` is continuous at `b`; + +* `integral_has_strict_deriv_at_of_tendsto_ae_left`: the function `u ↦ ∫ x in u..b, f x` has + derivative `-c` at `a` in the sense of strict differentiability provided that `f` tends to `c` + almost surely as `x` tends to `a`; + +* `integral_has_strict_deriv_at_left`: the function `u ↦ ∫ x in u..b, f x` has derivative `-f a` at + `a` in the sense of strict differentiability provided that `f` is continuous at `a`. +-/ + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite +limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then +`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` +in the sense of strict differentiability. -/ +lemma integral_has_strict_fderiv_at_of_tendsto_ae (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca)) + (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) : + has_strict_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) + ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) (a, b) := +begin + have := integral_sub_integral_sub_linear_is_o_of_tendsto_ae hfm hfi ha hb + ((continuous_fst.comp continuous_snd).tendsto ((a, b), (a, b))) + ((continuous_fst.comp continuous_fst).tendsto ((a, b), (a, b))) + ((continuous_snd.comp continuous_snd).tendsto ((a, b), (a, b))) + ((continuous_snd.comp continuous_fst).tendsto ((a, b), (a, b))), + refine (this.congr_left _).trans_is_O _, + { intro x, simp [sub_smul] }, + { exact is_O_fst_prod.norm_left.add is_O_snd_prod.norm_left } +end + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` +at `(a, b)` in the sense of strict differentiability. -/ +lemma integral_has_strict_fderiv_at (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : continuous_at f a) (hb : continuous_at f b) : + has_strict_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) + ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (a, b) := +integral_has_strict_fderiv_at_of_tendsto_ae hfm hfi + (ha.mono_left inf_le_left) (hb.mono_left inf_le_left) + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b` in the sense +of strict differentiability. -/ +lemma integral_has_strict_deriv_at_of_tendsto_ae_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) : + has_strict_deriv_at (λ u, ∫ x in a..u, f x) c b := +integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hfm hfi hb continuous_at_snd + continuous_at_fst + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense of strict +differentiability. -/ +lemma integral_has_strict_deriv_at_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) (hb : continuous_at f b) : + has_strict_deriv_at (λ u, ∫ x in a..u, f x) (f b) b := +integral_has_strict_deriv_at_of_tendsto_ae_right hfm hfi (hb.mono_left inf_le_left) + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense +of strict differentiability. -/ +lemma integral_has_strict_deriv_at_of_tendsto_ae_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : + has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-c) a := +by simpa only [← integral_symm] + using (integral_has_strict_deriv_at_of_tendsto_ae_right hfm hfi.symm ha).neg + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-f a` at `a` in the sense of strict +differentiability. -/ +lemma integral_has_strict_deriv_at_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : continuous_at f a) : + has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-f a) a := +by simpa only [← integral_symm] using (integral_has_strict_deriv_at_right hfm hfi.symm ha).neg + +/-! +#### Fréchet differentiability + +In this subsection we restate results from the previous subsection in terms of `has_fderiv_at`, +`has_deriv_at`, `fderiv`, and `deriv`. +-/ + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite +limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then +`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`. -/ +lemma integral_has_fderiv_at_of_tendsto_ae (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca)) + (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) : + has_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) + ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) (a, b) := +(integral_has_strict_fderiv_at_of_tendsto_ae hfm hfi ha hb).has_fderiv_at + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `a` and `b`, then `(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` +at `(a, b)`. -/ +lemma integral_has_fderiv_at (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : continuous_at f a) (hb : continuous_at f b) : + has_fderiv_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) + ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (a, b) := +(integral_has_strict_fderiv_at hfm hfi ha hb).has_fderiv_at + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has finite +limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then `fderiv` +derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)` equals `(u, v) ↦ v • cb - u • ca`. -/ +lemma fderiv_integral_of_tendsto_ae (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 ca)) + (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 cb)) : + fderiv ℝ (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) (a, b) = + (snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca := +(integral_has_fderiv_at_of_tendsto_ae hfm hfi ha hb).fderiv + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `a` and `b`, then `fderiv` derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)` equals `(u, v) ↦ +v • cb - u • ca`. -/ +lemma fderiv_integral (hfm : measurable f) (hfi : interval_integrable f volume a b) + (ha : continuous_at f a) (hb : continuous_at f b) : + fderiv ℝ (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) (a, b) = + (snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a) := +(integral_has_fderiv_at hfm hfi ha hb).fderiv + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b`. -/ +lemma integral_has_deriv_at_of_tendsto_ae_right (hfm : measurable f) (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) : has_deriv_at (λ u, ∫ x in a..u, f x) c b := +(integral_has_strict_deriv_at_of_tendsto_ae_right hfm hfi hb).has_deriv_at + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b`. -/ +lemma integral_has_deriv_at_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) (hb : continuous_at f b) : + has_deriv_at (λ u, ∫ x in a..u, f x) (f b) b := +(integral_has_strict_deriv_at_right hfm hfi hb).has_deriv_at + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite +limit `c` almost surely at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`. -/ +lemma deriv_integral_of_tendsto_ae_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 b ⊓ volume.ae) (𝓝 c)) : + deriv (λ u, ∫ x in a..u, f x) b = c := +(integral_has_deriv_at_of_tendsto_ae_right hfm hfi hb).deriv + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `f b`. -/ +lemma deriv_integral_right (hfm : measurable f) (hfi : interval_integrable f volume a b) + (hb : continuous_at f b) : + deriv (λ u, ∫ x in a..u, f x) b = f b := +(integral_has_deriv_at_right hfm hfi hb).deriv + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a`. -/ +lemma integral_has_deriv_at_of_tendsto_ae_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : + has_deriv_at (λ u, ∫ x in u..b, f x) (-c) a := +(integral_has_strict_deriv_at_of_tendsto_ae_left hfm hfi ha).has_deriv_at + +/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-f a` at `a`. -/ +lemma integral_has_deriv_at_left (hfm : measurable f) (hfi : interval_integrable f volume a b) + (ha : continuous_at f a) : + has_deriv_at (λ u, ∫ x in u..b, f x) (-f a) a := +(integral_has_strict_deriv_at_left hfm hfi ha).has_deriv_at + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite +limit `c` almost surely at `a`, then the derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-c`. -/ +lemma deriv_integral_of_tendsto_ae_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) (hb : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : + deriv (λ u, ∫ x in u..b, f x) a = -c := +(integral_has_deriv_at_of_tendsto_ae_left hfm hfi hb).deriv + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous +at `a`, then the derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-f a`. -/ +lemma deriv_integral_left (hfm : measurable f) (hfi : interval_integrable f volume a b) + (hb : continuous_at f a) : + deriv (λ u, ∫ x in u..b, f x) a = -f a := +(integral_has_deriv_at_left hfm hfi hb).deriv + +/-! +#### One-sided derivatives +-/ + +/-- Let `f` be a measurable function integrable on `a..b`. The function `(u, v) ↦ ∫ x in u..v, f x` +has derivative `(u, v) ↦ v • cb - u • ca` within `s × t` at `(a, b)`, where +`s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}` provided that `f` tends to `ca` +and `cb` almost surely at the filters `la` and `lb` from the following table. + +| `s` | `la` | `t` | `lb` | +| ------- | ---- | --- | ---- | +| `Iic a` | `𝓝[Iic a] a` | `Iic b` | `𝓝[Iic b] b` | +| `Ici a` | `𝓝[Ioi a] a` | `Ici b` | `𝓝[Ioi b] b` | +| `{a}` | `⊥` | `{b}` | `⊥` | +| `univ` | `𝓝 a` | `univ` | `𝓝 b` | +-/ +lemma integral_has_fderiv_within_at_of_tendsto_ae (hfm : measurable f) + (hfi : interval_integrable f volume a b) + {s t : set ℝ} [FTC_filter a (𝓝[s] a) la] [FTC_filter b (𝓝[t] b) lb] + (ha : tendsto f (la ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (lb ⊓ volume.ae) (𝓝 cb)) : + has_fderiv_within_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) + ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) (s.prod t) (a, b) := begin - refine ((integral_same_has_deriv_at_of_tendsto_ae hfm hb).const_add - (∫ x in a..b, f x)).congr_of_eventually_eq _, - suffices : ∀ᶠ u in 𝓝 b, interval_integrable f volume b u, - { refine this.mono (λ u hu, (integral_add_adjacent_intervals hfm hfi hu).symm) }, - simp only [interval_integrable, eventually_and], - exact ⟨(tendsto_const_nhds.Ioc tendsto_id).eventually - (hb.integrable_at_filter_ae (volume.finite_at_nhds _).inf_of_left).eventually, - (tendsto_id.Ioc tendsto_const_nhds).eventually - (hb.integrable_at_filter_ae (volume.finite_at_nhds _).inf_of_left).eventually⟩, + rw [has_fderiv_within_at, nhds_within_prod_eq], + have := integral_sub_integral_sub_linear_is_o_of_tendsto_ae hfm hfi ha hb + (tendsto_const_pure.mono_right FTC_filter.pure_le : tendsto _ _ (𝓝[s] a)) tendsto_fst + (tendsto_const_pure.mono_right FTC_filter.pure_le : tendsto _ _ (𝓝[t] b)) tendsto_snd, + refine (this.congr_left _).trans_is_O _, + { intro x, simp [sub_smul] }, + { exact is_O_fst_prod.norm_left.add is_O_snd_prod.norm_left } end +/-- Let `f` be a measurable function integrable on `a..b`. The function `(u, v) ↦ ∫ x in u..v, f x` +has derivative `(u, v) ↦ v • f b - u • f a` within `s × t` at `(a, b)`, where +`s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}` provided that `f` tends to +`f a` and `f b` at the filters `la` and `lb` from the following table. In most cases this assumption +is definitionally equal `continuous_at f _` or `continuous_within_at f _ _`. + +| `s` | `la` | `t` | `lb` | +| ------- | ---- | --- | ---- | +| `Iic a` | `𝓝[Iic a] a` | `Iic b` | `𝓝[Iic b] b` | +| `Ici a` | `𝓝[Ioi a] a` | `Ici b` | `𝓝[Ioi b] b` | +| `{a}` | `⊥` | `{b}` | `⊥` | +| `univ` | `𝓝 a` | `univ` | `𝓝 b` | +-/ +lemma integral_has_fderiv_within_at (hfm : measurable f) (hfi : interval_integrable f volume a b) + {s t : set ℝ} [FTC_filter a (𝓝[s] a) la] [FTC_filter b (𝓝[t] b) lb] + (ha : tendsto f la (𝓝 $ f a)) (hb : tendsto f lb (𝓝 $ f b)) : + has_fderiv_within_at (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) + ((snd ℝ ℝ ℝ).smul_right (f b) - (fst ℝ ℝ ℝ).smul_right (f a)) (s.prod t) (a, b) := +integral_has_fderiv_within_at_of_tendsto_ae hfm hfi (ha.mono_left inf_le_left) + (hb.mono_left inf_le_left) + +/-- An auxiliary tactic closing goals `unique_diff_within_at ℝ s a` where +`s ∈ {Iic a, Ici a, univ}`. -/ +meta def unique_diff_within_at_Ici_Iic_univ : tactic unit := +`[apply_rules [unique_diff_on.unique_diff_within_at, unique_diff_on_Ici, unique_diff_on_Iic, + left_mem_Ici, right_mem_Iic, unique_diff_within_at_univ]] + +/-- Let `f` be a measurable function integrable on `a..b`. Choose `s ∈ {Iic a, Ici a, univ}` +and `t ∈ {Iic b, Ici b, univ}`. Suppose that `f` tends to `ca` and `cb` almost surely at the filters +`la` and `lb` from the table below. Then `fderiv_within ℝ (λ p, ∫ x in p.1..p.2, f x) (s.prod t)` +is equal to `(u, v) ↦ u • cb - v • ca`. + +| `s` | `la` | `t` | `lb` | +| ------- | ---- | --- | ---- | +| `Iic a` | `𝓝[Iic a] a` | `Iic b` | `𝓝[Iic b] b` | +| `Ici a` | `𝓝[Ioi a] a` | `Ici b` | `𝓝[Ioi b] b` | +| `univ` | `𝓝 a` | `univ` | `𝓝 b` | + +-/ +lemma fderiv_within_integral_of_tendsto_ae (hfm : measurable f) + (hfi : interval_integrable f volume a b) + {s t : set ℝ} [FTC_filter a (𝓝[s] a) la] [FTC_filter b (𝓝[t] b) lb] + (ha : tendsto f (la ⊓ volume.ae) (𝓝 ca)) (hb : tendsto f (lb ⊓ volume.ae) (𝓝 cb)) + (hs : unique_diff_within_at ℝ s a . unique_diff_within_at_Ici_Iic_univ) + (ht : unique_diff_within_at ℝ t b . unique_diff_within_at_Ici_Iic_univ) : + fderiv_within ℝ (λ p : ℝ × ℝ, ∫ x in p.1..p.2, f x) (s.prod t) (a, b) = + ((snd ℝ ℝ ℝ).smul_right cb - (fst ℝ ℝ ℝ).smul_right ca) := +(integral_has_fderiv_within_at_of_tendsto_ae hfm hfi ha hb).fderiv_within $ hs.prod ht + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely as `x` tends to `b` from the right or from the left, +then `u ↦ ∫ x in a..u, f x` has right (resp., left) derivative `c` at `b`. -/ +lemma integral_has_deriv_within_at_of_tendsto_ae_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] + (hb : tendsto f (𝓝[t] b ⊓ volume.ae) (𝓝 c)) : + has_deriv_within_at (λ u, ∫ x in a..u, f x) c s b := +integral_sub_integral_sub_linear_is_o_of_tendsto_ae_right hfm hfi hb + (tendsto_const_pure.mono_right FTC_filter.pure_le) tendsto_id + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous +from the left or from the right at `b`, then `u ↦ ∫ x in a..u, f x` has left (resp., right) +derivative `f b` at `b`. -/ +lemma integral_has_deriv_within_at_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] + (hb : continuous_within_at f t b) : + has_deriv_within_at (λ u, ∫ x in a..u, f x) (f b) s b := +integral_has_deriv_within_at_of_tendsto_ae_right hfm hfi (hb.mono_left inf_le_left) + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely as `x` tends to `b` from the right or from the left, then the right +(resp., left) derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`. -/ +lemma deriv_within_integral_of_tendsto_ae_right (hfm : measurable f) + (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] + (hb : tendsto f (𝓝[t] b ⊓ volume.ae) (𝓝 c)) + (hs : unique_diff_within_at ℝ s b . unique_diff_within_at_Ici_Iic_univ) : + deriv_within (λ u, ∫ x in a..u, f x) s b = c := +(integral_has_deriv_within_at_of_tendsto_ae_right hfm hfi hb).deriv_within hs + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous +on the right or on the left at `b`, then the right (resp., left) derivative of +`u ↦ ∫ x in a..u, f x` at `b` equals `f b`. -/ +lemma deriv_within_integral_right (hfm : measurable f) (hfi : interval_integrable f volume a b) + {s t : set ℝ} [FTC_filter b (𝓝[s] b) (𝓝[t] b)] (hb : continuous_within_at f t b) + (hs : unique_diff_within_at ℝ s b . unique_diff_within_at_Ici_Iic_univ) : + deriv_within (λ u, ∫ x in a..u, f x) s b = f b := +(integral_has_deriv_within_at_right hfm hfi hb).deriv_within hs + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely as `x` tends to `a` from the right or from the left, +then `u ↦ ∫ x in u..b, f x` has right (resp., left) derivative `-c` at `a`. -/ +lemma integral_has_deriv_within_at_of_tendsto_ae_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] + (ha : tendsto f (𝓝[t] a ⊓ volume.ae) (𝓝 c)) : + has_deriv_within_at (λ u, ∫ x in u..b, f x) (-c) s a := +by { simp only [integral_symm b], + exact (integral_has_deriv_within_at_of_tendsto_ae_right hfm hfi.symm ha).neg } + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous +from the left or from the right at `a`, then `u ↦ ∫ x in u..b, f x` has left (resp., right) +derivative `-f a` at `a`. -/ +lemma integral_has_deriv_within_at_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] + (ha : continuous_within_at f t a) : + has_deriv_within_at (λ u, ∫ x in u..b, f x) (-f a) s a := +integral_has_deriv_within_at_of_tendsto_ae_left hfm hfi (ha.mono_left inf_le_left) + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite +limit `c` almost surely as `x` tends to `a` from the right or from the left, then the right +(resp., left) derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-c`. -/ +lemma deriv_within_integral_of_tendsto_ae_left (hfm : measurable f) + (hfi : interval_integrable f volume a b) {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] + (ha : tendsto f (𝓝[t] a ⊓ volume.ae) (𝓝 c)) + (hs : unique_diff_within_at ℝ s a . unique_diff_within_at_Ici_Iic_univ) : + deriv_within (λ u, ∫ x in u..b, f x) s a = -c := +(integral_has_deriv_within_at_of_tendsto_ae_left hfm hfi ha).deriv_within hs + +/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous +on the right or on the left at `a`, then the right (resp., left) derivative of +`u ↦ ∫ x in u..b, f x` at `a` equals `-f a`. -/ +lemma deriv_within_integral_left (hfm : measurable f) (hfi : interval_integrable f volume a b) + {s t : set ℝ} [FTC_filter a (𝓝[s] a) (𝓝[t] a)] (ha : continuous_within_at f t a) + (hs : unique_diff_within_at ℝ s a . unique_diff_within_at_Ici_Iic_univ) : + deriv_within (λ u, ∫ x in u..b, f x) s a = -f a := +(integral_has_deriv_within_at_left hfm hfi ha).deriv_within hs + end interval_integral diff --git a/src/measure_theory/l1_space.lean b/src/measure_theory/l1_space.lean index a314eb3ed1000..1c62d601da820 100644 --- a/src/measure_theory/l1_space.lean +++ b/src/measure_theory/l1_space.lean @@ -121,7 +121,7 @@ begin end lemma integrable_const [finite_measure μ] (c : β) : integrable (λ x : α, c) μ := -integrable_const_iff.2 (or.inr meas_univ_lt_top) +integrable_const_iff.2 (or.inr $ measure_lt_top _ _) lemma integrable_of_bounded [finite_measure μ] {f : α → β} {C : ℝ} (hC : ∀ᵐ a ∂μ, ∥f a∥ ≤ C) : integrable f μ := diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean index 411915f404a02..8408b19876c90 100644 --- a/src/measure_theory/measurable_space.lean +++ b/src/measure_theory/measurable_space.lean @@ -1093,6 +1093,12 @@ variables [measurable_space α] class is_measurably_generated (f : filter α) : Prop := (exists_measurable_subset : ∀ ⦃s⦄, s ∈ f → ∃ t ∈ f, is_measurable t ∧ t ⊆ s) +instance is_measurably_generated_bot : is_measurably_generated (⊥ : filter α) := +⟨λ _ _, ⟨∅, mem_bot_sets, is_measurable.empty, empty_subset _⟩⟩ + +instance is_measurably_generated_top : is_measurably_generated (⊤ : filter α) := +⟨λ s hs, ⟨univ, univ_mem_sets, is_measurable.univ, λ x _, hs x⟩⟩ + lemma eventually.exists_measurable_mem {f : filter α} [is_measurably_generated f] {p : α → Prop} (h : ∀ᶠ x in f, p x) : ∃ s ∈ f, is_measurable s ∧ ∀ x ∈ s, p x := diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean index 10fc30eaf7d1a..d4404ff580584 100644 --- a/src/measure_theory/measure_space.lean +++ b/src/measure_theory/measure_space.lean @@ -1034,17 +1034,23 @@ lemma restrict_congr {s t : set α} (H : s =ᵐ[μ] t) : μ.restrict s = μ.rest le_antisymm (restrict_mono_ae H.le) (restrict_mono_ae H.symm.le) /-- A measure `μ` is called a probability measure if `μ univ = 1`. -/ -class probability_measure (μ : measure α) : Prop := (meas_univ : μ univ = 1) +class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = 1) /-- A measure `μ` is called finite if `μ univ < ⊤`. -/ -class finite_measure (μ : measure α) : Prop := (meas_univ_lt_top : μ univ < ⊤) +class finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ⊤) -export finite_measure (meas_univ_lt_top) probability_measure (meas_univ) +export probability_measure (measure_univ) + +lemma measure_lt_top (μ : measure α) [finite_measure μ] (s : set α) : μ s < ⊤ := +(measure_mono (subset_univ s)).trans_lt finite_measure.measure_univ_lt_top + +lemma measure_ne_top (μ : measure α) [finite_measure μ] (s : set α) : μ s ≠ ⊤ := +ne_of_lt (measure_lt_top μ s) @[priority 100] instance probability_measure.to_finite_measure (μ : measure α) [probability_measure μ] : finite_measure μ := -⟨by simp only [meas_univ, ennreal.one_lt_top]⟩ +⟨by simp only [measure_univ, ennreal.one_lt_top]⟩ /-- A measure is called finite at filter `f` if it is finite at some set `s ∈ f`. Equivalently, it is eventually finite at `s` in `f.lift' powerset`. -/ @@ -1052,7 +1058,10 @@ def measure.finite_at_filter (μ : measure α) (f : filter α) : Prop := ∃ s lemma finite_at_filter_of_finite (μ : measure α) [finite_measure μ] (f : filter α) : μ.finite_at_filter f := -⟨univ, univ_mem_sets, meas_univ_lt_top⟩ +⟨univ, univ_mem_sets, measure_lt_top μ univ⟩ + +lemma measure.finite_at_bot (μ : measure α) : μ.finite_at_filter ⊥ := +⟨∅, mem_bot_sets, by simp only [measure_empty, with_top.zero_lt_top]⟩ /-- A measure is called locally finite if it is finite in some neighborhood of each point. -/ class locally_finite_measure [topological_space α] (μ : measure α) : Prop := diff --git a/src/measure_theory/set_integral.lean b/src/measure_theory/set_integral.lean index 1a4fe8ad265b2..0f6bc9510cff6 100644 --- a/src/measure_theory/set_integral.lean +++ b/src/measure_theory/set_integral.lean @@ -241,10 +241,10 @@ begin end lemma measure.finite_at_filter.integrable_at_filter_of_tendsto_ae - {l : filter α} [is_measurably_generated l] (hμ : μ.finite_at_filter (l ⊓ μ.ae)) {b} + {l : filter α} [is_measurably_generated l] (hμ : μ.finite_at_filter l) {b} (hf : tendsto f (l ⊓ μ.ae) (𝓝 b)) : integrable_at_filter f l μ := -(hμ.integrable_at_filter hf.norm.is_bounded_under_le).of_inf_ae +(hμ.inf_of_left.integrable_at_filter hf.norm.is_bounded_under_le).of_inf_ae alias measure.finite_at_filter.integrable_at_filter_of_tendsto_ae ← filter.tendsto.integrable_at_filter_ae @@ -344,7 +344,7 @@ begin intros ε ε₀, have : ∀ᶠ s in l.lift' powerset, ∀ᶠ x in μ.ae, x ∈ s → f x ∈ closed_ball b ε := eventually_lift'_powerset_eventually.2 (h.eventually $ closed_ball_mem_nhds _ ε₀), - refine hμ.eventually.mp ((h.integrable_at_filter_ae hμ.inf_of_left).eventually.mp (this.mono _)), + refine hμ.eventually.mp ((h.integrable_at_filter_ae hμ).eventually.mp (this.mono _)), simp only [mem_closed_ball, dist_eq_norm], intros s h_norm h_integrable hμs, rw [← set_integral_const, ← integral_sub hfm h_integrable measurable_const @@ -392,8 +392,7 @@ lemma continuous_at.integral_sub_linear_is_o_ae {μ : measure α} [locally_finite_measure μ] {a : α} {f : α → E} (ha : continuous_at f a) (hfm : measurable f) : is_o (λ s, ∫ x in s, f x ∂μ - (μ s).to_real • f a) (λ s, (μ s).to_real) ((𝓝 a).lift' powerset) := -(tendsto_le_left (@inf_le_left _ _ (𝓝 a) μ.ae) ha).integral_sub_linear_is_o_ae hfm - (μ.finite_at_nhds a) +(ha.mono_left inf_le_left).integral_sub_linear_is_o_ae hfm (μ.finite_at_nhds a) /- namespace integrable diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 9dbc9ad31ea9b..69096d7422f31 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -1996,6 +1996,11 @@ lemma tendsto.eventually {f : α → β} {l₁ : filter α} {l₂ : filter β} { ∀ᶠ x in l₁, p (f x) := hf h +lemma tendsto.frequently {f : α → β} {l₁ : filter α} {l₂ : filter β} {p : β → Prop} + (hf : tendsto f l₁ l₂) (h : ∃ᶠ x in l₁, p (f x)) : + ∃ᶠ y in l₂, p y := +mt hf.eventually h + @[simp] lemma tendsto_bot {f : α → β} {l : filter β} : tendsto f ⊥ l := by simp [tendsto] lemma tendsto_of_not_nonempty {f : α → β} {la : filter α} {lb : filter β} (h : ¬nonempty α) : @@ -2041,13 +2046,13 @@ calc map (g ∘ f) x = map g (map f x) : by rw [map_map] ... ≤ map g y : map_mono hf ... ≤ z : hg -lemma tendsto_le_left {f : α → β} {x y : filter α} {z : filter β} - (h : y ≤ x) : tendsto f x z → tendsto f y z := -le_trans (map_mono h) +lemma tendsto.mono_left {f : α → β} {x y : filter α} {z : filter β} + (hx : tendsto f x z) (h : y ≤ x) : tendsto f y z := +le_trans (map_mono h) hx -lemma tendsto_le_right {f : α → β} {x : filter α} {y z : filter β} - (h₁ : y ≤ z) (h₂ : tendsto f x y) : tendsto f x z := -le_trans h₂ h₁ +lemma tendsto.mono_right {f : α → β} {x : filter α} {y z : filter β} + (hy : tendsto f x y) (hz : y ≤ z) : tendsto f x z := +le_trans hy hz lemma tendsto.ne_bot {f : α → β} {x : filter α} {y : filter β} (h : tendsto f x y) [hx : ne_bot x] : ne_bot y := @@ -2110,9 +2115,9 @@ tendsto_inf.2 ⟨tendsto_inf_left h₁, tendsto_inf_right h₂⟩ tendsto f x (⨅i, y i) ↔ ∀i, tendsto f x (y i) := by simp only [tendsto, iff_self, le_infi_iff] -lemma tendsto_infi' {f : α → β} {x : ι → filter α} {y : filter β} (i : ι) : - tendsto f (x i) y → tendsto f (⨅i, x i) y := -tendsto_le_left (infi_le _ _) +lemma tendsto_infi' {f : α → β} {x : ι → filter α} {y : filter β} (i : ι) (hi : tendsto f (x i) y) : + tendsto f (⨅i, x i) y := +hi.mono_left $ infi_le _ _ lemma tendsto_sup {f : α → β} {x₁ x₂ : filter α} {y : filter β} : tendsto f (x₁ ⊔ x₂) y ↔ tendsto f x₁ y ∧ tendsto f x₂ y := diff --git a/src/order/filter/interval.lean b/src/order/filter/interval.lean index 5a4807227589f..23098c7f249f6 100644 --- a/src/order/filter/interval.lean +++ b/src/order/filter/interval.lean @@ -8,11 +8,36 @@ import order.filter.lift import order.filter.at_top_bot /-! -# Interval-generated filters +# Convergence of intervals + +If both `a` and `b` tend to some filter `l₁`, sometimes this implies that `Ixx a b` tends to +`l₂.lift' powerset`, i.e., for any `s ∈ l₂` eventually `Ixx a b` becomes a subset of `s`. Here and +below `Ixx` is one of `Icc`, `Ico`, `Ioc`, and `Ioo`. We define `filter.tendsto_Ixx_class Ixx l₁ l₂` +to be a typeclass representing this property. + +The instances provide the best `l₂` for a given `l₁`. In many cases `l₁ = l₂` but sometimes we can +drop an endpoint from an interval: e.g., we prove `tendsto_Ixx_class Ico (𝓟 $ Iic a) (𝓟 $ Iio a)`, +i.e., if `u₁ n` and `u₂ n` belong eventually to `Iic a`, then the interval `Ico (u₁ n) (u₂ n)` is +eventually included in `Iio a`. + +The next table shows “output” filters `l₂` for different values of `Ixx` and `l₁`. The instances +that need topology are defined in `topology/algebra/ordered`. + +| Input filter | `Ixx = Icc` | `Ixx = Ico` | `Ixx = Ioc` | `Ixx = Ioo` | +| -----------: | :-----------: | :-----------: | :-----------: | :-----------: | +| `at_top` | `at_top` | `at_top` | `at_top` | `at_top` | +| `at_bot` | `at_bot` | `at_bot` | `at_bot` | `at_bot` | +| `pure a` | `pure a` | `⊥` | `⊥` | `⊥` | +| `𝓟 (Iic a)` | `𝓟 (Iic a)` | `𝓟 (Iio a)` | `𝓟 (Iic a)` | `𝓟 (Iio a)` | +| `𝓟 (Ici a)` | `𝓟 (Ici a)` | `𝓟 (Ici a)` | `𝓟 (Ioi a)` | `𝓟 (Ioi a)` | +| `𝓟 (Ioi a)` | `𝓟 (Ioi a)` | `𝓟 (Ioi a)` | `𝓟 (Ioi a)` | `𝓟 (Ioi a)` | +| `𝓟 (Iio a)` | `𝓟 (Iio a)` | `𝓟 (Iio a)` | `𝓟 (Iio a)` | `𝓟 (Iio a)` | +| `𝓝 a` | `𝓝 a` | `𝓝 a` | `𝓝 a` | `𝓝 a` | +| `𝓝[Iic a] b` | `𝓝[Iic a] b` | `𝓝[Iio a] b` | `𝓝[Iic a] b` | `𝓝[Iio a] b` | +| `𝓝[Ici a] b` | `𝓝[Ici a] b` | `𝓝[Ici a] b` | `𝓝[Ioi a] b` | `𝓝[Ioi a] b` | +| `𝓝[Ioi a] b` | `𝓝[Ioi a] b` | `𝓝[Ioi a] b` | `𝓝[Ioi a] b` | `𝓝[Ioi a] b` | +| `𝓝[Iio a] b` | `𝓝[Iio a] b` | `𝓝[Iio a] b` | `𝓝[Iio a] b` | `𝓝[Iio a] b` | -We say that a filter `f` on a `preorder` is interval generated if each set `s ∈ f` includes -an `ord_connected` subset `t ∈ f`. Equivalently, `f` has a basis `{s i | p i}` which consists -of `ord_connected` sets. -/ variables {α β : Type*} @@ -21,112 +46,152 @@ open_locale classical filter open set function -namespace filter - variables [preorder α] -/-- -A filter `f` on a `preorder` is interval generated if each set `s ∈ f` includes an `ord_connected` -subset `t ∈ f`. --/ -class is_interval_generated (f : filter α) : Prop := -(exists_ord_connected_mem : ∀ ⦃s⦄, s ∈ f → ∃ t ∈ f, ord_connected t ∧ t ⊆ s) - -export is_interval_generated (exists_ord_connected_mem) +namespace filter -/-- If a filter `f` has a basis `{s i | p i}` such that all sets `s i` such that `p i` are -`ord_connected`, then `f` is an interval generated filter. -/ -lemma has_basis.is_interval_generated {f : filter α} {ι} {p : ι → Prop} {s} (h : f.has_basis p s) - (hs : ∀ i, p i → ord_connected (s i)) : - is_interval_generated f := +/-- A pair of filters `l₁`, `l₂` has `tendsto_Ixx_class Ixx` property if `Ixx a b` tends to +`l₂.lift' powerset` as `a` and `b` tend to `l₁`. In all instances `Ixx` is one of `Icc`, `Ico`, +`Ioc`, or `Ioo`. The instances provide the best `l₂` for a given `l₁`. In many cases `l₁ = l₂` but +sometimes we can drop an endpoint from an interval: e.g., we prove `tendsto_Ixx_class Ico (𝓟 $ Iic +a) (𝓟 $ Iio a)`, i.e., if `u₁ n` and `u₂ n` belong eventually to `Iic a`, then the interval `Ico (u₁ +n) (u₂ n)` is eventually included in `Iio a`. + +We mark `l₂` as an `out_param` so that Lean can automatically find an appropriate `l₂` based on +`Ixx` and `l₁`. This way, e.g., `tendsto.Ico h₁ h₂` works without specifying explicitly `l₂`. -/ +class tendsto_Ixx_class (Ixx : α → α → set α) (l₁ : filter α) (l₂ : out_param $ filter α) : Prop := +(tendsto_Ixx : tendsto (λ p : α × α, Ixx p.1 p.2) (l₁ ×ᶠ l₁) (l₂.lift' powerset)) + +lemma tendsto.Icc {l₁ l₂ : filter α} [tendsto_Ixx_class Icc l₁ l₂] + {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) : + tendsto (λ x, Icc (u₁ x) (u₂ x)) lb (l₂.lift' powerset) := +tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂ + +lemma tendsto.Ioc {l₁ l₂ : filter α} [tendsto_Ixx_class Ioc l₁ l₂] + {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) : + tendsto (λ x, Ioc (u₁ x) (u₂ x)) lb (l₂.lift' powerset) := +tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂ + +lemma tendsto.Ico {l₁ l₂ : filter α} [tendsto_Ixx_class Ico l₁ l₂] + {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) : + tendsto (λ x, Ico (u₁ x) (u₂ x)) lb (l₂.lift' powerset) := +tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂ + +lemma tendsto.Ioo {l₁ l₂ : filter α} [tendsto_Ixx_class Ioo l₁ l₂] + {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) : + tendsto (λ x, Ioo (u₁ x) (u₂ x)) lb (l₂.lift' powerset) := +tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂ + +lemma tendsto_Ixx_class_principal {s t : set α} {Ixx : α → α → set α} : + tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t) ↔ ∀ (x ∈ s) (y ∈ s), Ixx x y ⊆ t := begin - refine ⟨λ t ht, _⟩, - rcases h.mem_iff.1 ht with ⟨i, hi, hsi⟩, - exact ⟨s i, h.mem_of_mem hi, hs i hi, hsi⟩, + refine iff.trans ⟨λ h, h.1, λ h, ⟨h⟩⟩ _, + simp [lift'_principal monotone_powerset, -mem_prod, -prod.forall, forall_prod_set] end -/-- If `f` is an interval generated filter, then `ord_connected` sets `s ∈ f` form a basis -of `f`. -/ -lemma has_ord_connected_basis (f : filter α) [is_interval_generated f] : - f.has_basis (λ s : set α, s ∈ f ∧ ord_connected s) id := -f.basis_sets.restrict $ λ s hs, - by simpa only [exists_prop, and_assoc] using exists_ord_connected_mem hs - -lemma is_interval_generated_principal_iff {s : set α} : - is_interval_generated (𝓟 s) ↔ ord_connected s := -begin - refine ⟨_, λ h, (has_basis_principal _).is_interval_generated (λ _ _, h)⟩, - introI h, - rcases exists_ord_connected_mem (mem_principal_self s) with ⟨t, hst, ht, hts⟩, - rwa [subset.antisymm hst hts] -end +lemma tendsto_Ixx_class_inf {l₁ l₁' l₂ l₂' : filter α} {Ixx} + [h : tendsto_Ixx_class Ixx l₁ l₂] [h' : tendsto_Ixx_class Ixx l₁' l₂'] : + tendsto_Ixx_class Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂') := +⟨by simpa only [prod_inf_prod, lift'_inf_powerset] using h.1.inf h'.1⟩ + +lemma tendsto_Ixx_class_of_subset {l₁ l₂ : filter α} {Ixx Ixx' : α → α → set α} + (h : ∀ a b, Ixx a b ⊆ Ixx' a b) [h' : tendsto_Ixx_class Ixx' l₁ l₂] : + tendsto_Ixx_class Ixx l₁ l₂ := +⟨tendsto_lift'_powerset_mono h'.1 $ eventually_of_forall $ prod.forall.2 h⟩ + +lemma has_basis.tendsto_Ixx_class {ι : Type*} {p : ι → Prop} {s} {l : filter α} + (hl : l.has_basis p s) {Ixx : α → α → set α} + (H : ∀ i, p i → ∀ (x ∈ s i) (y ∈ s i), Ixx x y ⊆ s i) : + tendsto_Ixx_class Ixx l l := +⟨(hl.prod_self.tendsto_iff (hl.lift' monotone_powerset)).2 $ λ i hi, + ⟨i, hi, λ x hx, H i hi _ hx.1 _ hx.2⟩⟩ + +instance tendsto_Icc_at_top_at_top : tendsto_Ixx_class Icc (at_top : filter α) at_top := +(has_basis_infi_principal_finite _).tendsto_Ixx_class $ λ s hs, ord_connected_bInter $ + λ i hi, ord_connected_Ici -alias is_interval_generated_principal_iff ↔ _ set.ord_connected.is_interval_generated_principal +instance tendsto_Ico_at_top_at_top : tendsto_Ixx_class Ico (at_top : filter α) at_top := +tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self) -instance is_interval_generated_inf {f g : filter α} [is_interval_generated f] - [is_interval_generated g] : - is_interval_generated (f ⊓ g) := -begin - apply ((has_ord_connected_basis f).inf (has_ord_connected_basis g)).is_interval_generated, - rintros ⟨s, t⟩ ⟨⟨hsf, hsc⟩, htg, htc⟩, - exact hsc.inter htc -end +instance tendsto_Ioc_at_top_at_top : tendsto_Ixx_class Ioc (at_top : filter α) at_top := +tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self) -instance is_interval_generated_at_top : is_interval_generated (at_top : filter α) := -(has_basis_infi_principal_finite _).is_interval_generated $ λ t ht, ord_connected_bInter $ - λ i hi, ord_connected_Ici +instance tendsto_Ioo_at_top_at_top : tendsto_Ixx_class Ioo (at_top : filter α) at_top := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Icc_self) -instance is_interval_generated_at_bot : is_interval_generated (at_bot : filter α) := -(has_basis_infi_principal_finite _).is_interval_generated $ λ t ht, ord_connected_bInter $ +instance tendsto_Icc_at_bot_at_bot : tendsto_Ixx_class Icc (at_bot : filter α) at_bot := +(has_basis_infi_principal_finite _).tendsto_Ixx_class $ λ s hs, ord_connected_bInter $ λ i hi, ord_connected_Iic -/-- If `Ixx` is a function `α → α → set α` such that `Ixx x y ⊆ Icc x y` -(e.g., `Ixx` is one of `Ioo`, `Ico`, `Ioc`, `Icc`), then `Ixx a b` tends to `l.lift' powerset` -as `(a, b)` tends to `l ×ᶠ l`. -/ -lemma tendsto_Ixx_same_filter {Ixx : α → α → set α} (hI : ∀ x y, Ixx x y ⊆ Icc x y) - (l : filter α) [is_interval_generated l] : - tendsto (uncurry Ixx) (l ×ᶠ l) (l.lift' powerset) := -begin - rw [l.basis_sets.prod_self.tendsto_iff (l.basis_sets.lift' (λ _ _, powerset_mono.2))], - intros s hs, - rcases exists_ord_connected_mem hs with ⟨t, htl, htc, hts⟩, - exact ⟨t, htl, λ x hx, subset.trans (hI _ _) (subset.trans (htc hx.1 hx.2) hts)⟩ -end +instance tendsto_Ico_at_bot_at_bot : tendsto_Ixx_class Ico (at_bot : filter α) at_bot := +tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self) -/-- If `Ixx` is a function `α → α → set α` such that `Ixx x y ⊆ Icc x y` -(e.g., `Ixx` is one of `Ioo`, `Ico`, `Ioc`, `Icc`), then `Ixx (f t) (g t)` tends -to `l.lift' powerset` provided that both `f t` and `g t` tend to `l`. -/ -lemma tendsto.Ixx {la : filter α} [is_interval_generated la] - {Ixx : α → α → set α} (hI : ∀ x y, Ixx x y ⊆ Icc x y) - {lb : filter β} {f g : β → α} (hf : tendsto f lb la) (hg : tendsto g lb la) : - tendsto (λ x, Ixx (f x) (g x)) lb (la.lift' powerset) := -(tendsto_Ixx_same_filter hI _).comp (hf.prod_mk hg) - -lemma tendsto.Icc {lb : filter β} {la : filter α} [is_interval_generated la] - {f g : β → α} (hf : tendsto f lb la) (hg : tendsto g lb la) : - tendsto (λ x, Icc (f x) (g x)) lb (la.lift' powerset) := -hf.Ixx (λ _ _, subset.refl _) hg - -lemma tendsto.Ico {lb : filter β} {la : filter α} [is_interval_generated la] - {f g : β → α} (hf : tendsto f lb la) (hg : tendsto g lb la) : - tendsto (λ x, Ico (f x) (g x)) lb (la.lift' powerset) := -hf.Ixx (λ _ _, Ico_subset_Icc_self) hg - -lemma tendsto.Ioc {lb : filter β} {la : filter α} [is_interval_generated la] - {f g : β → α} (hf : tendsto f lb la) (hg : tendsto g lb la) : - tendsto (λ x, Ioc (f x) (g x)) lb (la.lift' powerset) := -hf.Ixx (λ _ _, Ioc_subset_Icc_self) hg - -lemma tendsto.Ioo {lb : filter β} {la : filter α} [is_interval_generated la] - {f g : β → α} (hf : tendsto f lb la) (hg : tendsto g lb la) : - tendsto (λ x, Ioo (f x) (g x)) lb (la.lift' powerset) := -hf.Ixx (λ _ _, Ioo_subset_Icc_self) hg +instance tendsto_Ioc_at_bot_at_bot : tendsto_Ixx_class Ioc (at_bot : filter α) at_bot := +tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self) -end filter +instance tendsto_Ioo_at_bot_at_bot : tendsto_Ixx_class Ioo (at_bot : filter α) at_bot := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Icc_self) + +instance tendsto_Icc_Ici_Ici {a : α} : tendsto_Ixx_class Icc (𝓟 (Ici a)) (𝓟 (Ici a)) := +tendsto_Ixx_class_principal.2 ord_connected_Ici + +instance tendsto_Icc_Iic_Iic {a : α} : tendsto_Ixx_class Icc (𝓟 (Iic a)) (𝓟 (Iic a)) := +tendsto_Ixx_class_principal.2 ord_connected_Iic + +instance tendsto_Icc_Ioi_Ioi {a : α} : tendsto_Ixx_class Icc (𝓟 (Ioi a)) (𝓟 (Ioi a)) := +tendsto_Ixx_class_principal.2 ord_connected_Ioi -open set filter +instance tendsto_Icc_Iio_Iio {a : α} : tendsto_Ixx_class Icc (𝓟 (Iio a)) (𝓟 (Iio a)) := +tendsto_Ixx_class_principal.2 ord_connected_Iio -lemma set.ord_connected.is_interval_generated_inf_principal [preorder α] - {f : filter α} [is_interval_generated f] {s : set α} (hs : ord_connected s) : - is_interval_generated (f ⊓ 𝓟 s) := -by haveI := hs.is_interval_generated_principal; apply_instance +instance tendsto_Ico_Ici_Ici {a : α} : tendsto_Ixx_class Ico (𝓟 (Ici a)) (𝓟 (Ici a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self) + +instance tendsto_Ico_Ioi_Ioi {a : α} : tendsto_Ixx_class Ico (𝓟 (Ioi a)) (𝓟 (Ioi a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self) + +instance tendsto_Ico_Iic_Iio {a : α} : tendsto_Ixx_class Ico (𝓟 (Iic a)) (𝓟 (Iio a)) := +tendsto_Ixx_class_principal.2 $ λ a ha b hb x hx, lt_of_lt_of_le hx.2 hb + +instance tendsto_Ico_Iio_Iio {a : α} : tendsto_Ixx_class Ico (𝓟 (Iio a)) (𝓟 (Iio a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self) + +instance tendsto_Ioc_Ici_Ioi {a : α} : tendsto_Ixx_class Ioc (𝓟 (Ici a)) (𝓟 (Ioi a)) := +tendsto_Ixx_class_principal.2 $ λ x hx y hy t ht, lt_of_le_of_lt hx ht.1 + +instance tendsto_Ioc_Iic_Iic {a : α} : tendsto_Ixx_class Ioc (𝓟 (Iic a)) (𝓟 (Iic a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self) + +instance tendsto_Ioc_Iio_Iio {a : α} : tendsto_Ixx_class Ioc (𝓟 (Iio a)) (𝓟 (Iio a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self) + +instance tendsto_Ioc_Ioi_Ioi {a : α} : tendsto_Ixx_class Ioc (𝓟 (Ioi a)) (𝓟 (Ioi a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self) + +instance tendsto_Ioo_Ici_Ioi {a : α} : tendsto_Ixx_class Ioo (𝓟 (Ici a)) (𝓟 (Ioi a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self) + +instance tendsto_Ioo_Iic_Iio {a : α} : tendsto_Ixx_class Ioo (𝓟 (Iic a)) (𝓟 (Iio a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ico_self) + +instance tendsto_Ioo_Ioi_Ioi {a : α} : tendsto_Ixx_class Ioo (𝓟 (Ioi a)) (𝓟 (Ioi a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self) + +instance tendsto_Ioo_Iio_Iio {a : α} : tendsto_Ixx_class Ioo (𝓟 (Iio a)) (𝓟 (Iio a)) := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self) + +variable [partial_order β] + +instance tendsto_Icc_pure_pure {a : β} : tendsto_Ixx_class Icc (pure a) (pure a : filter β) := +by { rw ← principal_singleton, exact tendsto_Ixx_class_principal.2 ord_connected_singleton } + +instance tendsto_Ico_pure_bot {a : β} : tendsto_Ixx_class Ico (pure a) ⊥ := +⟨by simp [lift'_bot monotone_powerset]⟩ + +instance tendsto_Ioc_pure_bot {a : β} : tendsto_Ixx_class Ioc (pure a) ⊥ := +⟨by simp [lift'_bot monotone_powerset]⟩ + +instance tendsto_Ioo_pure_bot {a : β} : tendsto_Ixx_class Ioo (pure a) ⊥ := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self) + +end filter diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean index 999a4a3ee84e2..4565ab26d9832 100644 --- a/src/topology/algebra/infinite_sum.lean +++ b/src/topology/algebra/infinite_sum.lean @@ -105,7 +105,7 @@ by rw [← set.indicator_range_comp, subtype.range_coe, has_sum_subtype_iff_of_support_subset $ set.subset.refl _ lemma has_sum_fintype [fintype β] (f : β → α) : has_sum f (∑ b, f b) := -order_top.tendsto_at_top _ +order_top.tendsto_at_top_nhds _ protected lemma finset.has_sum (s : finset β) (f : β → α) : has_sum (f ∘ coe : (↑s : set β) → α) (∑ b in s, f b) := diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean index 07dddb8011dc6..ee1c98fcb9f73 100644 --- a/src/topology/algebra/ordered.lean +++ b/src/topology/algebra/ordered.lean @@ -615,46 +615,28 @@ lemma tendsto_order {f : β → α} {a : α} {x : filter β} : tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ (∀ a' > a, ∀ᶠ b in x, f b < a') := by simp [nhds_eq_order a, tendsto_inf, tendsto_infi, tendsto_principal] -instance nhds_is_interval_generated (a : α) : is_interval_generated (𝓝 a) := +instance tendsto_Icc_class_nhds (a : α) : tendsto_Ixx_class Icc (𝓝 a) (𝓝 a) := begin simp only [nhds_eq_order, infi_subtype'], refine ((has_basis_infi_principal_finite _).inf - (has_basis_infi_principal_finite _)).is_interval_generated _, - refine λ s hs, (ord_connected_bInter $ λ _ _, _).inter (ord_connected_bInter $ λ _ _, _), + (has_basis_infi_principal_finite _)).tendsto_Ixx_class (λ s hs, _), + refine (ord_connected_bInter _).inter (ord_connected_bInter _); intros _ _, exacts [ord_connected_Ioi, ord_connected_Iio] end -instance nhds_within_Ici_is_interval_generated (a b : α) : - is_interval_generated (nhds_within a (Ici b)) := -ord_connected_Ici.is_interval_generated_inf_principal +instance tendsto_Ico_class_nhds (a : α) : tendsto_Ixx_class Ico (𝓝 a) (𝓝 a) := +tendsto_Ixx_class_of_subset (λ _ _, Ico_subset_Icc_self) -instance nhds_within_Ioi_is_interval_generated (a b : α) : - is_interval_generated (nhds_within a (Ioi b)) := -ord_connected_Ioi.is_interval_generated_inf_principal +instance tendsto_Ioc_class_nhds (a : α) : tendsto_Ixx_class Ioc (𝓝 a) (𝓝 a) := +tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self) -instance nhds_within_Iic_is_interval_generated (a b : α) : - is_interval_generated (nhds_within a (Iic b)) := -ord_connected_Iic.is_interval_generated_inf_principal +instance tendsto_Ioo_class_nhds (a : α) : tendsto_Ixx_class Ioo (𝓝 a) (𝓝 a) := +tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Icc_self) -instance nhds_within_Iio_is_interval_generated (a b : α) : - is_interval_generated (nhds_within a (Iio b)) := -ord_connected_Iio.is_interval_generated_inf_principal - -instance nhds_within_Icc_is_interval_generated (a b c : α) : - is_interval_generated (nhds_within a (Icc b c)) := -ord_connected_Icc.is_interval_generated_inf_principal - -instance nhds_within_Ico_is_interval_generated (a b c : α) : - is_interval_generated (nhds_within a (Ico b c)) := -ord_connected_Ico.is_interval_generated_inf_principal - -instance nhds_within_Ioc_is_interval_generated (a b c : α) : - is_interval_generated (nhds_within a (Ioc b c)) := -ord_connected_Ioc.is_interval_generated_inf_principal - -instance nhds_within_Ioo_is_interval_generated (a b c : α) : - is_interval_generated (nhds_within a (Ioo b c)) := -ord_connected_Ioo.is_interval_generated_inf_principal +instance tendsto_Ixx_nhds_within (a : α) {s t : set α} {Ixx} + [tendsto_Ixx_class Ixx (𝓝 a) (𝓝 a)] [tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t)]: + tendsto_Ixx_class Ixx (𝓝[s] a) (𝓝[t] a) := +filter.tendsto_Ixx_class_inf /-- Also known as squeeze or sandwich theorem. This version assumes that inequalities hold eventually for the filter. -/ @@ -1534,7 +1516,7 @@ lemma map_Sup_of_continuous_at_of_monotone' {f : α → β} {s : set α} (Cf : c f (Sup s) = Sup (f '' s) := --This is a particular case of the more general is_lub_of_is_lub_of_tendsto (is_lub_of_is_lub_of_tendsto (λ x hx y hy xy, Mf xy) (is_lub_Sup _) hs $ - tendsto_le_left inf_le_left Cf).Sup_eq.symm + Cf.mono_left inf_le_left).Sup_eq.symm /-- A monotone function `s` sending `bot` to `bot` and continuous at the supremum of a set sends this supremum to the supremum of the image of this set. -/ @@ -1623,7 +1605,7 @@ lemma map_cSup_of_continuous_at_of_monotone {f : α → β} {s : set α} (Cf : c begin refine ((is_lub_cSup (ne.image f) (Mf.map_bdd_above H)).unique _).symm, refine is_lub_of_is_lub_of_tendsto (λx hx y hy xy, Mf xy) (is_lub_cSup ne H) ne _, - exact tendsto_le_left inf_le_left Cf + exact Cf.mono_left inf_le_left end /-- If a monotone function is continuous at the indexed supremum of a bounded function on diff --git a/src/topology/basic.lean b/src/topology/basic.lean index 676f2867c0f22..4c79a75a9c56d 100644 --- a/src/topology/basic.lean +++ b/src/topology/basic.lean @@ -578,11 +578,11 @@ assume a s hs, mem_pure_sets.2 $ mem_of_nhds hs lemma tendsto_pure_nhds {α : Type*} [topological_space β] (f : α → β) (a : α) : tendsto f (pure a) (𝓝 (f a)) := -tendsto_le_right (pure_le_nhds _) (tendsto_pure_pure f a) +(tendsto_pure_pure f a).mono_right (pure_le_nhds _) -lemma order_top.tendsto_at_top {α : Type*} [order_top α] [topological_space β] (f : α → β) : +lemma order_top.tendsto_at_top_nhds {α : Type*} [order_top α] [topological_space β] (f : α → β) : tendsto f at_top (𝓝 $ f ⊤) := -tendsto_le_right (pure_le_nhds _) $ tendsto_at_top_pure f +(tendsto_at_top_pure f).mono_right (pure_le_nhds _) @[simp] instance nhds_ne_bot {a : α} : ne_bot (𝓝 a) := ne_bot_of_le (pure_le_nhds a) diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean index e52a1dc9831a7..83026c795bbbb 100644 --- a/src/topology/continuous_on.lean +++ b/src/topology/continuous_on.lean @@ -114,6 +114,10 @@ lemma filter.eventually.self_of_nhds_within {p : α → Prop} {s : set α} {x : (h : ∀ᶠ y in 𝓝[s] x, p y) (hx : x ∈ s) : p x := mem_of_mem_nhds_within hx h +lemma tendsto_const_nhds_within {l : filter β} {s : set α} {a : α} (ha : a ∈ s) : + tendsto (λ x : β, a) l (𝓝[s] a) := +tendsto_const_pure.mono_right $ pure_le_nhds_within ha + theorem nhds_within_restrict'' {a : α} (s : set α) {t : set α} (h : t ∈ 𝓝[s] a) : 𝓝[s] a = 𝓝[s ∩ t] a := le_antisymm @@ -199,17 +203,17 @@ lemma map_nhds_within (f : α → β) (a : α) (s : set α) : theorem tendsto_nhds_within_mono_left {f : α → β} {a : α} {s t : set α} {l : filter β} (hst : s ⊆ t) (h : tendsto f (𝓝[t] a) l) : tendsto f (𝓝[s] a) l := -tendsto_le_left (nhds_within_mono a hst) h +h.mono_left $ nhds_within_mono a hst theorem tendsto_nhds_within_mono_right {f : β → α} {l : filter β} {a : α} {s t : set α} (hst : s ⊆ t) (h : tendsto f l (𝓝[s] a)) : tendsto f l (𝓝[t] a) := -tendsto_le_right (nhds_within_mono a hst) h +h.mono_right (nhds_within_mono a hst) theorem tendsto_nhds_within_of_tendsto_nhds {f : α → β} {a : α} {s : set α} {l : filter β} (h : tendsto f (𝓝 a) l) : tendsto f (𝓝[s] a) l := -tendsto_le_left inf_le_left h +h.mono_left inf_le_left theorem principal_subtype {α : Type*} (s : set α) (t : set {x // x ∈ s}) : 𝓟 t = comap coe (𝓟 ((coe : s → α) '' t)) := @@ -392,7 +396,7 @@ by simp [continuous_iff_continuous_at, continuous_on, continuous_at, continuous_ lemma continuous_within_at.mono {f : α → β} {s t : set α} {x : α} (h : continuous_within_at f t x) (hs : s ⊆ t) : continuous_within_at f s x := -tendsto_le_left (nhds_within_mono x hs) h +h.mono_left (nhds_within_mono x hs) lemma continuous_within_at_inter' {f : α → β} {s t : set α} {x : α} (h : t ∈ 𝓝[s] x) : continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x := @@ -490,7 +494,7 @@ begin have : tendsto f (𝓟 s) (𝓟 t), by { rw tendsto_principal_principal, exact λx hx, h hx }, have : tendsto f (𝓝[s] x) (𝓟 t) := - tendsto_le_left inf_le_right this, + this.mono_left inf_le_right, have : tendsto f (𝓝[s] x) (𝓝[t] (f x)) := tendsto_inf.2 ⟨hf, this⟩, exact tendsto.comp hg this @@ -508,7 +512,7 @@ lemma continuous_on.comp {g : β → γ} {f : α → β} {s : set α} {t : set lemma continuous_on.mono {f : α → β} {s t : set α} (hf : continuous_on f s) (h : t ⊆ s) : continuous_on f t := -λx hx, tendsto_le_left (nhds_within_mono _ h) (hf x (h hx)) +λx hx, (hf x (h hx)).mono_left (nhds_within_mono _ h) lemma continuous_on.comp' {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : continuous_on g t) (hf : continuous_on f s) : @@ -524,7 +528,7 @@ end lemma continuous.continuous_within_at {f : α → β} {s : set α} {x : α} (h : continuous f) : continuous_within_at f s x := -tendsto_le_left inf_le_left (h.tendsto x) +h.continuous_at.continuous_within_at lemma continuous.comp_continuous_on {g : β → γ} {f : α → β} {s : set α} (hg : continuous g) (hf : continuous_on f s) :