From 2b875af25018a8d1c0e0ae4c5f5cbd5f48a2a4ab Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Jun 2024 12:59:41 +0900 Subject: [PATCH 1/2] ae corollary of FTC1 Co-authored-by: zstone1 --- CHANGELOG_UNRELEASED.md | 5 +++++ theories/ftc.v | 30 ++++++++++++++++++------------ 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c52d4873e..b8315e845 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -23,6 +23,8 @@ + definition `completed_algebra_gen` + lemmas `g_sigma_completed_algebra_genE`, `negligible_sub_caratheodory`, `completed_caratheodory_measurable` +- in `ftc.v`: + + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`) ### Changed @@ -52,6 +54,9 @@ + `lee_ndivr_mulr` -> `lee_ndivrMr` + `eqe_pdivr_mull` -> `eqe_pdivrMl` +- in `ftc.v`: + + `FTC1` -> `FTC1_lebesgue_pt` + ### Generalized ### Deprecated diff --git a/theories/ftc.v b/theories/ftc.v index c47b03571..0ffe796be 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -23,7 +23,7 @@ Local Open Scope ring_scope. Section FTC. Context {R : realType}. -Notation mu := lebesgue_measure. +Notation mu := (@lebesgue_measure R). Local Open Scope ereal_scope. Implicit Types (f : R -> R) (a : itv_bound R). @@ -179,7 +179,7 @@ apply: cvg_at_right_left_dnbhs. Unshelve. all: by end_near. Qed. (* NB: right-closed interval *) -Lemma FTC1 f a : mu.-integrable setT (EFin \o f) -> +Lemma FTC1_lebesgue_pt f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in forall x, a < BRight x -> lebesgue_pt f x -> derivable F x 1 /\ F^`() x = f x. @@ -191,7 +191,18 @@ have /= := FTC0 intf ax fx. set g := (f in f n @[n --> _] --> _ -> _). set h := (f in _ -> f n @[n --> _] --> _). suff : g = h by move=> <-. -by apply/funext => y;rewrite /g /h /= [X in F (X + _)](mulr1). +by apply/funext => y;rewrite /g /h /= [X in F (X + _)]mulr1. +Qed. + +Corollary FTC1 f a : mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in + {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}. +Proof. +move=> intf F. +have /lebesgue_differentiation : locally_integrable setT f. + by apply: integrable_locally => //; exact: openT. +apply: filterS; first exact: (ae_filter_ringOfSetsType mu). +by move=> i fi ai; apply: FTC1_lebesgue_pt => //; rewrite ltNyr. Qed. Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) -> @@ -199,18 +210,13 @@ Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) -> forall x, a < BRight x -> {for x, continuous f} -> derivable F x 1 /\ F^`() x = f x. Proof. -move=> fi F x ax fx. -have lfx : lebesgue_pt f x. - near (0%R:R)^'+ => e. - apply: (@continuous_lebesgue_pt _ _ _ (ball x e)). +move=> fi F x ax fx; have lfx : lebesgue_pt f x. + near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)). - exact: ball_open_nbhs. - exact: measurable_ball. - - case/integrableP : fi => + _. - by move/EFin_measurable_fun; exact: measurable_funS. + - by apply/measurable_funTS/EFin_measurable_fun; exact: measurable_int fi. - exact: fx. -have lif : locally_integrable setT f. - by apply: integrable_locally => //; exact: openT. -have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1 f a fi x. +have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1_lebesgue_pt f a fi x. by split; [exact: dfx|rewrite f'xE]. Unshelve. all: by end_near. Qed. From 130a44fd23423493cec28709d7c3476f6381776d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 24 Jun 2024 14:50:17 +0900 Subject: [PATCH 2/2] specialized lemma --- CHANGELOG_UNRELEASED.md | 1 + theories/ftc.v | 9 +++++++++ 2 files changed, 10 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b8315e845..b27e544cf 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -25,6 +25,7 @@ `completed_caratheodory_measurable` - in `ftc.v`: + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`) + + lemma `FTC1Ny` ### Changed diff --git a/theories/ftc.v b/theories/ftc.v index 0ffe796be..ab9f19614 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -205,6 +205,15 @@ apply: filterS; first exact: (ae_filter_ringOfSetsType mu). by move=> i fi ai; apply: FTC1_lebesgue_pt => //; rewrite ltNyr. Qed. +Corollary FTC1Ny f : mu.-integrable setT (EFin \o f) -> + let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in + {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}. +Proof. +move=> intf F; have := FTC1 -oo%O intf. +apply: filterS; first exact: (ae_filter_ringOfSetsType mu). +by move=> r /=; apply; rewrite ltNyr. +Qed. + Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in forall x, a < BRight x -> {for x, continuous f} ->