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

minor edits #50

Merged
merged 1 commit into from
Jul 16, 2024
Merged

minor edits #50

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
135 changes: 75 additions & 60 deletions theories/absolute_continuity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1709,8 +1709,10 @@ exists U_, Z; split.
exact: subIsetl.
by rewrite (le_lt_trans (mueS0E _))// ltry.
+ move=> i.
admit.
+ admit.
apply: measurableD.
by apply: open_measurable.
admit. (* measurable E *)
+ admit. (* measurable E *)
+ move=> m n mn.
apply/subsetPset; apply: setSD => x H k h.
apply: H => //.
Expand Down Expand Up @@ -1775,6 +1777,7 @@ Fail Lemma lusinN_total_variation a b f : abs_contN a b f ->

Lemma abs_contN_dominates a b (f : cumulative R) : abs_contN a b f ->
mu `<< lebesgue_stieltjes_measure f.
Proof.
Abort.

Fail Lemma differentiable_lusinN a b f : {in `]a, b[%classic, differentiable f} ->
Expand Down Expand Up @@ -3081,51 +3084,6 @@ Qed.
(* admit. *)
(* by apply: sub_Rhullr. *)

(* a wlog part in image_measure0_Lusin *)
Lemma image_measure0_Lusin'
(f : R -> R)
(cf : {within `[a, b], continuous f})
(ndf : {in `[a, b] &, {homo f : x y / x <= y}})
(HZ : forall Z : set R,
Z `<=` `[a, b] -> compact Z -> mu Z = 0 -> mu [set f x | x in Z] = 0)
(Z : set R)
(Zab : Z `<=` `[a, b])
(mZ : (((wlength idfun)^*)%mu).-cara.-measurable Z)
(muZ0 : mu Z = 0)
(muFZ0 : (0%R < mu [set f x | x in Z])%E)
(GdeltaZ : Gdelta Z) : False.
Proof.
(* lemma *)
have ndf' : {in `[a, b]%classic &, {homo f : n m / n <= m}}.
move=> x y.
rewrite !inE/= => xab yab.
exact: ndf.
have mfZ : measurable (f @` Z).
have set_fun_f : set_fun `[a, b] [set: R] f by [].
pose Hf := isFun.Build R R `[a, b]%classic [set: R] f set_fun_f.
pose F : {fun `[a, b] >-> [set: R]} := HB.pack f Hf.
simpl in F.
have := @measurable_image_delta_set_nondecreasing_fun R a b F ab ndf cf Z.
apply => //.
admit. (* ?! *)
have mfZ_gt0 : (0 < mu (f @` Z))%E.
done.
have [K [cK KfZ muK]] : exists K, [/\ compact K, K `<=` f @` Z & (0 < mu K)%E].
have /= := lebesgue_regularity_inner mfZ.
admit.
pose K1 := (f @^-1` K) `&` `[a, b].
have cK1 : compact K1.
(* using continuity, continuous_compact? *)
admit.
have K1ab : K1 `<=` `[a, b].
admit.
have K1Z : K1 `<=` Z.
admit.
have fK1K : f @` K1 = K.
admit.
have := HZ K1 K1ab cK1.
Admitted.

(* lemma3 (converse) *)
Lemma image_measure0_Lusin (f : R -> R) :
{within `[a, b], continuous f} ->
Expand All @@ -3139,13 +3097,42 @@ Proof.
move=> cf ndf HZ; apply: contrapT.
move=> /existsNP[Z]/not_implyP[Zab/=] /not_implyP[mZ] /not_implyP[muZ0].
move=> /eqP; rewrite neq_lt ltNge measure_ge0/= => muFZ0.
have lmZ : lebesgue_measurability Z.
wlog : Z Zab mZ muZ0 muFZ0 / Gdelta Z.
move=> wlg.
have [Z1 [gdZ1 mZ10 ZZ1]] : exists Z1, [/\ Gdelta Z1, mu Z1 = 0 & Z `<=` Z1].
admit.
have mFZ1 : (0 < (((wlength idfun)^*)%mu) (f @` Z1))%E.
admit.
apply: (wlg Z1) => //.
admit.
admit.
move=> gdZ.
have mFZ : measurable (f @` Z).
admit.
have muF0_gt0 : (0 < mu (f @` Z))%E.
admit.
have [K [cK KfZ muK]] : exists K, [/\ compact K, K `<=` f @` Z & (0 < mu K)%E].
(* have /= := lebesgue_regularity_inner mfZ.*)
admit.
pose K1 := (f @^-1` K) `&` `[a, b].
have cK1 : compact K1.
(* using continuity, continuous_compact? *)
admit.
have K1ab : K1 `<=` `[a, b].
admit.
have K1Z : K1 `<=` Z.
admit.
have fK1K : f @` K1 = K.
admit.
have := HZ K1 K1ab cK1.
rewrite fK1K.
(*have lmZ : lebesgue_measurability Z.
move=> e e0.
have [U [oU ZU /andP[muZU muUZe]]] := outer_regularity_outer0 Z e0.
exists U; split => //.
rewrite -(@leeD2lE _ (((wlength idfun)^*)%mu (U `&` Z))); last first.
rewrite -(@leeD2lE _ (((wlength idfun)^* )%mu (U `&` Z))); last first.
rewrite ge0_fin_numE; last exact: outer_measure_ge0.
apply: (@le_lt_trans _ _ (((wlength idfun)^*)%mu `[a, b]%classic)).
apply: (@le_lt_trans _ _ (((wlength idfun)^* )%mu `[a, b]%classic)).
apply: le_outer_measure.
by rewrite setIidr.
rewrite [ltLHS](_:_= lebesgue_measure `[a, b]%classic); last by [].
Expand All @@ -3168,7 +3155,7 @@ apply.
exact: open_measurable.
- admit.
- admit.
- by exists H.
- by exists H.*)
Admitted.

End lemma3.
Expand Down Expand Up @@ -3224,17 +3211,45 @@ Lemma Lusin_total_variation (f : R -> R) :
lusinN `[a, b] (fun x => fine (total_variation a ^~ f x)).
Proof.
move=> cf bvf lf.
have ndt := @total_variation_nondecreasing R a b f.
have ct := total_variation_continuous ab cf bvf.
apply: image_measure0_Lusin => //.
apply: contrapT.
move=> H.
pose H := fun x => fine (total_variation a ^~ f x).
have ndt : {in `[a, b] &, nondecreasing_fun H}.
move=> x y xab yab xy.
have axyf := @total_variation_nondecreasing R a b f _ _ xab yab xy.
rewrite /H fine_le//.
- apply/bounded_variationP => //.
by move: xab; rewrite in_itv/= => /andP[].
move: xab; rewrite in_itv/= => /andP[? ?].
by move: bvf; apply: bounded_variationl.
- apply/bounded_variationP => //.
by move: yab; rewrite in_itv/= => /andP[].
move: yab; rewrite in_itv/= => /andP[? ?].
by move: bvf; apply: bounded_variationl.
have cH : {within `[a, b], continuous H}.
exact: total_variation_continuous.
apply: contrapT => ababsurdo.
have := image_measure0_Lusin ab cH ndt.
move/contra_not => /(_ ababsurdo).
move/existsNP => [Z /not_implyP [Zab /not_implyP[cZ /not_implyP[muZ0]]]].
move/eqP; rewrite neq_lt ltNge measure_ge0/= => muHZ_gt0.
have compactH : compact (H @` Z).
have := @continuous_compact _ _ H Z.
apply.
apply: continuous_subspaceW.
exact: Zab.
assumption.
exact: cZ.
pose c : R := inf Z.
pose d : R := sup Z.
wlog : Z Zab cZ muZ0 muHZ_gt0 compactH c d / perfect_set Z.
admit.
move=> perfectZ.

pose TV := (fine \o (total_variation a)^~ f).
have : exists n : nat, (0 < n)%N /\ exists Z_ : `I_ n -> interval R, trivIset setT (fun i => [set` (Z_ i)])
/\ (0 < mu (TV @` (\bigcup_i [set` Z_ i])))%E
/\ forall i, [/\ [set` Z_ i] `<=` `[a, b], compact [set` Z_ i] & mu [set` Z_ i] = 0].
admit.
move=> [n [] n0 [Z_]] [trivZ [Uz0]] /all_and3 [Zab cZ Z0].
move=> [n [] n0 [Z_]] [trivZ [Uz0]] /all_and3 [Zab' cZ' Z0].
pose UZ := \bigcup_i [set` Z_ i].
have UZ_not_empty : UZ !=set0.
admit.
Expand Down Expand Up @@ -3964,15 +3979,15 @@ Theorem Banach_Zarecki (f : R -> R) :
abs_cont a b f.
Proof.
move=> cf bvf Lf.
apply: total_variation_AC => //.
apply: Banach_Zarecki_nondecreasing => //.
apply: total_variation_AC => //. (* lemma 8 *)
apply: Banach_Zarecki_nondecreasing => //. (* lemma 7 *)
- exact: total_variation_continuous.
- move=> x y; rewrite !in_itv /= => /andP[ax xb] /andP[ay yb] xy.
apply: fine_le.
+ apply/(bounded_variationP _ ax); exact:(bounded_variationl _ xb).
+ apply/(bounded_variationP _ ay); exact:(bounded_variationl _ yb).
+ by apply: (@total_variation_nondecreasing _ _ b); rewrite ?in_itv /= ?ax ?ay.
- exact: Lusin_total_variation.
- exact: Lusin_total_variation. (* lemma 6 *)
Qed.

End banach_zarecki.
Loading