Skip to content

Commit

Permalink
vitali lemma finite case
Browse files Browse the repository at this point in the history 
- test with different Zorn statement
- minor cleaning
  • Loading branch information
@affeldt-aist
affeldt-aist committed Jul 19, 2023
1 parent 6094827 commit f2a57df
Showing 1 changed file with 180 additions and 30 deletions.
210 changes: 180 additions & 30 deletions theories/lebesgue_measure.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2110,28 +2110,35 @@ End egorov.
(* PR in progress *)
(* NB: turning P into set (set I) and T := P does not improve much *)
Section Zorn_subset.
Variables (T : Type) (P : set T -> Prop).
Let sigP := {x | P x}.
Let R (sA sB : sigP) := sval sA `<=` sval sB.
Variables (T : Type) (P : set (set T)).

Lemma Zorn_bigcup :
(forall F, total_on F R -> P (\bigcup_(x in F) sval x)) ->
(forall F : set (set T), F `<=` P -> total_on F subset ->
P (\bigcup_(X in F) X)) ->
exists A, P A /\ forall B, A `<` B -> ~ P B.
Proof.
move=> totR.
have {}totR F : total_on F R -> exists sB, forall sA, F sA -> R sA sB.
by move=> FR; exists (exist _ _ (totR _ FR)) => sA FsA; exact: bigcup_sup.
move=> totP; pose R (sA sB : P) := sval sA `<=` sval sB.
have {}totR F (FR : total_on F R) : exists sB, forall sA, F sA -> R sA sB.
have FP : [set val x | x in F] `<=` P.
by move=> _ [X FX <-]; apply: set_mem; apply: valP.
have totF : total_on [set val x | x in F] subset.
by move=> _ _ [X FX <-] [Y FY <-]; apply: FR.
exists (SigSub (mem_set (totP _ FP totF))) => A FA; rewrite /R/=.
exact: (bigcup_sup (imageP val _)).
have [| | |sA sAmax] := Zorn _ _ _ totR.
- by move=> ?; exact: subset_refl.
- by move=> ? ? ?; exact: subset_trans.
- by move=> [A PA] [B PB]; rewrite /R /= => AB BA; exact/eq_exist/seteqP.
- exists (sval sA); case: sA => A PA in sAmax *; split => //= B AB PB.
have [BA] := sAmax (exist _ B PB) (properW AB).
- exists (val sA); case: sA => A PA /= in sAmax *; split; first exact: set_mem.
move=> B AB PB; have [BA] := sAmax (SigSub (mem_set PB)) (properW AB).
by move: AB; rewrite BA; exact: properxx.
Qed.

End Zorn_subset.

Lemma mkset_set (T : eqType) (x : T) : [set` [:: x]] = [set x].
Proof. by apply/seteqP; split => y /=; rewrite ?inE => /eqP. Qed.

Section ball_extra.
Variable R : realType.

Expand All @@ -2155,6 +2162,19 @@ rewrite lte_fin ltr_subl_addr -addrA ltr_addl addr_gt0 //.
by rewrite -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n.
Qed.

Lemma closed_ball_itv (x r : R) : 0 < r ->
(closed_ball x r = `[x - r, x + r]%classic)%R.
Proof.
move=> r0.
by apply/seteqP; split => y; rewrite (@closed_ballE _ [normedModType R of R^o])//;
rewrite /closed_ball_ /= in_itv/= ler_distlC.
Qed.

Lemma measurable_closed_ball (x : R^o) r : 0 < r -> measurable (closed_ball x r).
Proof.
by move=> r0; rewrite closed_ball_itv.
Qed.

End ball_extra.

Section scale_ball.
Expand All @@ -2163,6 +2183,22 @@ Variable R : realType.
Definition scale_ball k (c : R * {posnum R}) :=
ball c.1 (k * c.2%:num).

Lemma scale_ball1 (c : R * {posnum R}) :
scale_ball 1 c = ball c.1 c.2%:num.
Proof. by rewrite /scale_ball mul1r. Qed.

Lemma scale_ball_neq0 k (c : R * {posnum R}) : 0 < k -> scale_ball k c !=set0.
Proof.
by exists c.1; rewrite /= /scale_ball /ball /= subrr normr0 mulr_gt0.
Qed.

Lemma sub_scale_ball k l (c : R * {posnum R}) :
k <= l -> scale_ball k c `<=` scale_ball l c.
Proof.
move=> kl x; rewrite /scale_ball /ball/= => /lt_le_trans; apply.
by rewrite ler_wpmul2r.
Qed.

Definition scale_cball k (c : R * {posnum R}) :=
[set x | `|c.1 - x| <= k * c.2%:num].

Expand All @@ -2172,9 +2208,18 @@ by apply/seteqP; split => // x;
rewrite /scale_cball/= mul0r normr_le0 subr_eq0 eq_sym => /eqP.
Qed.

Lemma scale_cball1 c : scale_cball 1 c = [set x | `|c.1 - x| <= c.2%:num].
Proof. by rewrite /scale_cball mul1r. Qed.

Lemma scale_cball_neq0 k (c : R * {posnum R}) : 0 <= k -> scale_cball k c !=set0.
Proof. by exists c.1; rewrite /= /scale_cball /= subrr normr0 mulr_ge0. Qed.

Lemma scale_cball_itv k c :
(scale_cball k c = `[c.1 - k * c.2%:num, c.1 + k * c.2%:num]%classic)%R.
Proof.
by apply/seteqP; split => y; rewrite /scale_cball/= in_itv/= ler_distlC.
Qed.

Lemma trivIset_bigcup_scale_cball (I : Type) (B : I -> R * {posnum R})
(D : nat -> set I) k :
(forall n, trivIset (D n) (scale_cball k \o B)) ->
Expand All @@ -2187,10 +2232,6 @@ have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm.
exact: (H _ _ _ _ nm).
Qed.

Lemma scale_cball_itv k c :
(scale_cball k c = `[c.1 - k * c.2%:num, c.1 + k * c.2%:num]%classic)%R.
Proof. by apply/seteqP; split => y; rewrite /scale_cball/= in_itv/= ler_distlC. Qed.

Lemma interior_scale_cball_neq0 (B : R * {posnum R}) k : 0 < k ->
(scale_cball k B)^° !=set0.
Proof.
Expand All @@ -2205,7 +2246,7 @@ Qed.
Lemma measurable_scale_cball k c : measurable (scale_cball k c).
Proof. by rewrite scale_cball_itv; exact: measurable_itv. Qed.

Lemma measure_scale_cballE k c : 0 <= k ->
Lemma lebesgue_measure_scale_cballE k c : 0 <= k ->
lebesgue_measure (scale_cball k c) = (k%:E * ((c.2)%:num *+ 2)%:E)%E.
Proof.
rewrite le_eqVlt => /predU1P[<-|].
Expand All @@ -2217,9 +2258,10 @@ rewrite -EFinD; congr (_%:E).
by rewrite opprB addrAC addrCA subrr addr0 -mulrDr -mulr2n.
Qed.

Lemma measure_scale_cball k c : 0 <= k ->
lebesgue_measure (scale_cball k c) = (k%:E * lebesgue_measure (scale_cball 1 c))%E.
Proof. by move=> k0; rewrite !measure_scale_cballE// mul1e. Qed.
Lemma lebesgue_measure_scale_cball k c : 0 <= k ->
lebesgue_measure (scale_cball k c) =
(k%:E * lebesgue_measure (scale_cball 1 c))%E.
Proof. by move=> k0; rewrite !lebesgue_measure_scale_cballE// mul1e. Qed.

(* NB: this can be generalized *)
Lemma separated_countable (I : Type) (B : I -> R * {posnum R})
Expand Down Expand Up @@ -2258,15 +2300,14 @@ Definition maximal_disjoint_subcollection (E D : set I) :=
Variable D : set I.

Let P := fun X => X `<=` D /\ trivIset X (scale_cball 1 \o B).
Let T := {x : set I | P x}.

Let H (A : set T) :
total_on A (fun x y => sval x `<=` sval y) -> P (\bigcup_(x in A) sval x).
Let H (A : set (set I)) :
A `<=` P -> total_on A (fun x y => x `<=` y) -> P (\bigcup_(x in A) x).
Proof.
move=> h; split; first by apply: bigcup_sub => -[E [/=]].
move=> AP h; split; first by apply: bigcup_sub => E /AP [].
move=> i j [x Ax] xi [y Ay] yj ij; have [xy|yx] := h _ _ Ax Ay.
- by apply: (svalP y).2 => //; exact: xy.
- by apply: (svalP x).2 => //; exact: yx.
- by apply: (AP _ Ay).2 => //; exact: xy.
- by apply: (AP _ Ax).2 => //; exact: yx.
Qed.

Lemma ex_maximal_disjoint : { E | maximal_disjoint_subcollection E D }.
Expand Down Expand Up @@ -2297,10 +2338,12 @@ Definition collection_partition n :=

Hypothesis VBr : forall i, V i -> (B i).2%:num <= r.

Lemma r_gt0 i0 : V i0 -> 0 < r.
Proof. move=> Vi0; by rewrite (lt_le_trans _ (VBr Vi0)). Qed.
Lemma collection_partition_ub_gt0 i : V i -> 0 < r.
Proof. move=> Vi; by rewrite (lt_le_trans _ (VBr Vi)). Qed.

Notation r_gt0 := collection_partition_ub_gt0.

Lemma ex_collection_partition (i : I) : V i -> exists n, (collection_partition n) i.
Lemma ex_collection_partition i : V i -> exists n, (collection_partition n) i.
Proof.
move=> Vi; pose f := floor (r / ((B i).2)%:num).
have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi).
Expand Down Expand Up @@ -2470,7 +2513,7 @@ have Bjrn : (B j).2%:num > r / (2 ^ n.+1)%:R.
have [+ _ _] := maxD m.
by move/(_ _ Dmk) => -[Bmk] _; exists m.
move/(_ _ Dj) => [m/= mn1] [_] /andP[+ _].
apply: le_lt_trans; rewrite ler_pmul2l//; last by rewrite (r_gt0 VBr Vi).
apply: le_lt_trans; rewrite ler_pmul2l ?(collection_partition_ub_gt0 VBr Vi)//.
by rewrite lef_pinv// ?posrE ?ltr0n ?expn_gt0// ler_nat leq_pexp2l.
exists j; split => //.
- by case: Dj => m /= mn Dm; exists m.
Expand All @@ -2480,11 +2523,11 @@ exists j; split => //.
apply: (@le_trans _ _ (2 * (B i).2%:num + (B j).2%:num)).
case: BiBj => y [Biy Bjy].
rewrite (le_trans (ler_dist_add y _ _))// [in leRHS]addrC ler_add//.
by move: Bjy; rewrite /scale_cball/= mul1r.
by move: Bjy; rewrite scale_cball1.
rewrite (le_trans (ler_dist_add (B i).1 _ _))//.
rewrite (_ : 2 = 1 + 1)// mulrDl !mul1r// ler_add//; last first.
by move: Bix; rewrite /scale_cball/= mul1r.
by move: Biy; rewrite /scale_cball/= mul1r distrC.
by move: Bix; rewrite scale_cball1.
by move: Biy; rewrite scale_cball1 distrC.
rewrite -ler_subr_addr// (_ : 5 = 4 + 1); last by rewrite natr1.
rewrite mulrDl mul1r addrK (_ : 4 = 2 * 2); last by rewrite -natrM.
rewrite -mulrA ler_pmul2l//.
Expand All @@ -2503,3 +2546,110 @@ by move/(_ _ cBix) => ?; exists j.
Qed.

End vitali_lemma.

Section vitali_lemma_finite.
Context {R : realType} {I : eqType}.
Variable (B : I -> R * {posnum R}).

Let LE x y := (B x).2%:num <= (B y).2%:num.

Let LE_trans : transitive LE. Proof. by move=> x y z; exact: le_trans. Qed.

Let vitali_lemma_finite_sorted (V : seq I) : sorted LE V ->
{ D : seq I | [/\
{subset D <= V}, trivIset [set` D] (scale_ball 1 \o B) &
forall i, i \in V -> exists j, [/\ j \in D,
scale_ball 1 (B i) `&` scale_ball 1 (B j) !=set0,
(B j).2%:num >= (B i).2%:num &
scale_ball 1 (B i) `<=` scale_ball 3 (B j)] ] }.
Proof.
elim: V => [_|a [_ /= _|h2 t]]; first by exists nil.
exists [:: a]; split => //=.
- by rewrite mkset_set; exact: trivIset1.
- move=> i; rewrite inE => /eqP <-{a}; exists i; split => //.
by rewrite mem_head.
by rewrite setIid; exact: scale_ball_neq0.
by apply: sub_scale_ball; rewrite ler1n.
set t' := h2 :: t.
rewrite /= => + /andP[h2h1 h2t].
move/(_ h2t) => [s [sh2t sB H]].
have [K|] := pselect (forall j, j \in s ->
scale_ball 1 (B j) `&` scale_ball 1 (B a) = set0).
exists (a :: s); split => //.
- move=> x; rewrite in_cons => /predU1P[->|].
by rewrite mem_head.
by move/sh2t => xt'; rewrite in_cons xt' orbT.
- move=> i j /=; rewrite inE => /predU1P[->{i}|si].
rewrite inE => /predU1P[->{j}//|js].
by move/set0P; rewrite setIC K// eqxx.
rewrite inE => /predU1P[->{j}//|js].
by move/set0P; rewrite K// eqxx.
exact: sB.
- move=> i.
rewrite in_cons => /orP[/eqP ->{i}|].
exists a; split => //.
by rewrite mem_head.
by rewrite setIid; exact: scale_ball_neq0.
by apply: sub_scale_ball; rewrite ler1n.
- move/H => [j [js ij0 ij i3j]].
exists j; split => //.
by rewrite in_cons js orbT.
move/existsNP/cid => [j /not_implyP[js /eqP/set0P jh10]].
exists s; split => //.
by move=> x /sh2t; rewrite inE => ->; rewrite orbT.
move=> i; rewrite in_cons => /predU1P[->{i}|/H//].
exists j; split => //.
- by rewrite setIC.
- rewrite (le_trans h2h1)//.
move/sh2t : js; rewrite inE => /predU1P[<-//|jt].
have /allP := order_path_min LE_trans h2t.
exact.
- case: jh10 => x [Bjx Bh1x] y.
rewrite scale_ball1 /ball /= => h1y.
rewrite /scale_ball /ball /=.
rewrite -(subrK x y).
rewrite -(addrC x).
rewrite opprD addrA opprB.
rewrite (le_lt_trans (ler_norm_add _ _))//.
rewrite -(subrK (B a).1 y).
rewrite (_ : 3 = 1 + 2)// mulrDl mul1r.
rewrite ltr_add//.
move: Bjx.
by rewrite /scale_ball /ball/= mul1r.
rewrite -(addrC (B a).1).
rewrite opprD addrA opprB.
rewrite (le_lt_trans (ler_norm_add _ _))//.
rewrite (_ : 2 = 1 + 1)// mulrDl mul1r.
rewrite distrC.
rewrite ltr_add//.
move: Bh1x.
rewrite scale_ball1 /ball /= => /lt_le_trans; apply.
rewrite (le_trans h2h1)//.
move/sh2t : js; rewrite inE => /predU1P[<-//|jt].
have /allP := order_path_min LE_trans h2t.
exact.
move: h1y => /lt_le_trans; apply.
rewrite (le_trans h2h1)//.
move/sh2t : js; rewrite inE => /predU1P[<-//|jt].
have /allP := order_path_min LE_trans h2t.
exact.
Qed.

Lemma vitali_lemma_finite (V : seq I) :
{ D : seq I | [/\
{subset D <= V}, trivIset [set` D] (scale_ball 1 \o B) &
forall i, i \in V -> exists j, [/\ j \in D,
scale_ball 1 (B i) `&` scale_ball 1 (B j) !=set0,
(B j).2%:num >= (B i).2%:num &
scale_ball 1 (B i) `<=` scale_ball 3 (B j)] ] }.
Proof.
have /vitali_lemma_finite_sorted : sorted LE (sort LE V).
by apply: sort_sorted => x y; exact: le_total.
move=> [D [DV tD H]]; exists D; split => //.
- by move=> x /DV; rewrite mem_sort.
move=> i.
have := H i.
by rewrite mem_sort => /[apply].
Qed.

End vitali_lemma_finite.

0 comments on commit f2a57df

Please sign in to comment.