Skip to content

gen ge0_integralZ{l,r} #2158

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
Nov 1, 2026
Merged

gen ge0_integralZ{l,r} #2158

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
41a6551
gen ge0_integralZ{l,r}
affeldt-aist Oct 31, 2026
ec6ecca
nitpick
affeldt-aist Oct 31, 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
9 changes: 9 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,21 @@

### Added

- in `ereal_normedtype.v`:
+ lemma `ge0_cvgMly`

### Changed

- in `lebesgue_integral_nonneg.v`, generalized and deprecated:
+ lemma `ge0_integralZl_EFin` (no condition on `k`)

### Renamed

### Generalized

- in `lebesgue_integral_nonneg.v`:
+ lemmas `ge0_integralZl`, `ge0_integralZr`

### Deprecated

### Removed
Expand Down
11 changes: 4 additions & 7 deletions theories/hoelder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -448,8 +448,7 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]).
rewrite ger0_norm; first by rewrite mulr_ge0 ?divr_ge0 ?fine_ge0 ?Lnorm_ge0.
by rewrite mulrACA -normrM EFinM; over.
rewrite ge0_integralZr//.
- by do 2 apply: measurableT_comp => //; exact: measurable_funM.
- by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
by do 2 apply: measurableT_comp => //; exact: measurable_funM.
rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA.
rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e.
rewrite -[X in _ * X]fineK; first by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
Expand Down Expand Up @@ -477,16 +476,14 @@ rewrite ge0_integralD//.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
under eq_integral do rewrite EFinM.
rewrite [X in X + _]ge0_integralZr//.
- by move=> x _; rewrite lee_fin powR_ge0.
- apply: measurableT_comp => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin powR_ge0.
- by rewrite lee_fin invr_ge0 ltW.
under [X in _ + X]eq_integral => x _ do rewrite EFinM.
rewrite ge0_integralZr//.
- by move=> x _; rewrite lee_fin powR_ge0.
- apply: measurableT_comp => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin powR_ge0.
- by rewrite lee_fin invr_ge0 ltW.
rewrite integral_normalized//; first exact: integrable_powR.
rewrite integral_normalized//; first exact: integrable_powR.
by rewrite 2!mul1e -EFinD pq.
Expand Down Expand Up @@ -641,7 +638,7 @@ apply: (@le_lt_trans _ _ x).
exact/measurableT_comp_powR/measurableT_comp.
- by move=> ? _; rewrite lee_fin.
rewrite {}/x; under eq_integral do rewrite EFinM.
rewrite ge0_integralZl_EFin ?powR_ge0//.
rewrite ge0_integralZl ?powR_ge0//.
by apply/measurable_EFinP/measurable_funD => //;
exact/measurableT_comp_powR/measurableT_comp.
rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//.
Expand Down
5 changes: 2 additions & 3 deletions theories/lebesgue_integral_theory/lebesgue_Rintegral.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -268,14 +268,13 @@ by rewrite mul0e.
Qed.

#[local] Lemma integral_measure_of_densityMindic (r : R) (A : set T) : measurable A ->
(0 <= r)%R ->
\int[mu]_x (r%:E * (\1_A x)%:E * (h x)%:E) = r%:E * mu' A.
Proof.
move=> mA r0.
move=> mA.
under eq_integral do rewrite -muleA.
rewrite ge0_integralZl//=.
- apply: emeasurable_funM => //; by apply /measurable_EFinP.
- by move=> x _; apply: mule_ge0; rewrite ?lee_fin.
- apply: emeasurable_funM => //; by apply /measurable_EFinP.
- by rewrite integral_measure_of_density_indic.
Qed.

Expand Down
26 changes: 13 additions & 13 deletions theories/lebesgue_integral_theory/lebesgue_integrable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,10 @@ From mathcomp Require Import lebesgue_integral_nonneg.

Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").

Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Expand Down Expand Up @@ -522,9 +522,9 @@ End integrable_ae.

Section integralZl.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variable (f : T -> \bar R).
Context {d} {T : measurableType d} {R : realType}
(mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
(f : T -> \bar R).
Hypothesis intf : mu.-integrable D f.

Let mesf : measurable_fun D f. Proof. exact: measurable_int intf. Qed.
Expand All @@ -534,13 +534,13 @@ Lemma integralZl r :
Proof.
have /orP[r0|r0] := le_total r 0%R.
- rewrite [in LHS]integralE// le0_funeposM// le0_funenegM//.
rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _)) ?oppr_ge0//.
rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _)) ?oppr_ge0//.
rewrite !EFinN addeC !mulNe oppeK -muleBr ?integrable_add_def//.
by rewrite [in RHS]integralE.
rewrite (ge0_integralZl _ _ _ (measurable_funeneg _))//.
rewrite (ge0_integralZl _ _ _ (measurable_funepos _))//.
rewrite !mulNe oppeK addeC -muleBr ?integrable_add_def//.
by rewrite -integralE.
- rewrite [in LHS]integralE// ge0_funeposM// ge0_funenegM//=.
rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _) r0)//.
rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _) r0)//.
rewrite (ge0_integralZl _ _ _ (measurable_funepos _))//.
rewrite (ge0_integralZl _ _ _ (measurable_funeneg _))//.
by rewrite -muleBr 1?[in RHS]integralE// integrable_add_def.
Qed.

Expand All @@ -552,9 +552,9 @@ End integralZl.

Section integralD_EFin.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
Variables f1 f2 : T -> R.
Context {d} {T : measurableType d} {R : realType}
(mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
(f1 f2 : T -> R).
Let g1 := EFin \o f1.
Let g2 := EFin \o f2.
Hypothesis if1 : mu.-integrable D g1.
Expand Down
37 changes: 15 additions & 22 deletions theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
(* *)
(******************************************************************************)

Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Expand Down Expand Up @@ -306,7 +305,7 @@ move=> mA1 mA2 /=; rewrite /product_measure1 /=.
rewrite (eq_integral (fun x => (\1_A1 x)%:E * m2 A2)).
by move=> x _; rewrite indicE; have [xA1|xA1] /= := boolP (x \in A1);
[rewrite in_xsectionX// mul1e|rewrite mul0e notin_xsectionX].
rewrite ge0_integralZr ?integral_indic ?setIT//; exact: measurableT_comp.
by rewrite ge0_integralZr ?integral_indic ?setIT//; exact: measurableT_comp.
Qed.

End product_measure1E.
Expand Down Expand Up @@ -461,7 +460,7 @@ Proof.
have mA1A2 : measurable (A1 `*` A2) by apply: measurableX.
transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //.
rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E); last first.
rewrite ge0_integralZl ?integral_indic ?setIT//; exact: measurableT_comp.
by rewrite ge0_integralZl ?integral_indic ?setIT//; exact: measurableT_comp.
rewrite funeqE => y; rewrite indicE.
have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionX.
by rewrite mule0 /= notin_ysectionX.
Expand Down Expand Up @@ -588,9 +587,8 @@ rewrite ge0_integral_fsum //.
- by move=> r y _; rewrite EFinM nnfun_muleindic_ge0.
apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
under eq_fun do rewrite EFinM.
rewrite ge0_integralZl//; [|by rewrite lee_fin|].
- exact/measurable_EFinP/measurableT_comp.
- by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
rewrite ge0_integralZl//; first exact/measurable_EFinP/measurableT_comp.
by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
Qed.

Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun [set: T1] F.
Expand All @@ -610,9 +608,8 @@ rewrite ge0_integral_fsum //.
- by move=> r x _; rewrite EFinM nnfun_muleindic_ge0.
apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
under eq_fun do rewrite EFinM.
rewrite ge0_integralZl//; [|by rewrite lee_fin|].
- exact/measurable_EFinP/measurableT_comp.
- by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
rewrite ge0_integralZl//; first exact/measurable_EFinP/measurableT_comp.
by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
Qed.

Lemma sfun_measurable_fun_fubini_tonelli_G : measurable_fun setT G.
Expand All @@ -634,16 +631,14 @@ under [LHS]eq_integral
transitivity (\sum_(k \in range f)
\int[m1]_x (k%:E * fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x)).
apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
rewrite ge0_integralZl//.
- exact/measurable_EFinP.
- by rewrite lee_fin.
rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin.
- exact: indic_measurable_fun_fubini_tonelli_F.
- by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
rewrite ge0_integralZl//=; first exact/measurable_EFinP.
rewrite indic_fubini_tonelli1// -ge0_integralZl//.
by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
exact: indic_measurable_fun_fubini_tonelli_F.
rewrite -ge0_integral_fsum; [by []| | |by []|]; first 2 last.
- apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE.
by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//.
- by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
- by move=> r; exact/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
move=> r x _; rewrite /fubini_F.
have [r0|r0] := leP 0%R r.
by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0.
Expand All @@ -660,12 +655,10 @@ under [LHS]eq_integral
transitivity (\sum_(k \in range f)
\int[m2]_x (k%:E * (fubini_G m1 (EFin \o \1_(f @^-1` [set k])) x))).
apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
rewrite ge0_integralZl//.
- exact/measurable_EFinP.
- by rewrite lee_fin.
rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin.
- exact: indic_measurable_fun_fubini_tonelli_G.
- by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
rewrite ge0_integralZl//=; first exact/measurable_EFinP.
rewrite indic_fubini_tonelli2// -ge0_integralZl//.
by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
exact: indic_measurable_fun_fubini_tonelli_G.
rewrite -ge0_integral_fsum; [by []| | |by []|]; first 2 last.
- apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE.
by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//.
Expand Down
Loading
Loading