Skip to content

generalized measurable_ln #1602

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

Merged
affeldt-aist merged 1 commit into from
May 1, 2025
Merged

generalized measurable_ln #1602

Show file tree
Hide file tree
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
29 changes: 24 additions & 5 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,12 @@
- in `functions.v`:
+ lemma `natmulfctE`

- in `ereal.v`:
+ lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN`
+ lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`,
`ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`,
`ereal_sup_real`, `ereal_inf_real`

### Changed

- in `pi_irrational`:
Expand Down Expand Up @@ -79,11 +85,9 @@
- in `functions.v`:
+ `fct_sumE`, `addrfctE`, `sumrfctE` (from `zmodType` to `nmodType`)
+ `scalerfctE` (from `pointedType` to `Type`)
- in `ereal.v`:
+ lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN`
+ lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`,
`ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`,
`ereal_sup_real`, `ereal_inf_real`

- in `measurable_realfun.v`
+ lemma `measurable_ln`

### Deprecated

Expand All @@ -92,6 +96,21 @@
- in `functions.v`:
+ definitions `fct_ringMixin`, `fct_ringMixin` (was only used in an `HB.instance`)

- in `measurable_realfun.v`:
+ notation `measurable_fun_ln` (deprecated since 0.6.3)
+ notations `emeasurable_itv_bnd_pinfty`, `emeasurable_itv_ninfty_bnd` (deprecated since 0.6.2)
+ notation `measurable_fun_lim_sup` (deprecated since 0.6.6)
+ notation `measurable_fun_max` (deprecated since 0.6.3)
+ notation `measurable_fun_er_map` (deprecated since 0.6.3)
+ notations `emeasurable_funN`, `emeasurable_fun_max`, `emeasurable_fun_min`,
`emeasurable_fun_funepos`, `emeasurable_fun_funeneg` (deprecated since 0.6.3)
+ notation `measurable_fun_lim_esup` (deprecated since 0.6.6)

- in `measure.v`:
+ notation `measurable_fun_ext` (deprecated since 0.6.2)
+ notations `measurable_fun_id`, `measurable_fun_cst`, `measurable_fun_comp` (deprecated since 0.6.3)
+ notation `measurable_funT_comp` (deprecated since 0.6.3)

### Infrastructure

### Misc
45 changes: 7 additions & 38 deletions theories/measurable_realfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,10 +391,6 @@ Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1|
apply: emeasurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_bnd_pinfty := emeasurable_itv (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")]
Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing).

Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D ->
measurable_fun D fine.
Expand Down Expand Up @@ -1125,27 +1121,20 @@ by rewrite -[_ @^-1` _]setTI; exact: m1.
Qed.

End measurable_fun_realType.
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")]
Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing).

Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R).
Lemma measurable_ln (R : realType) : measurable_fun [set: R] (@ln R).
Proof.
rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first.
by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=;
rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP].
rewrite -set_itvNyy (@itv_bndbnd_setU _ _ _ (BRight 0))//.
apply/measurable_funU => //; split.
- apply/measurable_restrictT => //=.
rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE.
by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW.
- have : {in `]0, +oo[%classic, continuous (@ln R)}.
by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln.
rewrite -continuous_open_subspace; last exact: interval_open.
by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv.
- apply: subspace_continuous_measurable_fun => //.
rewrite continuous_open_subspace; last exact: interval_open.
by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln.
Qed.
#[global] Hint Extern 0 (measurable_fun _ (@ln _)) =>
solve [apply: measurable_ln] : core.
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_ln` instead")]
Notation measurable_fun_ln := measurable_ln (only parsing).

Lemma measurable_expR (R : realType) : measurable_fun [set: R] expR.
Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed.
Expand All @@ -1170,13 +1159,11 @@ Notation measurable_fun_pow := measurable_funX (only parsing).

Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p).
Proof.
apply: measurable_fun_if => //.
apply: measurable_fun_ifT => //.
- apply: (measurable_fun_bool true).
rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//.
by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx.
- rewrite setTI; apply: measurableT_comp => //.
rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp.
by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP.
- by apply: measurableT_comp => //; exact: measurable_funM.
Qed.
#[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) =>
solve [apply: measurable_powR] : core.
Expand All @@ -1192,9 +1179,6 @@ rewrite /powR; apply: measurable_fun_if => //.
exact: mulrr_measurable.
Qed.

#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")]
Notation measurable_fun_max := measurable_maxr (only parsing).

Module NGenCInfty.
Section ngencinfty.
Implicit Types x y z : nat.
Expand Down Expand Up @@ -1457,8 +1441,6 @@ apply: measurable_fun_ifT => //=.
+ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num.
+ exact/measurable_EFinP/measurableT_comp.
Qed.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")]
Notation measurable_fun_er_map := measurable_er_map (only parsing).

Section emeasurable_fun.
Local Open Scope ereal_scope.
Expand Down Expand Up @@ -1547,19 +1529,6 @@ Qed.
End emeasurable_fun.
Arguments emeasurable_fun_cvg {d T R D} f_.

#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurableT_comp` instead")]
Notation emeasurable_funN := measurableT_comp (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")]
Notation emeasurable_fun_max := measurable_maxe (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mine` instead")]
Notation emeasurable_fun_min := measurable_mine (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")]
Notation emeasurable_fun_funepos := measurable_funepos (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funeneg` instead")]
Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")]
Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing).

Section open_itv_cover.
Context {R : realType}.
Implicit Types (A : set R).
Expand Down
10 changes: 0 additions & 10 deletions theories/measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1589,14 +1589,6 @@ End measurable_fun.
solve [apply: measurable_id] : core.
Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}.
#[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")]
Notation measurable_fun_ext := eq_measurable_fun (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")]
Notation measurable_fun_id := measurable_id (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_cst`")]
Notation measurable_fun_cst := measurable_cst (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_comp`")]
Notation measurable_fun_comp := measurable_comp (only parsing).

Section measurable_fun_measurableType.
Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2)
Expand Down Expand Up @@ -1708,8 +1700,6 @@ End measurable_fun_measurableType.
solve [apply: measurable_id] : core.
Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_bool {d1 T1 D f} b.
#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurableT_comp`")]
Notation measurable_funT_comp := measurableT_comp (only parsing).

Section measurability.

Expand Down
Loading