From 1ce88e65e2f1110d193405dbb9f36ca5b5bf7bc4 Mon Sep 17 00:00:00 2001 From: IshYosh <103252572+IshiguroYoshihiro@users.noreply.github.com> Date: Thu, 21 Dec 2023 15:55:11 +0900 Subject: [PATCH] ae_eq lemmas (#1110) * fixes #1096 --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 19 ++++++++- theories/lebesgue_integral.v | 51 +----------------------- theories/measure.v | 75 ++++++++++++++++++++++++++++++++++-- 3 files changed, 91 insertions(+), 54 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 89956a72b..80bd1e42e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,12 +58,29 @@ `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`, `maximal_inequality` +- in file `measure.v` + + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`. + ### Changed - in `normedtype.v`: + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns duplicate-free lists of indices - + +- moved from `lebesgue_integral.v` to `measure.v`: + + definition `ae_eq` + + lemmas + `ae_eq0`, + `ae_eq_comp`, + `ae_eq_funeposneg`, + `ae_eq_refl`, + `ae_eq_trans`, + `ae_eq_sub`, + `ae_eq_mul2r`, + `ae_eq_mul2l`, + `ae_eq_mul1l`, + `ae_eq_abse` + ### Renamed - in `exp.v`: diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0c58399f6..4e65d1f10 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -38,7 +38,6 @@ Require Import esum measure lebesgue_measure numfun. (* Rintegral mu D f := fine (\int[mu]_(x in D) f x). *) (* mu.-integrable D f == f is measurable over D and the integral of f *) (* w.r.t. D is < +oo *) -(* ae_eq D f g == f is equal to g almost everywhere *) (* m1 \x m2 == product measure over T1 * T2, m1 is a measure *) (* measure over T1, and m2 is a sigma finite *) (* measure over T2 *) @@ -3535,54 +3534,6 @@ Proof. by rewrite -integral_setI_indic// setIid. Qed. End integral_indic. -Section ae_eq. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (D : set T). -Implicit Types f g h i : T -> \bar R. - -Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}. - -Lemma ae_eq0 f g : measurable D -> mu D = 0 -> ae_eq f g. -Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed. - -Lemma ae_eq_comp (j : \bar R -> \bar R) f g : - ae_eq f g -> ae_eq (j \o f) (j \o g). -Proof. by apply: filterS => x /[apply] /= ->. Qed. - -Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. -Proof. -split=> [fg|[]]. - by rewrite /funepos /funeneg; split; apply: filterS fg => x /[apply] ->. -apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. -by rewrite (funeposneg f) (funeposneg g) fg gf. -Qed. - -Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed. - -Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f. -Proof. by apply: filterS => x + Dx => /(_ Dx). Qed. - -Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h. -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed. - -Lemma ae_eq_sub f g h i : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) -> /(_ Dx) ->. Qed. - -Lemma ae_eq_mul2r f g h : ae_eq f g -> ae_eq (f \* h) (g \* h). -Proof. by apply: filterS => x /[apply] ->. Qed. - -Lemma ae_eq_mul2l f g h : ae_eq f g -> ae_eq (h \* f) (h \* g). -Proof. by apply: filterS => x /[apply] ->. Qed. - -Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f). -Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed. - -Lemma ae_eq_abse f g : ae_eq f g -> ae_eq (abse \o f) (abse \o g). -Proof. by apply: filterS => x /[apply] /= ->. Qed. - -End ae_eq. - Section ae_eq_integral. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) @@ -3806,7 +3757,7 @@ Qed. Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> (forall x, D x -> 0 <= f x) -> (forall x, D x -> 0 <= g x) -> - ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). + ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEindic// [RHS]integralEindic//. diff --git a/theories/measure.v b/theories/measure.v index c96a326f4..52903be3b 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -195,6 +195,7 @@ From HB Require Import structures. (* measure_is_complete mu == the measure mu is complete *) (* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *) (* declared as an instance of the type of filters *) +(* ae_eq D f g == f is equal to g almost everywhere *) (* *) (* * From a premeasure to an outer measure (Measure Extension Theorem part 1) *) (* measurable_cover X == the set of sequences F such that *) @@ -3363,6 +3364,66 @@ move=> aP; have -> : P = setT by rewrite predeqE => t; split. by apply/negligibleP; [rewrite setCT|rewrite setCT measure0]. Qed. +Section ae_eq. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (D : set T). +Implicit Types f g h i : T -> \bar R. + +Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}. + +Lemma ae_eq0 f g : measurable D -> mu D = 0 -> ae_eq f g. +Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed. + +Lemma ae_eq_comp (j : \bar R -> \bar R) f g : + ae_eq f g -> ae_eq (j \o f) (j \o g). +Proof. by apply: filterS => x /[apply] /= ->. Qed. + +Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. +Proof. +split=> [fg|[]]. + by rewrite /funepos /funeneg; split; apply: filterS fg => x /[apply] ->. +apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. +by rewrite (funeposneg f) (funeposneg g) fg gf. +Qed. + +Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed. + +Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f. +Proof. by apply: filterS => x + Dx => /(_ Dx). Qed. + +Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h. +Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed. + +Lemma ae_eq_sub f g h i : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). +Proof. by apply: filterS2 => x + + Dx => /(_ Dx) -> /(_ Dx) ->. Qed. + +Lemma ae_eq_mul2r f g h : ae_eq f g -> ae_eq (f \* h) (g \* h). +Proof. by apply: filterS => x /[apply] ->. Qed. + +Lemma ae_eq_mul2l f g h : ae_eq f g -> ae_eq (h \* f) (h \* g). +Proof. by apply: filterS => x /[apply] ->. Qed. + +Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f). +Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed. + +Lemma ae_eq_abse f g : ae_eq f g -> ae_eq (abse \o f) (abse \o g). +Proof. by apply: filterS => x /[apply] /= ->. Qed. + +End ae_eq. + +Section ae_eq_lemmas. +Context d (T : measurableType d) (R : realType). +Implicit Types mu : {measure set T -> \bar R}. + +Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. +Proof. +move=> BA [N [mN N0 fg]]; exists N; split => //. +by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->. +Qed. + +End ae_eq_lemmas. + Definition sigma_subadditive {T} {R : numFieldType} (mu : set T -> \bar R) := forall (F : (set T) ^nat), mu (\bigcup_n (F n)) <= \sum_(i \bar R. Definition measure_dominates m1 m2 := forall A, measurable A -> m2 A = 0 -> m1 A = 0. -Local Notation "m1 `<< m2" := (measure_dominates m1 m2). +End absolute_continuity. +Notation "m1 `<< m2" := (measure_dominates m1 m2). + +Section absolute_continuity_lemmas. +Context d (T : measurableType d) (R : realType). +Implicit Types m : {measure set T -> \bar R}. Lemma measure_dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3. Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed. -End absolute_continuity. -Notation "m1 `<< m2" := (measure_dominates m1 m2). +Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> + m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g. +Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed. + +End absolute_continuity_lemmas. Section essential_supremum. Context d {T : measurableType d} {R : realType}.