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

missing lemmas about ereal #1264

Merged
merged 9 commits into from
Jul 25, 2024
Merged

missing lemmas about ereal #1264

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
b60f80b
missing lemmas about ereal
affeldt-aist Jul 22, 2024
3b4ffb3
dual variants
affeldt-aist Jul 23, 2024
1d880b7
renaming in dual variants
affeldt-aist Jul 23, 2024
167f766
more renamings
affeldt-aist Jul 24, 2024
d8fde79
minor gen
affeldt-aist Jul 24, 2024
0675c3e
Update CHANGELOG_UNRELEASED.md
affeldt-aist Jul 24, 2024
b85f23b
Update CHANGELOG_UNRELEASED.md
affeldt-aist Jul 24, 2024
a653f94
Update CHANGELOG_UNRELEASED.md
affeldt-aist Jul 24, 2024
83bb193
Update CHANGELOG_UNRELEASED.md
affeldt-aist Jul 24, 2024
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
3 changes: 3 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,9 @@
- in `realfun.v`:
+ lemma `nondecreasing_at_left_is_cvgr`

- in `constructive_ereal.v`:
+ lemmas `lteD2rE`, `leeD2rE`

### Changed

- in `topology.v`:
Expand Down
6 changes: 6 additions & 0 deletions theories/constructive_ereal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1783,6 +1783,9 @@ move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(ltry, ltNyr)//.
by rewrite !lte_fin ltrD2l.
Qed.

Lemma lteD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b).
Proof. by rewrite -!(addeC x); exact: lteD2lE. Qed.

Lemma leeD2l x a b : a <= b -> x + a <= x + b.
Proof.
move: a b x => -[a [b [x /=|//|//] | []// |//] | []// | ].
Expand All @@ -1797,6 +1800,9 @@ move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(leey, leNye)//.
by rewrite !lee_fin lerD2l.
Qed.

Lemma leeD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b).
Proof. by rewrite -!(addeC x); exact: leeD2lE. Qed.

Lemma leeD2r x a b : a <= b -> a + x <= b + x.
Proof. rewrite addeC (addeC b); exact: leeD2l. Qed.

Expand Down
6 changes: 2 additions & 4 deletions theories/lebesgue_measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2224,11 +2224,9 @@ move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD.
rewrite (@le_trans _ _ (mu V))//; last first.
apply: ereal_sup_ub; exists V => //=; split => //.
exact: (subset_trans VFND (@subIsetr _ _ _)).
rewrite -(@leeD2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//.
rewrite -(@leeD2rE _ 1)// -EFinD (le_trans M1FD)//.
rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI.
rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first.
by rewrite measureIr//; apply: measurableI.
by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI.
by rewrite addeC leeD//; [rewrite measureIr//; exact: measurableI|exact/ltW].
Qed.

End lebesgue_regularity.
Expand Down
3 changes: 1 addition & 2 deletions theories/realfun.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2358,8 +2358,7 @@ rewrite {1}variation_prev; last exact: itv_partition1.
rewrite /= -addeA -lteBrDr; last by rewrite fin_numD; apply/andP.
rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA.
move/lt_trans; apply.
rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lteD2lE //.
rewrite -addeA.
rewrite [in ltRHS](splitr (eps%:num)) EFinD lteD2rE// -addeA.
apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E).
rewrite [in leRHS]variation_prev; last exact: itv_partition1.
rewrite geeDl// sube_le0; apply: ereal_sup_ub => /=.
Expand Down
Loading