From d27d6e6dabe91a57395208282b342168642adc40 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Sun, 12 Apr 2026 12:22:45 +0200 Subject: [PATCH] discrete and continuous abel transforms --- CHANGELOG_UNRELEASED.md | 9 + classical/unstable.v | 9 +- reals/real_interval.v | 21 ++ .../lebesgue_integrable.v | 39 +++ theories/showcase/pnt.v | 228 +++++++++++++++++- 5 files changed, 302 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 196bb251a..4bdff66a6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -19,6 +19,15 @@ - in `measurable_function.v`: + lemma `preimage_measurability` +- in `real_interval.v` + + lemma `itvzz_bnd_bigcupD1` + +- in `lebesgue_integrable.v` + + lemmas `integrable_setU`, `integrable_bigsetU` + +- in `pnt.v` + + lemmas `Abel_discrete`, `Abel_continuous` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: diff --git a/classical/unstable.v b/classical/unstable.v index a5e7ac3db..9e3877e09 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -35,7 +35,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.TTheory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. Section IntervalNumDomain. @@ -592,3 +592,10 @@ Proof. exact: real_ltr_bound. Qed. Lemma ltrNbound {R : archiRealDomainType} (x : R) : - x < (Num.bound x)%:R. Proof. exact: real_ltrNbound. Qed. + +Lemma floor_nat (R : archiNumDomainType) n : absz (floor (n%:R : R)) = n. +Proof. +apply: (can_inj absz_nat). +rewrite gez0_abs; first by rewrite real_floor_ge0. +by apply /(@intr_inj R) /eqP; rewrite -[_ == _]intrEfloor. +Qed. diff --git a/reals/real_interval.v b/reals/real_interval.v index b29819933..2513a834e 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -322,3 +322,24 @@ Proof. rewrite -subTset => x _ /=; exists (Num.bound x) => //=. by rewrite in_itv lteifNl 2?lteifS// (ltr_bound, ltrNbound). Qed. + +Lemma itvzz_bnd_bigcupD1 (R : realType) (x y : int) : + (x <= y)%R -> + `[x%:~R, y%:~R[%classic = + (\bigcup_(i < `|(y - x)%R|) + `[(x + i%:R)%:~R, (x + i.+1%:R)%:~R[)%classic :> set R. +Proof. +rewrite predeqE => xy z/=. rewrite in_itv/=. +split=> [/andP[xz zy]|[] i /=]; last first. + rewrite -(ltr_nat int) [(`|_|%:R)%R]natz gez0_abs ?subr_ge0//. + rewrite -lezD1 natr1 => iyx; rewrite in_itv/= => /andP[xz zx]. + apply/andP; split; first by apply: (le_trans _ xz); rewrite ler_int lerDl. + by apply: (lt_le_trans zx); rewrite ler_int -lerBrDl. +exists (`|floor (z - x%:~R)|)%N => /=. + rewrite -(ltr_nat int) !natz !gez0_abs ?floor_ge0 ?subr_ge0//. + rewrite -(ltr_int R) intrB. + by apply/(le_lt_trans (floor_le _)); rewrite ltrD2r. +rewrite -natr1 natz gez0_abs; first by rewrite floor_ge0 subr_ge0. +rewrite -[X in X \in _](subrK x%:~R) addrC in_itv/= 2!intrD. +by rewrite lerD2l ltrD2l floor_itv. +Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 6c62cd461..4fdb7bba0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -445,6 +445,45 @@ apply: le_lt_trans ifoo; apply: ge0_subset_integral => //. exact: measurableT_comp. Qed. +Lemma integrable_setU (E D : set T) (f : T -> \bar R) : + d.-measurable E -> + d.-measurable D -> + mu.-integrable (E `|` D) f <-> mu.-integrable E f /\ mu.-integrable D f. +Proof. +move=> ??; split=> [fi|[]]. + by split; apply: (integrableS _ _ _ fi) => //; apply: measurableU. +move=> /integrableP[] fmE fiE /integrableP[] fmD fiD. +apply/integrableP; split; first exact/measurable_funU. +have ED: E `|` D = E `|` (D `\` E). + by rewrite -(setDUK (@subsetUl _ E D)) setDUD setDv set0U. +rewrite ED ge0_integral_setU//. +- exact: measurableD. +- apply: (measurable_comp measurableT) => //. + by rewrite -ED; apply/measurable_funU. +- by apply/disj_setPRL; apply: subIsetr. +apply: lte_add_pinfty => //. +apply/(le_lt_trans _ fiD); apply/ge0_subset_integral => //. + exact: measurableD. +exact: (measurable_comp measurableT). +Qed. + +(* TOTHINK: The equivalence is painful to state because I need to filter s. + However, the reciprocal is a consequence of `integrableS`, so maybe we do + not care. *) +Lemma integrable_bigsetU (I : Type) (s : seq I) (P : pred I) (D : I -> set T) + (f : T -> \bar R) : + (forall i, P i -> d.-measurable (D i)) -> + (forall i, P i -> mu.-integrable (D i) f) -> + mu.-integrable (\big[setU/set0]_(i <- s | P i) D i) f. +Proof. +move=> Dm fi. +elim: s => [|i s IHs]; first by rewrite big_nil; apply: integrable_set0. +rewrite big_cons; case: ifP => // iP. +apply/integrable_setU; first exact: Dm. + by apply: bigsetU_measurable. +by split=> //; apply: fi. +Qed. + Lemma integrable_mkcond D f : measurable D -> mu.-integrable D f <-> mu.-integrable setT (f \_ D). Proof. diff --git a/theories/showcase/pnt.v b/theories/showcase/pnt.v index 2b850a136..ea3b83ed3 100644 --- a/theories/showcase/pnt.v +++ b/theories/showcase/pnt.v @@ -1,8 +1,12 @@ From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. #[warning="-warn-library-file-internal-analysis"] -From mathcomp Require Import unstable. -From mathcomp Require Import classical_sets boolp topology. -From mathcomp Require Import ereal sequences reals. +From mathcomp Require Import archimedean mathcomp_extra unstable. +From mathcomp Require Import classical_sets boolp topology measure_function. +From mathcomp Require Import set_interval normed_module. +From mathcomp Require Import pseudometric_normed_Zmodule measurable_function. +From mathcomp Require Import measurable_realfun measurable_structure . +From mathcomp Require Import derive lebesgue_measure lebesgue_integral ftc. +From mathcomp Require Import ereal sequences reals realfun real_interval. Import Order.POrderTheory GRing.Theory Num.Theory. (**md**************************************************************************) @@ -23,6 +27,10 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Import Num.Def. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. +Local Open Scope order_scope. Local Open Scope classical_set_scope. Local Open Scope set_scope. Local Open Scope nat_scope. @@ -452,3 +460,217 @@ apply: (@cardG R); first by move: Rklthalf; rewrite /un div1r. Qed. End dvg_sum_inv_prime_seq. + +Lemma Abel_discrete (R : comPzRingType) (a b : nat -> R) (n p : nat) : + p < n -> let A n := (\sum_(0 <= k < n.+1) a k)%R in + (\sum_(p.+1 <= k < n.+1) (a k) * (b k) = A n * b n - A p * b p.+1 + + \sum_(p.+1 <= k < n) A k * (b k - b k.+1))%R. +Proof. +move=> ngtp A. +rewrite big_nat_cond. +under eq_bigr => k /andP [] /andP [] pk _ _. + rewrite (_ : a k = (A k - A k.-1)%R) ?mulrBl. + by rewrite /A (ltn_predK pk) // big_nat_recr //= [RHS]addrC addKr. + over. +rewrite -big_nat_cond. +under [in RHS]eq_bigr do rewrite mulrBr. +rewrite !big_split !sumrN /= [X in (_ - X)%R]big_add1 -pred_Sn. +under [X in (_ - X)%R]eq_bigr do rewrite -pred_Sn. +by rewrite [RHS](AC (2*2) ((3*1)*(2*4)))/= -big_nat_recr//= -opprD -big_ltn. +Qed. + +Local Notation "\int_( x 'in' D ) F" := (\int[lebesgue_measure]_(x in D) F)%R + (at level 36, F at level 36, x, D at level 50). + +Lemma Abel_continuous (R : realType) (x y : R^o) (f : R^o -> R^o) + (a : nat -> R) : (0 <= y <= x)%R -> derivable_oo_LRcontinuous f y x -> + {within `[y, x] : set R^o, continuous f^`()} -> + let A := fun x : R => (\sum_(0 <= n < `|floor x|.+1) a n)%R in + (\sum_(`|floor y|.+1 <= n < `|floor x|.+1) a n * f n%:R = + A x * f x - A y * f y - \int_(t in `[y, x]) (A t * f^`() t))%R. +Proof. +move=> /andP [] y0 /[dup] /(le_trans y0) x0 /[dup] yx. +rewrite le_eqVlt => /orP[/eqP <-|yx'] fderivable fC1 A. + by rewrite big_geq// subrr set_itv1 Rintegral_set1 subr0. +have x0' := le_lt_trans y0 yx'. +set p := `|floor y|; set q := `|floor x|. +have floory0: (0 <= floor y)%R by rewrite floor_ge0. +have floorx0: (0 <= floor x)%R by rewrite floor_ge0. +have py : (p%:R <= y)%R. + by rewrite -mulrz_nat natz gez0_abs ?floor_ge0// floor_le. +have yp : (y < p.+1%:R)%R. + by rewrite -natr1 -mulrz_nat natz -intrD1 gez0_abs// floorD1_gt. +have qx : (q%:R <= x)%R. + by rewrite -mulrz_nat natz gez0_abs ?floor_ge0// floor_le. +have xq : (x < q.+1%:R)%R. + by rewrite -natr1 -mulrz_nat natz -intrD1 gez0_abs// floorD1_gt. +have AteqAn: forall n t, (n%:R <= t < n.+1%:R)%R -> A t = A n%:R. + move=> n t /andP [] tb1 tb2. + have: floor t = n. + apply /floor_def /andP. split=> //. + by rewrite -natz natr1 mulrz_nat. + suff: @floor R n%:R = n by rewrite /A => -> ->. + by apply /(@intr_inj R) /eqP; rewrite -[_ == _]intrEfloor. +have pleq: p <= q by apply: lez_abs2 => //; apply: le_floor. +have fi: lebesgue_measure.-integrable `[y, x] (EFin \o f^`()). + by apply: continuous_compact_integrable => //; apply: segment_compact. +have fcontinuous: {in `]y, x[ : set R^o, continuous f}. + rewrite -continuous_open_subspace //. apply: derivable_within_continuous. + by case: fderivable. +have tfct1t2 : forall t1 t2, (y <= t1)%R -> (t1 <= t2)%R -> (t2 <= x)%R -> + \int_(x in `[t1, t2]) f^`() x = (f t2 - f t1)%R. + move=> t1 t2 ylet1. + rewrite /Rintegral le_eqVlt => /orP [/eqP ->|t1ltt2 t2lex]. + by rewrite subrr set_itv1 (integral_Sset1 t2). + rewrite (@continuous_FTC2 _ _ f)//. + by apply/(continuous_subspaceW _ fC1)/subset_itv; rewrite bnd_simp. + split. + - apply: (@in1_subset_itv _ _ _ `]y, x[%R); last first. + by case: fderivable. + by apply: subset_itv; rewrite bnd_simp. + - move: ylet1. rewrite le_eqVlt => /orP [/eqP <-|yltn]. + by case: fderivable. + apply/cvg_at_right_filter/fcontinuous. + rewrite inE/= in_itv/=. apply/andP. split=> //. + exact: (lt_le_trans t1ltt2). + - move: t2lex. rewrite le_eqVlt => /orP [/eqP ->|t2ltx]. + by case: fderivable. + apply: cvg_at_left_filter. apply: fcontinuous. + rewrite inE/= in_itv/=. apply/andP. split=> //. + exact: (le_lt_trans ylet1). +move: pleq. rewrite leq_eqVlt => /orP [/eqP|] pq. + rewrite pq big_geq; first exact: ltnSn. + suff AteqAx t : t \in `[y, x] -> A t = A x. + rewrite (AteqAx y); first by rewrite set_itvcc inE/= lexx. + under eq_Rintegral => t tyx do rewrite AteqAx//. + by rewrite RintegralZl//= -!mulrBr tfct1t2// subrr// mulr0. + rewrite inE/= in_itv/= => /andP[] yt tx. + rewrite !(AteqAn p)// ?[X in X.+1]pq; apply/andP; split=> //. + - exact: (le_trans py yt). + - exact: (le_lt_trans tx xq). + - exact: (le_trans py yx). +have ->: ((\sum_(p.+1 <= n < q.+1) a n * f n%:R)%R = + (A q%:R * f q%:R - A p%:R * f p.+1%:R)%R - + (\sum_(p.+1 <= n < q) A n%:R * (f n.+1%:R - f n%:R)))%R. + rewrite -sumrN /A !floor_nat Abel_discrete//. congr (_ + _)%R. + by under [RHS]eq_bigr do rewrite floor_nat -mulrN opprB. +rewrite big_nat. +under eq_bigr => i /andP [] plti iltq. + have yi : (y <= i%:R)%R by apply/(le_trans (ltW yp)); rewrite ler_nat. + have ix : (i.+1%:R <= x)%R by apply: (le_trans _ qx); rewrite ler_nat. + rewrite -tfct1t2// ?ler_nat//. + have {}fi: lebesgue_measure.-integrable `[i%:R, i.+1%:R] (EFin \o f^`()). + apply: (integrableS _ _ _ fi) => //. + by apply: subset_itv => //=; rewrite bnd_simp. + rewrite -RintegralZl// -Rintegral_itv_bndo_bndc. + apply: eq_integrable; first exact: measurable_itv. + by move=> t _ /=; rewrite EFinM. + apply: integrableZl; first exact: measurable_itv. + apply: (integrableS _ _ _ fi) => //. + by apply: subset_itv => //=; rewrite bnd_simp. + under eq_Rintegral => t. + rewrite set_itvco inE/= => /AteqAn <-. + over. + over. +rewrite -big_nat => /=. +have Afi: lebesgue_measure.-integrable (`[y, x] : set R^o) + (EFin \o (fun x0 : R^o => A x0 * f^`() x0)%R). + have /setIidl <-: `[y, x] `<=` `[p%:R, q.+1%:R[. + by apply: subset_itv; rewrite bnd_simp/=. + rewrite -[p%:R]mulrz_nat -[q.+1%:R]mulrz_nat itvzz_bnd_bigcupD1. + by rewrite ler_nat; apply/ltnW/(ltn_trans pq). + rewrite setI_bigcupr bigcup_mkord. + apply: integrable_bigsetU => i _; first exact: measurableI. + apply: eq_integrable; first exact: measurableI. + move=> t; rewrite inE/= => -[_]; rewrite in_itv/=. + by rewrite -!natrD !mulrz_nat addnS EFinM => /AteqAn ->. + apply: integrableZl; first exact: measurableI. + by apply: (integrableS _ _ _ fi) => //; apply: measurableI. +rewrite /Rintegral big_nat sum_fine => [i /andP[] pi iq//|]. + apply: integrable_fin_num => //. + apply: (integrableS _ _ _ Afi) => //. + apply: subset_itv; rewrite bnd_simp. + by apply/ltW/(lt_le_trans yp); rewrite ler_nat. + by apply: (le_trans _ qx); rewrite ler_nat. +rewrite -big_nat -integral_bigsetU_EFin //=; first exact: iota_uniq. +- apply /trivIsetP => i j _ _ /eqP ineqj. rewrite -subset0 => z/=. + rewrite !in_itv/= => -[] /andP[] iz zi /andP[] jz zj. + move: (le_lt_trans iz zj) (le_lt_trans jz zi). + by rewrite !ltr_nat => ij ji; apply/ineqj/anti_leq/andP; split. +- apply: measurable_int. + apply: (integrableS _ _ _ Afi) => //. + exact: bigsetU_measurable. + rewrite (big_addn 0) big_mkord. + rewrite -(bigcup_mkord _ (fun i => `[(i + p.+1)%:R, (i + p.+1).+1%:R[)). + apply: bigcup_sub => i/=; rewrite ltn_subRL addnC => ipq. + apply: subset_itv; rewrite bnd_simp. + by apply/ltW/(lt_le_trans yp); rewrite ler_nat leq_addl. + by apply: (le_trans _ qx); rewrite ler_nat. +rewrite (big_addn 0) big_mkord. +rewrite -(bigcup_mkord _ (fun i => `[(i + p.+1)%:R, (i + p.+1).+1%:R[)). +under eq_bigcupr do + rewrite addnC -addnS -mulrz_nat -[(_ + _.+1)%:R]mulrz_nat !natrD. +rewrite -(absz_nat (q - p.+1)) -natz natrB//. +rewrite -itvzz_bnd_bigcupD1; first by rewrite ler_nat. +rewrite !mulrz_nat -![fine _]/(Rintegral _ _ _). +have itvyq: `[y, p.+1%:R[ `|` `[p.+1%:R, q%:R[ = `[y, q%:R[. + by rewrite -itv_bndbnd_setU// bnd_simp// ?ler_nat// ltW. +have itvyx: `[y, x[ = `[y, p.+1%:R[ `|` `[p.+1%:R, q%:R[ `|` `[q%:R, x[. + rewrite itvyq -itv_bndbnd_setU// bnd_simp. + by apply/ltW/(lt_le_trans yp); rewrite ler_nat. +have ->: + (\int_(t in `[y, x]) (A t * f^`() t) = + \int_(t in `[y, p.+1%:R[) (A t * f^`() t) + + \int_(t in `[p.+1%:R, q%:R[) (A t * f^`() t) + + \int_(t in `[q%:R, x[) (A t * f^`() t))%R. + rewrite /Rintegral -integral_itv_bndo_bndc. + apply: (measurable_int (@lebesgue_measure R)). + apply: (integrableS _ _ _ Afi) => //. + by apply: subset_itv; rewrite bnd_simp//. + rewrite itvyx -![fine _]/(Rintegral _ _ _) !Rintegral_setU //=. + - exact: measurableU. + - rewrite -itvyx. + apply: (integrableS _ _ _ Afi) => //. + by apply: subset_itv; rewrite bnd_simp//. + - apply /disj_setPS => z. + rewrite itvyq => /= -[] /andP [] _ zq /andP [] qz _. + suff: (z < z)%R by rewrite ltxx. + exact: (lt_le_trans zq qz). + - rewrite itvyq. + apply: (integrableS _ _ _ Afi) => //. + by apply: subset_itv; rewrite bnd_simp//. + - apply /disj_setPS => z /= [] /andP [] _ zp /andP [] pz _. + suff: (z < z)%R by rewrite ltxx. + exact: (lt_le_trans zp pz). +under [in RHS]eq_Rintegral => t. + rewrite inE/= in_itv/= => /andP [] /(le_trans py) pt tp. + rewrite (AteqAn p) ?pt//. + over. +under [X in (_ = _ - (_ + _ + X))%R]eq_Rintegral => t. + rewrite inE/= in_itv/= => /andP [] qt tx. + rewrite (AteqAn q); first by rewrite qt; apply: (lt_trans tx). + over. +rewrite !RintegralZl //=. +- apply: (integrableS _ _ _ fi) => //. + apply: subset_itv; rewrite bnd_simp//=. + by apply: (le_trans _ qx); rewrite ler_nat. +- apply: (integrableS _ _ _ fi) => //. + apply: subset_itv; rewrite bnd_simp//=. + by apply: (le_trans (ltW yp)); rewrite ler_nat. +rewrite /Rintegral [in RHS]integral_itv_bndo_bndc. + apply: (measurable_int (@lebesgue_measure R)). + apply: (integrableS _ _ _ fi) => //. + apply: subset_itv; rewrite bnd_simp//=. + by apply: (le_trans _ qx); rewrite ler_nat. +rewrite [X in (A q%:R * fine X)%R]integral_itv_bndo_bndc. + apply: (measurable_int (@lebesgue_measure R)). + apply: (integrableS _ _ _ fi) => //. + apply: subset_itv; rewrite bnd_simp//=. + by apply: (le_trans (ltW yp)); rewrite ler_nat. +rewrite -![fine _]/(Rintegral _ _ _) !tfct1t2 //. +- exact: ltW. +- by apply: (le_trans _ qx); rewrite ler_nat. +- by apply: (le_trans (ltW yp)); rewrite ler_nat. +rewrite (AteqAn q x) ?qx// (AteqAn p y) ?py// !opprD !mulrBr !opprB !addrA. +by rewrite (AC 7 ((1*7)*(3*2)*6*4*5))/= !subrr !add0r. +Qed.