Skip to content

Generalize integration_by_parts #1674

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

Open
IshiguroYoshihiro wants to merge 30 commits into
base: master
Choose a base branch
from
Open

Generalize integration_by_parts #1674

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
baacc90
rename and boolify some predicates for open intervals
t6s Jan 16, 2026
0f54bc5
address review comments
t6s Jan 17, 2026
4f05af6
revert experimental Arguments declaration
t6s Jan 17, 2026
18b1844
integration_by_party
IshiguroYoshihiro Jul 4, 2025
d26a120
upd and rebase
affeldt-aist Oct 30, 2025
40a6ae7
lint
affeldt-aist Oct 30, 2025
efdaef9
Update theories/ftc.v
affeldt-aist Nov 18, 2025
54169c7
Update theories/ftc.v
affeldt-aist Nov 18, 2025
cab4c34
Update theories/ftc.v
affeldt-aist Nov 18, 2025
19691fc
Update theories/ftc.v
affeldt-aist Nov 18, 2025
2aceefa
Update theories/ftc.v
affeldt-aist Nov 18, 2025
3dd463d
Update theories/ftc.v
affeldt-aist Nov 18, 2025
7a7219e
Update theories/ftc.v
affeldt-aist Nov 18, 2025
eee5752
Update theories/ftc.v
affeldt-aist Nov 18, 2025
2b184dd
Update theories/ftc.v
affeldt-aist Nov 18, 2025
dfffa60
Update theories/ftc.v
affeldt-aist Nov 18, 2025
e8112c2
Update theories/ftc.v
affeldt-aist Nov 18, 2025
87a0c25
Update theories/ftc.v
affeldt-aist Nov 18, 2025
a331e6f
Update theories/ftc.v
affeldt-aist Nov 18, 2025
12ea4b1
Update theories/ftc.v
affeldt-aist Nov 18, 2025
7e72396
Update theories/ftc.v
affeldt-aist Nov 18, 2025
680dde4
Update theories/ftc.v
affeldt-aist Nov 18, 2025
5421a87
Update theories/ftc.v
affeldt-aist Nov 18, 2025
6fbca0b
Update theories/ftc.v
affeldt-aist Nov 18, 2025
243a8ba
Update theories/realfun.v
affeldt-aist Nov 18, 2025
bb9c30e
fix
IshiguroYoshihiro Jan 9, 2026
efcc45d
minor fix
IshiguroYoshihiro Jan 9, 2026
f69b03a
wip cleaning Let
IshiguroYoshihiro Jan 13, 2026
21e23f2
prove admit
affeldt-aist Jan 13, 2026
3a69bde
rename: derivable_oy_continuous_bndN -> derivable_oy_RcontinuousN
t6s Jan 17, 2026
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
340 changes: 340 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop

Large diffs are not rendered by default.

34 changes: 34 additions & 0 deletions reals/real_interval.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,40 @@ Qed.

End itv_realDomainType.

(* generalization of
Copy link
Member

@t6s t6s Jan 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This lemma can be an instance of the monotonicity of the closure operator.

a < b -> `]a, b] `<=` `]r, +oo[ -> `[a, b] `<=` `[r, +oo[. *)
Lemma subset_itvoSo_cSc {R : realFieldType} (r a : R) (b x : itv_bound R) :
(BRight a < b)%O ->
(b <= x)%O ->
[set` Interval (BRight a)(*open*) b]
`<=` [set` Interval (BRight r)(*open*) x] ->
[set` Interval (BLeft a)(*closed*) b]
`<=` [set` Interval (BLeft r)(*closed*) x].
Proof.
move: b => [[|]b ab bx abrx|[//|/= _]]; rewrite ?bnd_simp.
- apply: subset_itv => //=; rewrite bnd_simp leNgt; apply/negP => ar.
have rb : (r <= b)%O.
rewrite leNgt; apply/negP => br; have /= := abrx ((a + b) / 2).
rewrite !in_itv/= !midf_lt//= => /(_ isT).
by rewrite ltNge (le_trans _ (ltW br))//= midf_le// ltW.
have /abrx /= : (a + r) / 2 \in `]a, b[.
by rewrite in_itv/= midf_lt//= (lt_le_trans _ rb)// midf_lt.
by rewrite in_itv/= ltNge midf_le// ltW.
- apply: subset_itv => //=; rewrite bnd_simp leNgt; apply/negP => ar.
have rb : r <= b.
rewrite leNgt; apply/negP => br; have /= := abrx ((a + b) / 2).
rewrite !in_itv/= midf_lt// (midf_le (ltW _))// => /(_ isT).
by rewrite ltNge (le_trans _ (ltW br))//= midf_le// ltW.
have /abrx /= : (a + r) / 2 \in `]a, b].
by rewrite in_itv/= midf_lt//= (le_trans _ rb)// (midf_le (ltW _)).
by rewrite in_itv/= ltNge midf_le// ltW.
- move/eqP => ->{x} ar.
apply/subset_itvr; rewrite bnd_simp leNgt; apply/negP => ra.
have /= := ar ((a + r) / 2).
rewrite !in_itv/= !andbT midf_lt// => /(_ isT).
by rewrite ltNge midf_le// ltW.
Qed.

Section set_ereal.
Context (R : realType) T (f g : T -> \bar R).
Local Open Scope ereal_scope.
Expand Down
4 changes: 2 additions & 2 deletions theories/charge.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1890,7 +1890,7 @@ have int_f_E j S : measurable S -> \int[mu]_(x in S) f_ j x = nu (S `&` E j).
have mSIEj := measurableI _ _ mS (mE j).
have mSDEj := measurableD mS (mE j).
rewrite -{1}(setUIDK S (E j)) (ge0_integral_setU _ mSIEj mSDEj)//; last 2 first.
- by rewrite setUIDK; exact: (measurable_funS measurableT).
- by rewrite setUIDK; exact: measurable_funTS.
- by apply/disj_set2P; rewrite setDE setIACA setICr setI0.
rewrite /f_ -(eq_integral _ (g_ j)); last first.
by move=> x /[!inE] SIEjx; rewrite /f_ ifT// inE; exact: (@subIsetr _ S).
Expand Down Expand Up @@ -2002,7 +2002,7 @@ have -> : \int[nu]_(x in E) f x =
under eq_integral => x /[!inE] /fE -> //.
apply: monotone_convergence => //.
- move=> n; apply/measurable_EFinP.
by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
by apply: measurable_funTS => //; exact/measurable_funP.
- by move=> n x Ex //=; rewrite lee_fin.
- by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
have -> : \int[mu]_(x in E) (f \* g) x =
Expand Down
Loading