From 826b4bfce45e2dffd95e0c59d051ca03340079cc Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 20 Aug 2026 01:18:31 +0900 Subject: [PATCH 1/3] add Rintegral_gt0_itvcc --- classical/classical_sets.v | 4 + .../lebesgue_Rintegral.v | 113 ++++++++++++++++++ .../lebesgue_integrable.v | 81 +++++++++++++ theories/normedtype_theory/normed_module.v | 16 +++ theories/topology_theory/topology_structure.v | 23 +++- 5 files changed, 236 insertions(+), 1 deletion(-) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 95449d426c..f9249df94a 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -443,6 +443,10 @@ Notation "`] a , '+oo' [" := Notation "`] -oo , '+oo' [" := [set` Interval -oo%O +oo%O] : classical_set_scope. +Lemma in1_mksetP (T : Type) (p : {pred T}) (P : T -> Prop) : + {in p, forall x, P x} <-> {in [set` p], forall x, P x}. +Proof. by split => H x; rewrite ?inE/= => xp; apply: H => //; rewrite inE. Qed. + Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed. #[global] Hint Resolve nat_nonempty : core. diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 6327d6b5e1..05ee08d330 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -246,6 +246,119 @@ rewrite addrC addKr Rintegral_itvob_itvcb//. by apply: integrableS itf => //; exact/subset_itvr/ltW. Qed. +Lemma Rintegral_gt0 f D : + mu.-integrable D (EFin \o f) -> + open D -> + {in D, continuous f} -> + {in D, forall x : R, 0 <= f x} -> + ~ {in D, forall x : R, f x == 0} -> + 0 < \int[mu]_(x in D) f x. +Proof. +move=> f_ble oD cf f_ge0 /existsNP [] c /not_implyP [] cD /negP fc_neq0. +have fc_gt0 : f c > 0 by rewrite lt_neqAle eq_sym fc_neq0 f_ge0. +pose U := `]f c / 2, +oo[%classic. +have oU : open U by exact: itv_open_ends_open. +have /(continuous_inP _ oD)/(_ U oU) oDfU:= cf. +have mD : measurable D by exact: open_measurable. +have : D `&` f @^-1` U != set0. + apply/set0P; exists c; split => /=; first by move/set_mem: cD. + rewrite /U /= in_itv/= andbT. + by rewrite -[fc in fc / _]add0r midf_lt. +have -> := open_bigcup_basis real_basis oDfU. +case/eqP/bigcup0P/existsNP => I /not_implyP[] I_spec /eqP/set0P[]/= p Ip. +have := I_spec => -[]/= [] a _ [] b _ IE IDfU. +have mI : measurable I by rewrite -IE; exact: open_measurable. +have ID : I `<=` D by apply: (subset_trans IDfU); exact: subIsetl. +rewrite -fine0; apply: fine_lt => //; first exact: integrable_fin_num. +suff : (0 < \int[mu]_(x in I) (f x)%:E)%E. + move/lt_le_trans; apply. + apply: ge0_subset_integral => //=. + apply/measurable_EFinP. + exact: open_continuous_measurable_fun. + by move=> x Dx; apply: f_ge0; rewrite inE. +apply: (@lt_le_trans _ _ (\int[mu]_(x in I) (cst (f c / 2)%:E x))%E). + rewrite integral_cst//=. + apply: mule_gt0; first by rewrite lte_fin divr_gt0. + rewrite -IE lebesgue_measure_itv/= lte_fin. + suff ab : a < b by rewrite ab lte_fin subr_gt0. + by move: Ip; rewrite -IE/= in_itv/= => /andP[] /lt_trans /[apply]. +apply: ge0_le_integral => //=. +- by move=> ? ?; rewrite lee_fin divr_ge0// ltW. +- apply/measurable_EFinP. + apply: open_continuous_measurable_fun; first by rewrite -IE. + by move=> ?; rewrite inE => ?; apply: cf; rewrite inE; apply: ID. +move=> x Ix; rewrite lee_fin ltW//. +move: Ix => /IDfU[] Dx /=. +by rewrite /U/= in_itv/= andbT. +Qed. + +Lemma Rintegral_gt0_itvcc f (a b : R) : + a < b -> + {in `[a, b], continuous f} -> + {in `[a, b], forall x : R, 0 <= f x} -> + ~ {in `[a, b], forall x : R, f x == 0} -> + 0 < \int[mu]_(x in `[a, b]) f x. +Proof. +move=> ab cf f_ge0 f_neq0. +have ooSab : `]a, b[ `<=` `[a, b] by exact: subset_itvW. +have cf_oo := sub_in1 ooSab cf. +have within_cf := continuous_subspace_itv cf. +have := f_neq0 => /existsNP[] p /not_implyP[] pab /negP fp_neq0. +have fp_gt0 : 0 < f p by rewrite lt_neqAle eq_sym fp_neq0/= f_ge0. +have f_ble : mu.-integrable `[a, b] (EFin \o f). + apply: compact_continuous_Rintegrable => //; first by exists p. + exact: segment_compact. +have f_ble_oo : mu.-integrable `]a, b[ (EFin \o f). + exact: (integrableS _ _ _ f_ble). +suff : (0 < \int[mu]_(x in `[a, b]) (f x)%:E)%E. + move/fine_lt; apply => //. + exact: integrable_fin_num. +rewrite integral_itvbb_itvoo/=. + apply/measurable_EFinP. + apply: subspace_continuous_measurable_fun => //. + exact: continuous_subspace_itv. +rewrite -[ltRHS]fineK ?integrable_fin_num//=. +rewrite lte_fin Rintegral_gt0//. +- by rewrite -in1_mksetP. +- by rewrite -in1_mksetP; apply: (sub_in1 ooSab). +(* the rest of the proof is just for ~ {in `]a, b[, forall x : R, f x == 0}, + i.e., about extending a constant function on an open interval to its closure *) +move=> f_eq0oo. +have faboo_sing : f @` `]a, b[%classic = [set 0]. + apply/seteqP; split => x /=. + by case => y /mem_set /f_eq0oo /eqP -> /esym. + move->; exists (miditv `]a, b[); first exact: mem_miditv. + by apply/eqP/f_eq0oo; rewrite inE; exact: mem_miditv. +have: `[a, b]%classic p by []. +rewrite -(setUitv_set2 false true) ?ltW//. +case; first by move/mem_set/f_eq0oo; rewrite (negPf fp_neq0). +case => [pa|pb]/=. + have : connected `[a, b[%classic. + exact/connected_intervalP/interval_is_interval. + have : {within `[a, b[, continuous f}. + have := within_cf; apply: continuous_subspaceW. + by apply/subset_itvl; rewrite bnd_simp. + move/connected_continuous_connected/[apply]. + rewrite -setU_1itvob ?bnd_simp// image_setU faboo_sing -pa image_set1. + apply/connectedPn; exists (fun b => if b then [set 0] else [set f p]). + split => //; first by case; [exists 0 | exists (f p)]. + split. + by rewrite -(closure_id [set _]).1// set1I in_set1 (negPf fp_neq0). + by rewrite -(closure_id [set _]).1// set1I in_set1 (negPf fp_neq0). +have : connected `]a, b]%classic. + exact/connected_intervalP/interval_is_interval. +have : {within `]a, b], continuous f}. + have := within_cf; apply: continuous_subspaceW. + by apply/subset_itvr; rewrite bnd_simp. +move/connected_continuous_connected/[apply]. +rewrite -setU_itvob1 ?bnd_simp// image_setU faboo_sing -pb image_set1. +apply/connectedPn; exists (fun b => if b then [set f p] else [set 0]). +split => //; first by case; [exists (f p) | exists 0]. +split. + by rewrite -(closure_id [set _]).1// setI1 in_set1 (negPf fp_neq0). +by rewrite -(closure_id [set _]).1// setI1 in_set1 (negPf fp_neq0). +Qed. + End Rintegral_lebesgue_measure. #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvbo_itvbc)] Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing). diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 36fd2ec2d7..4467cb9eeb 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -1101,3 +1101,84 @@ rewrite h set_neq_lt setIUr measureU//; [exact: measurable_lte..| |]. Qed. End integral_ae_eq. + +Lemma gerNE : forall {R : numDomainType(*porderedZmodType*)} (x : R), (0 <= x) = (- x <= x). +Proof. +move=> ? x. +apply/idP/idP; first exact: gerN. +rewrite -[leLHS]add0r lerBlDl -mulr2n. +by rewrite pmulrn_lge0. +Qed. + +Lemma lerNE : forall {R : numDomainType(*porderedZmodType*)} (x : R), (x <= 0) = (x <= - x). +Proof. by move=> ? x; rewrite -[RHS]lerN2 -gerNE oppr_ge0. Qed. + +Lemma EVT_abs_max : + forall [T : topologicalType] [R : realType] [f : T -> R] [A : set T], + A !=set0 -> + compact A -> + {within A, continuous f} -> + exists2 c : T, c \in A & forall t : T, t \in A -> `|f t| <= `|f c|. +Proof. +move=> ? ? f D D_neq0 cptD cf. +have /= [x xD x_ub] := derive.compact_EVT_max D_neq0 cptD cf. +have /= [y yD y_lb] := derive.compact_EVT_min D_neq0 cptD cf. +have [xy| /ltW yx] := leP `|f x| `|f y|. + exists y => // t tD; move: xy. + rewrite !ler_normr !ler_norml opprK !x_ub//= !y_lb//=. + case/orP => [/andP[Nfyx fxy]|fxNy]. + have fxEy : f x = f y. + apply: le_anti; rewrite fxy x_ub//. + have := Nfyx; rewrite fxEy. + have fyx := x_ub y yD. + rewrite -gerNE => fy_ge0. + rewrite orbC -implyNb. + apply/implyP; rewrite -ltNge => /ltW -> /=. + by rewrite -fxEy x_ub. + rewrite orbC -implyNb. + apply/implyP; rewrite -ltNge => /[dup] H /ltW /[dup] Nfyt -> /=. + have fxEt : f x = f t. + by apply: le_anti; rewrite x_ub// (le_trans fxNy Nfyt). + have fxENy : f x = - f y. + by apply: le_anti; rewrite fxNy fxEt Nfyt. + by have := H; rewrite -fxEt fxENy ltxx. +exists x => // t tD; move: yx. +rewrite !ler_normr !ler_norml !opprK !x_ub//= !andbT. +case/orP => [Nfxy|/andP[fxy fyNx]]; last first. + have fxEy : f x = f y. + apply: le_anti; rewrite fxy x_ub//. + have := fyNx; rewrite fxEy. + have fyx := x_ub y yD. + rewrite -lerNE => fy_ge0. + rewrite -implyNb. + apply/implyP; rewrite -ltNge => /ltW -> /=. + by rewrite y_lb. +rewrite -implyNb. +apply/implyP; rewrite -ltNge => /[dup] H /ltW /[dup] ftNx -> /=; rewrite andbT. +have fyEt : f y = f t. + by apply: le_anti; rewrite y_lb// (le_trans ftNx Nfxy). +have fyENx : f y = - f x. + by apply: le_anti; rewrite Nfxy fyEt ftNx. +by have := H; rewrite -fyEt fyENx ltxx. +Qed. + +Lemma compact_continuous_Rintegrable {R : realType} (D : set R) (f : R -> R) : + D !=set0 -> compact D -> {within D, continuous f} -> + lebesgue_measure.-integrable D (EFin \o f). +Proof. +move=> D_neq0 cptD cf. +apply/integrableP; split. + apply/measurable_EFinP. + apply: subspace_continuous_measurable_fun. + exact: compact_measurable. + exact: cf. +have /=[x xD x_ub] := EVT_abs_max D_neq0 cptD cf. +have mD := compact_measurable cptD. +apply: (@le_lt_trans _ _ (\int[lebesgue_measure]_(d in D) (cst `|f x|%:E d))%E). + apply: ge0_le_integral => //. + - apply/measurable_EFinP. + apply: measurableT_comp => //. + exact: subspace_continuous_measurable_fun. + by move=> /= ? ?; apply: x_ub; rewrite inE. +by rewrite integral_cst//= lte_mul_pinfty // compact_finite_measure. +Qed. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index d8720f1c64..d1d1a9af6f 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2573,6 +2573,22 @@ Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed. End open_set_disjoint_real_intervals. +Section real_basis. +Context {R : realFieldType}. + +Lemma real_basis : + @basis R [set `]x, y[%classic | x in [set: R] & y in [set: R]]. +Proof. +split; first by move=> U [] x _ [] y _ <-; exact: interval_open. +move=> x U [] e /= e0 bU. +exists (ball_ Num.Def.normr x e) => //=. +rewrite subrr normr0; split => //. +exists (x - e) => //; exists (x + e) => //. +by rewrite -ball_itv. +Qed. + +End real_basis. + Section EquivalenceNorms. Variables (R : realType). diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index ca3115f5ec..79ccc48f5a 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -118,7 +118,7 @@ HB.structure Definition SubTopological (V : topologicalType) (S : pred V) := {U of SubNbhs V S U & Topological U}. Section Topological1. -Context {T : topologicalType}. +Context {T T' : topologicalType}. Definition open_nbhs (p : T) (A : set T) := open A /\ A p. @@ -231,6 +231,17 @@ rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 ?] | []]. [exact: open_nbhsI | rewrite subsetI; split; apply: subIset; [left|right]]. Qed. +Lemma open_bigcup_basis (F : set_system T) (A : set T) : + basis F -> open A -> + A = \bigcup_(i in [set i | F i /\ i `<=` A]) i. +Proof. +case=> Fo Ffilt oA; apply/seteqP; split => x. + move=> Ax. + have:= Ffilt x A (open_nbhs_nbhs (conj oA Ax)). + by case=> U /= [] FU Ux UA; exists U => //; split. +by case=> U /= [] FU; exact. +Qed. + End Topological1. Lemma open_in_nearW {T : topologicalType} (P : T -> Prop) (S : set T) : @@ -265,6 +276,16 @@ move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA]. by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA]. Qed. +Lemma continuous_on_basis (S T : topologicalType) + (F : set_system T) (f : S -> T) : + basis F -> (forall A : set T, F A -> open (f @^-1` A)) -> continuous f. +Proof. +move=> bF bcf. +apply/continuousP => A /(open_bigcup_basis bF) ->. +rewrite preimage_bigcup; apply: bigcup_open. +by move=> U /= [] FU UA; exact: bcf. +Qed. + Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) : {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D). Proof. From 470c76db770e87af4714690a85accc720b0f6c01 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 20 Aug 2026 01:30:16 +0900 Subject: [PATCH 2/3] cleaning --- .../lebesgue_integrable.v | 65 ++----------------- 1 file changed, 4 insertions(+), 61 deletions(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 4467cb9eeb..be436d1f11 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -1102,66 +1102,6 @@ Qed. End integral_ae_eq. -Lemma gerNE : forall {R : numDomainType(*porderedZmodType*)} (x : R), (0 <= x) = (- x <= x). -Proof. -move=> ? x. -apply/idP/idP; first exact: gerN. -rewrite -[leLHS]add0r lerBlDl -mulr2n. -by rewrite pmulrn_lge0. -Qed. - -Lemma lerNE : forall {R : numDomainType(*porderedZmodType*)} (x : R), (x <= 0) = (x <= - x). -Proof. by move=> ? x; rewrite -[RHS]lerN2 -gerNE oppr_ge0. Qed. - -Lemma EVT_abs_max : - forall [T : topologicalType] [R : realType] [f : T -> R] [A : set T], - A !=set0 -> - compact A -> - {within A, continuous f} -> - exists2 c : T, c \in A & forall t : T, t \in A -> `|f t| <= `|f c|. -Proof. -move=> ? ? f D D_neq0 cptD cf. -have /= [x xD x_ub] := derive.compact_EVT_max D_neq0 cptD cf. -have /= [y yD y_lb] := derive.compact_EVT_min D_neq0 cptD cf. -have [xy| /ltW yx] := leP `|f x| `|f y|. - exists y => // t tD; move: xy. - rewrite !ler_normr !ler_norml opprK !x_ub//= !y_lb//=. - case/orP => [/andP[Nfyx fxy]|fxNy]. - have fxEy : f x = f y. - apply: le_anti; rewrite fxy x_ub//. - have := Nfyx; rewrite fxEy. - have fyx := x_ub y yD. - rewrite -gerNE => fy_ge0. - rewrite orbC -implyNb. - apply/implyP; rewrite -ltNge => /ltW -> /=. - by rewrite -fxEy x_ub. - rewrite orbC -implyNb. - apply/implyP; rewrite -ltNge => /[dup] H /ltW /[dup] Nfyt -> /=. - have fxEt : f x = f t. - by apply: le_anti; rewrite x_ub// (le_trans fxNy Nfyt). - have fxENy : f x = - f y. - by apply: le_anti; rewrite fxNy fxEt Nfyt. - by have := H; rewrite -fxEt fxENy ltxx. -exists x => // t tD; move: yx. -rewrite !ler_normr !ler_norml !opprK !x_ub//= !andbT. -case/orP => [Nfxy|/andP[fxy fyNx]]; last first. - have fxEy : f x = f y. - apply: le_anti; rewrite fxy x_ub//. - have := fyNx; rewrite fxEy. - have fyx := x_ub y yD. - rewrite -lerNE => fy_ge0. - rewrite -implyNb. - apply/implyP; rewrite -ltNge => /ltW -> /=. - by rewrite y_lb. -rewrite -implyNb. -apply/implyP; rewrite -ltNge => /[dup] H /ltW /[dup] ftNx -> /=; rewrite andbT. -have fyEt : f y = f t. - by apply: le_anti; rewrite y_lb// (le_trans ftNx Nfxy). -have fyENx : f y = - f x. - by apply: le_anti; rewrite Nfxy fyEt ftNx. -by have := H; rewrite -fyEt fyENx ltxx. -Qed. - Lemma compact_continuous_Rintegrable {R : realType} (D : set R) (f : R -> R) : D !=set0 -> compact D -> {within D, continuous f} -> lebesgue_measure.-integrable D (EFin \o f). @@ -1172,7 +1112,10 @@ apply/integrableP; split. apply: subspace_continuous_measurable_fun. exact: compact_measurable. exact: cf. -have /=[x xD x_ub] := EVT_abs_max D_neq0 cptD cf. +have : {within D, continuous (fun t => `|f t|)}. + apply: within_continuous_comp => //. + by move=> *; exact: norm_continuous. +move/(derive.compact_EVT_max D_neq0 cptD) => /= [x xD x_ub]. have mD := compact_measurable cptD. apply: (@le_lt_trans _ _ (\int[lebesgue_measure]_(d in D) (cst `|f x|%:E d))%E). apply: ge0_le_integral => //. From 23957e3f7f9d4287409a5f62f8f4480441c558cf Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 20 Aug 2026 01:33:04 +0900 Subject: [PATCH 3/3] cleaning --- theories/topology_theory/topology_structure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 79ccc48f5a..5352229d7e 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -118,7 +118,7 @@ HB.structure Definition SubTopological (V : topologicalType) (S : pred V) := {U of SubNbhs V S U & Topological U}. Section Topological1. -Context {T T' : topologicalType}. +Context {T : topologicalType}. Definition open_nbhs (p : T) (A : set T) := open A /\ A p.