Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lebesgue measure 20230807 #1005

Merged
merged 2 commits into from
Aug 8, 2023
Merged

Lebesgue measure 20230807 #1005

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0ec4248
lebesgue inner regularity lemma
affeldt-aist Aug 7, 2023
d43b2b2
fix for compatibility with earlier versions
affeldt-aist Aug 8, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,17 @@

- in `kernel.v`:
+ `kseries` is now an instance of `Kernel_isSFinite_subdef`
- in `classical_sets.v`:
+ lemma `setU_id2r`
- in `lebesgue_measure.v`:
+ lemma `compact_measurable`

- in `measure.v`:
+ lemmas `outer_measure_subadditive`, `outer_measureU2`

- in `lebesgue_measure.v`:
+ declare `lebesgue_measure` as a `SigmaFinite` instance
+ lemma `lebesgue_regularity_inner_sup`

### Changed

Expand Down
9 changes: 9 additions & 0 deletions classical/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -650,6 +650,14 @@ Proof. by rewrite setUA !(setUAC _ C) -(setUA _ C) setUid. Qed.
Lemma setUUr A B C : A `|` (B `|` C) = (A `|` B) `|` (A `|` C).
Proof. by rewrite !(setUC A) setUUl. Qed.

Lemma setU_id2r C A B :
(forall x, (~` B) x -> A x = C x) -> (A `|` B) = (C `|` B).
Proof.
move=> h; apply/seteqP; split => [x [Ax|Bx]|x [Cx|Bx]]; [|by right| |by right].
- by have [|/h {}h] := pselect (B x); [by right|left; rewrite -h].
- by have [|/h {}h] := pselect (B x); [by right|left; rewrite h].
Qed.

Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.

Lemma setDUK A B : A `<=` B -> A `|` (B `\` A) = B.
Expand Down Expand Up @@ -1028,6 +1036,7 @@ Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.
Notation setvI := setICl.
#[deprecated(since="mathcomp-analysis 0.6", note="Use setICr instead.")]
Notation setIv := setICr.
Arguments setU_id2r {T} C {A B}.

Section set_order.
Import Order.TTheory.
Expand Down
71 changes: 62 additions & 9 deletions theories/lebesgue_measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -387,6 +387,14 @@ Qed.
Definition lebesgue_measure := measure_extension [the measure _ _ of hlength].
HB.instance Definition _ := Measure.on lebesgue_measure.

(* TODO: this ought to be turned into a Let but older version of mathcomp/coq
does not seem to allow, try to change asap *)
Local Lemma sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.
Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.

HB.instance Definition _ := @isSigmaFinite.Build _ _ _
lebesgue_measure sigmaT_finite_lebesgue_measure.

End itv_semiRingOfSets.
Arguments hlength {R}.
#[global] Hint Extern 0 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core.
Expand Down Expand Up @@ -1424,17 +1432,19 @@ by apply: measurableI => //; exact: open_measurable.
Qed.

Lemma closed_measurable (U : set R) : closed U -> measurable U.
Proof. by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed.

Lemma compact_measurable (A : set R) : compact A -> measurable A.
Proof.
move/closed_openC=> ?; rewrite -[U]setCK; apply: measurableC.
exact: open_measurable.
by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable.
Qed.

Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) :
measurable D -> continuous f -> measurable_fun D f.
Proof.
move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)).
move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //.
by exact/cf/interval_open.
exact/cf/interval_open.
Qed.

Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) :
Expand Down Expand Up @@ -1975,9 +1985,9 @@ wlog : eps epspos D mD finD / exists ab : R * R, D `<=` `[ab.1, ab.2]%classic.
by apply: compact_closed => //; exact: Rhausdorff.
exact: interval_closed.
- by move=> ? [/VDab []].
have -> : D `\` (V `&` `[a, b]) = (D `&` `[a, b]) `\` V `|` D `\` `[a, b].
by rewrite setDIr eqEsubset; split => z /=; case: (z \in `[a, b]);
(try tauto); try (by case; case; left); try (by case; case; right).
rewrite setDIr (setU_id2r ((D `&` `[a, b]) `\` V)); last first.
move=> z ; rewrite setDE setCI setCK => -[?|?];
by apply/propext; split => [[]|[[]]].
have mV : measurable V.
by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff.
rewrite [eps]splitr EFinD (measureU mu) // ?lte_add //.
Expand All @@ -1999,10 +2009,53 @@ exists (`[a, b] `&` ~` U); split.
rewrite [_ `&` ~` _ ](iffRL (disjoints_subset _ _)) ?setCK // set0U.
move: mDeps; rewrite /D' ?setDE setCI setIUr setCK [U `&` D]setIC.
move => /(le_lt_trans _); apply; apply: le_measure; last by move => ?; right.
by rewrite inE; apply: measurableI => //; apply: open_measurable.
by rewrite inE; apply: measurableI => //; exact: open_measurable.
rewrite inE; apply: measurableU.
by (apply: measurableI; first exact: open_measurable); exact: measurableC.
by apply: measurableI => //; apply: open_measurable.
by apply: measurableI; [exact: open_measurable|exact: measurableC].
by apply: measurableI => //; exact: open_measurable.
Qed.

Let lebesgue_regularity_innerE_bounded (A : set R) : measurable A ->
mu A < +oo ->
mu A = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` A]].
Proof.
move=> mA muA; apply/eqP; rewrite eq_le; apply/andP; split; last first.
by apply: ub_ereal_sup => /= x [B /= [cB BA <-{x}]]; exact: le_outer_measure.
apply/lee_addgt0Pr => e e0.
have [B [cB BA /= ABe]] := lebesgue_regularity_inner mA muA e0.
rewrite -{1}(setDKU BA) (@le_trans _ _ (mu B + mu (A `\` B)))//.
by rewrite setUC outer_measureU2.
by rewrite lee_add//; [apply: ereal_sup_ub => /=; exists B|exact/ltW].
Qed.

Lemma lebesgue_regularity_inner_sup (D : set R) (eps : R) : measurable D ->
mu D = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` D]].
Proof.
move=> mD; have [?|] := ltP (mu D) +oo.
exact: lebesgue_regularity_innerE_bounded.
have /sigma_finiteP [/= F RFU [Fsub ffin]] := sigmaT_finite_lebesgue_measure R (*TODO: sigma_finiteT mu should be enough but does not seem to work with holder version of mathcomp/coq *).
rewrite leye_eq => /eqP /[dup] + ->.
have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI.
move=> FDp; apply/esym/eq_infty => M.
have : (fun n => mu (F n `&` D)) @ \oo --> +oo.
rewrite -FDp; apply: nondecreasing_cvg_mu.
- by move=> i; apply: measurableI => //; exact: (ffin i).1.
- by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1).
- by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub.
move/cvgey_ge => /(_ (M + 1)%R) [N _ /(_ _ (lexx N))].
have [mFN FNoo] := ffin N.
have [] := @lebesgue_regularity_inner (F N `&` D) _ _ _ ltr01.
- exact: measurableI.
- by rewrite (le_lt_trans _ (ffin N).2)// measureIl.
move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD.
rewrite (@le_trans _ _ (mu V))//; last first.
apply: ereal_sup_ub; exists V => //=; split => //.
exact: (subset_trans VFND (@subIsetr _ _ _)).
rewrite -(@lee_add2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//.
rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI.
rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first.
by rewrite measureIr//; apply: measurableI.
by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI.
Qed.

End lebesgue_regularity.
Expand Down
33 changes: 32 additions & 1 deletion theories/measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3352,6 +3352,37 @@ Arguments outer_measure_ge0 {R T} _.
Arguments le_outer_measure {R T} _.
Arguments outer_measure_sigma_subadditive {R T} _.

Section outer_measureU.
Context d (T : semiRingOfSetsType d) (R : realType).
Variable mu : {outer_measure set T -> \bar R}.
Local Open Scope ereal_scope.

Lemma outer_measure_subadditive (F : nat -> set T) n :
mu (\big[setU/set0]_(i < n) F i) <= \sum_(i < n) mu (F i).
Proof.
pose F' := fun k => if (k < n)%N then F k else set0.
rewrite -(big_mkord xpredT F) big_nat (eq_bigr F')//; last first.
by move=> k /= kn; rewrite /F' kn.
rewrite -big_nat big_mkord.
have := outer_measure_sigma_subadditive mu F'.
rewrite (bigcup_splitn n) (_ : bigcup _ _ = set0) ?setU0; last first.
by rewrite bigcup0 // => k _; rewrite /F' /= ltnNge leq_addr.
move/le_trans; apply.
rewrite (nneseries_split n); last by move=> ?; exact: outer_measure_ge0.
rewrite [X in _ + X](_ : _ = 0) ?adde0//; last first.
rewrite eseries_cond/= eseries_mkcond eseries0//.
by move=> k _; case: ifPn => //; rewrite /F' leqNgt => /negbTE ->.
by apply: lee_sum => i _; rewrite /F' ltn_ord.
Qed.

Lemma outer_measureU2 A B : mu (A `|` B) <= mu A + mu B.
Proof.
have := outer_measure_subadditive (bigcup2 A B) 2.
by rewrite !big_ord_recl/= !big_ord0 setU0 adde0.
Qed.

End outer_measureU.

Lemma le_outer_measureIC (R : realFieldType) T
(mu : {outer_measure set T -> \bar R}) (A X : set T) :
mu X <= mu (X `&` A) + mu (X `&` ~` A).
Expand Down Expand Up @@ -3576,7 +3607,7 @@ Notation "mu .-cara.-measurable" :=

Section caratheodory_measure.
Variables (R : realType) (T : pointedType).
Variable (mu : {outer_measure set T -> \bar R}).
Variable mu : {outer_measure set T -> \bar R}.
Let U := caratheodory_type mu.

Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
Expand Down