Skip to content

generalized measurable_fun_itv_(bndo_bndc/obnd_cbnd) #1662

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 2 commits into from
Aug 13, 2025
Merged

generalized measurable_fun_itv_(bndo_bndc/obnd_cbnd) #1662

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
2ac5979
fix
IshiguroYoshihiro Jul 1, 2025
1a91f3a
fix
affeldt-aist Aug 13, 2025
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
5 changes: 5 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,11 @@
- in `constructive_ereal.v`:
+ lemma `mulN1e`

- in `measurable_realfun.v`:
+ generalized and renamed:
* `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP`
* `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP`

### Renamed

- in `lebesgue_stieltjes_measure.v`:
Expand Down
10 changes: 5 additions & 5 deletions theories/ftc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -684,7 +684,7 @@ transitivity (\sum_(0 <= i <oo) ((F (a + i.+1%:R))%:E - (F (a + i%:R))%:E)).
by rewrite lee_fin; exact: f_ge0.
apply: eq_eseriesr => n _.
rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
apply: measurable_fun_itv_bndo_bndc.
apply/measurable_fun_itv_bndo_bndcP.
apply: open_continuous_measurable_fun => //.
move: cf => /continuous_within_itvcyP[cf _] x.
rewrite inE/= in_itv/= => /andP[anx _].
Expand Down Expand Up @@ -1284,12 +1284,12 @@ Proof.
move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo].
move=> [dF cFa] Fny /continuous_within_itvNycP[cG cGFa] G0.
have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G.
apply: measurable_fun_itv_bndo_bndc.
apply/measurable_fun_itv_bndo_bndcP.
apply: open_continuous_measurable_fun; first exact: interval_open.
move=> x; rewrite inE/= in_itv/= => /andP[_ xFa].
by apply: cG; rewrite in_itv.
have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R.
apply: measurable_fun_itv_obnd_cbnd.
apply/measurable_fun_itv_obnd_cbndP.
apply: open_continuous_measurable_fun; first exact: interval_open.
move=> x; rewrite inE/= in_itv/= => /andP[ax _].
apply: continuousM; last first.
Expand Down Expand Up @@ -1391,7 +1391,7 @@ transitivity (limn (fun n =>
apply: congr_lim; apply/funext => -[|n].
by rewrite addr0 set_itvco0 set_itvoo0 !integral_set0.
rewrite integral_itv_bndo_bndc; last first.
apply: measurable_fun_itv_obnd_cbnd; apply: measurable_funS (mG n) => //.
apply/measurable_fun_itv_obnd_cbndP; apply: measurable_funS (mG n) => //.
by apply: subset_itvl; rewrite bnd_simp.
rewrite integration_by_substitution_decreasing.
- rewrite integral_itv_bndo_bndc// ?integral_itv_obnd_cbnd//.
Expand Down Expand Up @@ -1683,7 +1683,7 @@ rewrite -[RHS]integral_itv_obnd_cbnd; last first.
apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=.
rewrite opp_itv_bndy opprK/=.
by apply: subset_itvl; rewrite bnd_simp.
apply: measurable_fun_itv_bndo_bndc; apply: measurable_funM => //.
apply/measurable_fun_itv_bndo_bndcP; apply: measurable_funM => //.
- apply: (@measurable_comp _ _ _ _ _ _ `]-oo, F b[) => //=.
move=> x/= [r]; rewrite in_itv/= => rb <-{x}.
by rewrite in_itv/= ndF ?in_itv//= ltW.
Expand Down
2 changes: 1 addition & 1 deletion theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1541,7 +1541,7 @@ have [xy|yx _|-> _] := ltgtP x y; last 2 first.
move=> mf.
transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E).
case: b1 => //; rewrite -integral_itv_bndo_bndc//.
by case: b0 => //; exact: measurable_fun_itv_obnd_cbnd.
by case: b0 => //; exact/measurable_fun_itv_obnd_cbndP.
by case: b0 => //; rewrite -integral_itv_obnd_cbnd.
Qed.

Expand Down
59 changes: 26 additions & 33 deletions theories/measurable_realfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,37 +183,30 @@ End puncture_ereal_itv.
Section salgebra_R_ssets.
Variable R : realType.

Lemma measurable_fun_itv_bndo_bndc (a : itv_bound R) (b : R)
(f : R -> R) :
measurable_fun [set` Interval a (BLeft b)] f ->
Lemma measurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> R) :
measurable_fun [set` Interval a (BLeft b)] f <->
measurable_fun [set` Interval a (BRight b)] f.
Proof.
have [ab|ab] := leP a (BLeft b).
- move: a => [a0 a|[|//]] in ab *;
move=> mf; rewrite -setUitv1//; apply/measurable_funU => //;
by split => //; exact: measurable_fun_set1.
- move: a => [[|] a|[|]//] in ab *; rewrite bnd_simp in ab.
+ move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//.
exact: measurable_fun_set0.
+ move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//.
exact: measurable_fun_set0.
split; [have [ab ?|ab _] := leP a (BLeft b) |have [ab _|ab] := leP (BLeft b) a].
- rewrite -setUitv1//; apply/measurable_funU => //; split => //.
exact: measurable_fun_set1.
- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
- by rewrite -setUitv1 ?ltW// => /measurable_funU[].
Qed.

Lemma measurable_fun_itv_obnd_cbnd (a : R) (b : itv_bound R)
(f : R -> R) :
measurable_fun [set` Interval (BRight a) b] f ->
Lemma measurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> R) :
measurable_fun [set` Interval (BRight a) b] f <->
measurable_fun [set` Interval (BLeft a) b] f.
Proof.
have [ab|ab] := leP (BRight a) b.
- move: b => [[|] b|[//|]] in ab *;
move=> mf; rewrite -setU1itv//; apply/measurable_funU => //;
by split => //; exact: measurable_fun_set1.
- move: b => [[|] b|[|//]] in ab *; rewrite bnd_simp in ab.
+ move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//.
exact: measurable_fun_set0.
+ move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//.
exact: measurable_fun_set0.
+ by move=> _; rewrite set_itv_ge//=; exact: measurable_fun_set0.
split; [have [ab mf|ab _] := leP (BRight a) b|
have [ab _|ab] := leP b (BRight a)].
- rewrite -setU1itv//; apply/measurable_funU => //; split => //.
exact: measurable_fun_set1.
- rewrite set_itv_ge; first exact: measurable_fun_set0.
by rewrite -leNgt; case: b ab => -[].
- by rewrite set_itv_ge// -?leNgt//; exact: measurable_fun_set0.
- by rewrite -setU1itv ?ltW// => /measurable_funU[].
Qed.

#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")]
Expand All @@ -223,9 +216,9 @@ Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) :
Proof.
move: b0 b1 => [|] [|]//.
- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
- exact: measurable_fun_itv_obnd_cbnd.
- by move/measurable_fun_itv_obnd_cbndP.
- move=> mf.
have : measurable_fun `[x, y] f by exact: measurable_fun_itv_obnd_cbnd.
have : measurable_fun `[x, y] f by exact/measurable_fun_itv_obnd_cbndP.
by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
Qed.

Expand All @@ -236,22 +229,22 @@ Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) :
Proof.
move: b0 b1 => [|] [|]//.
- move=> mf.
have : measurable_fun `[x, y] f by exact: measurable_fun_itv_bndo_bndc.
have : measurable_fun `[x, y] f by exact/measurable_fun_itv_bndo_bndcP.
by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
- exact: measurable_fun_itv_bndo_bndc.
- by move/measurable_fun_itv_bndo_bndcP.
Qed.

Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) :
measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
measurable_fun `[x, y] f.
Proof.
move: b0 b1 => [|] [|]//.
- exact: measurable_fun_itv_bndo_bndc.
- by move/measurable_fun_itv_bndo_bndcP.
- move=> mf.
have : measurable_fun `[x, y[ f by exact: measurable_fun_itv_obnd_cbnd.
exact: measurable_fun_itv_bndo_bndc.
- exact: measurable_fun_itv_obnd_cbnd.
have : measurable_fun `[x, y[ f by exact/measurable_fun_itv_obnd_cbndP.
by move/measurable_fun_itv_bndo_bndcP.
- by move/measurable_fun_itv_obnd_cbndP.
Qed.

HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)).
Expand Down