Skip to content

fixes #1178 (ge0_integralZr) #1181

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 3 commits into from
Mar 6, 2024
Merged

fixes #1178 (ge0_integralZr) #1181

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fdf927b
fixes #1178
affeldt-aist Mar 5, 2024
a61798f
use ge0_integralZr
affeldt-aist Mar 5, 2024
34a54e2
rename section name
affeldt-aist Mar 6, 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 @@ -7,6 +7,9 @@
- in `exp.v`
+ lemma `ln_lt0`

- in `lebesgue_integral.v`
+ lemma `ge0_integralZr`

### Changed

- move from `kernel.v` to `measure.v`
Expand Down
7 changes: 2 additions & 5 deletions theories/charge.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1734,11 +1734,8 @@ under [RHS]eq_integral do rewrite EFinM.
rewrite integralZl_indic_nnsfun => //.
under eq_integral do rewrite EFinM -muleA.
rewrite ge0_integralZl//.
congr *%E.
under eq_integral do rewrite muleC.
under [RHS]eq_integral do rewrite -[_%:E]mul1e -/(idfun 1).
rewrite -(integral_setI_indic _ _)// -(integral_setI_indic _ _)//.
by rewrite -f_integral//= integral_cst ?mul1e.
- under eq_integral do rewrite muleC.
by rewrite -integral_setI_indic// -f_integral// integral_indic// setIC.
- apply: emeasurable_funM; first exact/EFin_measurable_fun.
exact/measurable_funTS/(measurable_int (f_integrable _)).
- by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0.
Expand Down
30 changes: 13 additions & 17 deletions theories/hoelder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,21 +199,17 @@ have [foo|foo] := eqVneq 'N_p%:E[f] +oo%E; first by rewrite foo gt0_mulye ?leey.
have [goo|goo] := eqVneq 'N_q%:E[g] +oo%E; first by rewrite goo gt0_muley ?leey.
pose F := normalized p f; pose G := normalized q g.
rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
rewrite !Lnorm1.
under [in RHS]eq_integral.
move=> x _.
rewrite /F /G /= /normalized (mulrC `|f x|)%R mulrA -(mulrA (_^-1)).
rewrite (mulrC (_^-1)) -mulrA ger0_norm; last first.
by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0).
by rewrite mulrC -normrM EFinM; over.
rewrite ge0_integralZl//; last 2 first.
rewrite !Lnorm1; under [in RHS]eq_integral.
move=> x _; rewrite /F /G /normalized/=.
rewrite ger0_norm; last by rewrite mulr_ge0 ?divr_ge0 ?fine_ge0 ?Lnorm_ge0.
by rewrite mulrACA -normrM EFinM; over.
rewrite ge0_integralZr//; last 2 first.
- by do 2 apply: measurableT_comp => //; exact: measurable_funM.
- by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
rewrite -muleA muleC muleA EFinM muleCA 2!muleA.
rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA.
rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
rewrite (_ : 'N_q%:E[g] * _ = 1) ?mul1e// muleC.
rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
Expand All @@ -227,29 +223,29 @@ rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
exact: measurable_normalized.
apply/aeW => x _; rewrite lee_fin ger0_norm ?conjugate_powR ?normalized_ge0//.
by rewrite mulr_ge0// normalized_ge0.
under eq_integral do rewrite EFinD mulrC (mulrC _ (_^-1)).
under eq_integral do rewrite EFinD.
rewrite ge0_integralD//; last 4 first.
- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
- do 2 apply: measurableT_comp => //.
- apply: measurableT_comp => //; apply: measurable_funM => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
- do 2 apply: measurableT_comp => //.
- apply: measurableT_comp => //; apply: measurable_funM => //.
by apply: measurableT_comp_powR => //; exact: measurable_normalized.
under eq_integral do rewrite EFinM.
rewrite {1}ge0_integralZl//; last 3 first.
rewrite [X in X + _]ge0_integralZr//; last 3 first.
- 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)%E]eq_integral => x _ do rewrite EFinM.
rewrite ge0_integralZl//; last 3 first.
under [X in _ + X]eq_integral => x _ do rewrite EFinM.
rewrite ge0_integralZr//; last 3 first.
- 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//; last exact: integrable_powR.
rewrite integral_normalized//; last exact: integrable_powR.
by rewrite 2!mule1 -EFinD pq.
by rewrite 2!mul1e -EFinD pq.
Qed.

End hoelder.
Expand Down
8 changes: 4 additions & 4 deletions theories/kernel.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -545,11 +545,11 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
exact/measurableT_comp.
- by move=> m y _; rewrite nnfun_muleindic_ge0.
apply: emeasurable_fun_fsum => // r.
rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E *
\int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first.
rewrite [X in measurable_fun _ X](_ : _ = fun x => r%:E *
\int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E); last first.
apply/funext => x; under eq_integral do rewrite EFinM.
have [r0|r0] := leP 0%R r.
rewrite ge0_integralZl//; last by move=> y _; rewrite lee_fin.
rewrite ge0_integralZl//; last by move=> *; rewrite lee_fin.
exact/EFin_measurable_fun/measurableT_comp.
rewrite integral0_eq; last first.
by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
Expand Down Expand Up @@ -1056,7 +1056,7 @@ rewrite /= integral_kcomp_indic; last exact/measurable_sfunP.
have [r0|r0] := leP 0%R r.
rewrite ge0_integralZl//; last first.
exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _.
by congr (_ * _); apply: eq_integral => y _; rewrite integral_indic// setIT.
by under eq_integral do rewrite integral_indic// setIT.
rewrite integral0_eq ?mule0; last first.
move=> y _; rewrite integral0_eq// => z _.
by rewrite preimage_nnfun0// indic0.
Expand Down
86 changes: 46 additions & 40 deletions theories/lebesgue_integral.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,12 @@ Require Import esum measure lebesgue_measure numfun.
(* *)
(* This file contains a formalization of the Lebesgue integral. It starts *)
(* with simple functions and their integral, provides basic operations *)
(* (addition, etc.), and proves the properties of their integral *)
(* (semi-linearity, non-decreasingness). It then defines the integral of *)
(* measurable functions, proves the approximation theorem, the properties of *)
(* their integral (semi-linearity, non-decreasingness), the monotone *)
(* convergence theorem, and Fatou's lemma. Finally, it proves the linearity *)
(* properties of the integral, the dominated convergence theorem and *)
(* Fubini's theorem, etc. *)
(* (addition, etc.), and proves the properties of their integral (linearity, *)
(* non-decreasingness). It then defines the integral of measurable functions, *)
(* proves the approximation theorem, the properties of their integral *)
(* (linearity, non-decreasingness), the monotone convergence theorem, and *)
(* Fatou's lemma. Finally, it proves the linearity properties of the *)
(* integral, the dominated convergence theorem and Fubini's theorem, etc. *)
(* *)
(* Main notation: *)
(* | Coq notation | | Meaning | *)
Expand Down Expand Up @@ -1621,8 +1620,7 @@ Qed.

End approximation.


Section semi_linearity0.
Section ge0_linearityZ.
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).
Expand Down Expand Up @@ -1654,11 +1652,11 @@ rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg).
by apply: cvgeMl => //; exact: gh1.
Qed.

End semi_linearity0.
End ge0_linearityZ.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `ge0_integralZl_EFin` instead")]
Notation ge0_integralM_EFin := ge0_integralZl_EFin (only parsing).

Section semi_linearity.
Section ge0_linearityD.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
Expand Down Expand Up @@ -1733,7 +1731,7 @@ rewrite lee_fin; apply: nondecreasing_cvgn_le.
by apply/cvg_ex; eexists; exact: u_h1.
Unshelve. all: by end_near. Qed.

End semi_linearity.
End ge0_linearityD.

Section approximation_sfun.
Context d (T : measurableType d) (R : realType) (f : T -> \bar R).
Expand Down Expand Up @@ -2276,24 +2274,25 @@ Qed.

End integral_nneseries.

(* generalization of ge0_integralZl_EFin to a constant potentially +oo
using the monotone convergence theorem *)
Section ge0_integralZl.
(**md Generalization of `ge0_integralZl_EFin` to a constant potentially $+\infty$
using the monotone convergence theorem: *)
Section ge0_integralZ.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType).
Context d {T : measurableType d} {R : realType}.
Variable mu : {measure set T -> \bar R}.
Variables (D : set T) (mD : measurable D) (f : T -> \bar R).
Hypothesis mf : measurable_fun D f.
Implicit Type k : \bar R.

Lemma ge0_integralZl (k : \bar R) : (forall x, D x -> 0 <= f x) ->
0 <= k -> \int[mu]_(x in D) (k * f x)%E = k * \int[mu]_(x in D) (f x).
Lemma ge0_integralZl k : (forall x, D x -> 0 <= f x) ->
0 <= k -> \int[mu]_(x in D) (k * f x) = k * \int[mu]_(x in D) (f x).
Proof.
move=> f0; move: k => [k|_|//]; first exact: ge0_integralZl_EFin.
pose g : (T -> \bar R)^nat := fun n x => n%:R%:E * f x.
have mg n : measurable_fun D (g n) by apply: measurable_funeM.
have g0 n x : D x -> 0 <= g n x.
by move=> Dx; apply: mule_ge0; [rewrite lee_fin|exact:f0].
have nd_g x : D x -> nondecreasing_seq (g^~x).
have nd_g x : D x -> nondecreasing_seq (g ^~ x).
by move=> Dx m n mn; rewrite lee_wpmul2r ?f0// lee_fin ler_nat.
pose h := fun x => limn (g^~ x).
transitivity (\int[mu]_(x in D) limn (g^~ x)).
Expand All @@ -2318,17 +2317,17 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
rewrite -(ler_nat R); apply: le_trans.
rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// -mulrNN.
by rewrite mulr_ge0// lerNr oppr0// ltW// invr_lt0.
- rewrite -fx0 mule0 /g -fx0 [X in X @ _ --> _](_ : _ = cst 0).
exact: cvg_cst.
by rewrite funeqE => n /=; rewrite mule0.
- rewrite -fx0 mule0 /g -fx0.
under eq_fun do rewrite mule0/=. (*TODO: notation broken*)
exact: cvg_cst.
rewrite (monotone_convergence mu mD mg g0 nd_g).
under eq_fun do rewrite /g ge0_integralZl_EFin//.
have : 0 <= \int[mu]_(x in D) (f x) by exact: integral_ge0.
under eq_fun do rewrite /g ge0_integralZl_EFin//.
have : 0 <= \int[mu]_(x in D) f x by exact: integral_ge0.
rewrite le_eqVlt => /predU1P[<-|if_gt0].
by rewrite mule0; under eq_fun do rewrite mule0; rewrite lim_cst.
rewrite gt0_mulye//; apply/cvg_lim => //; apply/cvgeyPgey; near=> M.
have M0 : (0 <= M)%R by [].
near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) (f x)) +oo; last first.
near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) f x) +oo; last first.
rewrite leye_eq => /eqP ->; rewrite mulry muleC gt0_mulye ?leey//.
by near: n; exists 1%N => // n /= n0; rewrite gtr0_sg// ?lte_fin// ltr0n.
rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first.
Expand All @@ -2339,10 +2338,17 @@ near: n.
exists `|ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans.
rewrite lee_fin natr_absz ger0_norm ?ceil_ge// ceil_ge0//.
by rewrite mulr_ge0// ?invr_ge0//; apply/fine_ge0/integral_ge0.
by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
Unshelve. all: by end_near. Qed.

End ge0_integralZl.
Lemma ge0_integralZr k : (forall x, D x -> 0 <= f x) ->
0 <= k -> \int[mu]_(x in D) (f x * k) = \int[mu]_(x in D) (f x) * k.
Proof.
move=> f0 k0; under eq_integral do rewrite muleC.
by rewrite ge0_integralZl// muleC.
Qed.

End ge0_integralZ.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `ge0_integralZl` instead")]
Notation ge0_integralM := ge0_integralZl (only parsing).

Expand Down Expand Up @@ -3364,7 +3370,7 @@ Qed.

End integrable_ae.

Section linearity.
Section linearityZ.
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).
Expand Down Expand Up @@ -3397,11 +3403,11 @@ have [r0|r0|->] := ltgtP r 0%R; last first.
by rewrite [in RHS]integralE.
Qed.

End linearity.
End linearityZ.
#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl` instead")]
Notation integralM := integralZl (only parsing).

Section linearity.
Section linearityD_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).
Expand Down Expand Up @@ -3484,7 +3490,7 @@ rewrite (ge0_integralD mu mD) //; last exact: measurable_funepos.
exact/measurable_funeneg/emeasurable_funD.
Qed.

End linearity.
End linearityD_EFin.

Lemma integralB_EFin d (T : measurableType d) (R : realType)
(mu : {measure set T -> \bar R}) (D : set T) (f1 f2 : T -> R)
Expand Down Expand Up @@ -4743,11 +4749,11 @@ Lemma product_measure1E (A1 : set T1) (A2 : set T2) :
measurable A1 -> measurable A2 -> (m1 \x m2) (A1 `*` A2) = m1 A1 * m2 A2.
Proof.
move=> mA1 mA2 /=; rewrite /product_measure1 /=.
rewrite (eq_integral (fun x => m2 A2 * (\1_A1 x)%:E)); last first.
rewrite (eq_integral (fun x => (\1_A1 x)%:E * m2 A2)); last first.
by move=> x _; rewrite indicE; have [xA1|xA1] /= := boolP (x \in A1);
[rewrite in_xsectionM// mule1|rewrite mule0 notin_xsectionM].
rewrite ge0_integralZl//; last by move=> x _; rewrite lee_fin.
- by rewrite muleC integral_indic// setIT.
[rewrite in_xsectionM// mul1e|rewrite mul0e notin_xsectionM].
rewrite ge0_integralZr//; last by move=> x _; rewrite lee_fin.
- by rewrite integral_indic// setIT.
- exact: measurableT_comp.
Qed.

Expand Down Expand Up @@ -4860,10 +4866,10 @@ Proof.
have mA1A2 : measurable (A1 `*` A2) by apply: measurableM.
transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //.
rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E).
rewrite ge0_integralZl//; last 2 first.
- exact: measurableT_comp.
- by move=> y _; rewrite lee_fin.
by rewrite integral_indic ?setIT ?mul1e.
rewrite ge0_integralZl//.
- by rewrite integral_indic ?setIT ?mul1e.
- exact: measurableT_comp.
- by move=> y _; rewrite lee_fin.
rewrite funeqE => y; rewrite indicE.
have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionM.
by rewrite mule0 /= notin_ysectionM.
Expand Down Expand Up @@ -5226,7 +5232,7 @@ under [LHS]eq_integral
apply/EFin_measurable_fun/measurableT_comp => //=.
- by move=> r /= z _; exact: nnfun_muleindic_ge0.
transitivity (\sum_(k \in range f)
\int[m1]_x (k%:E * (fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x))).
\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//; last 3 first.
- exact/EFin_measurable_fun.
Expand Down