Skip to content

Commit d27d6e6

Browse files
TragicusTragicus
committed
discrete and continuous abel transforms
1 parent 903b60a commit d27d6e6

5 files changed

Lines changed: 302 additions & 4 deletions

File tree

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,15 @@
1919
- in `measurable_function.v`:
2020
+ lemma `preimage_measurability`
2121

22+
- in `real_interval.v`
23+
+ lemma `itvzz_bnd_bigcupD1`
24+
25+
- in `lebesgue_integrable.v`
26+
+ lemmas `integrable_setU`, `integrable_bigsetU`
27+
28+
- in `pnt.v`
29+
+ lemmas `Abel_discrete`, `Abel_continuous`
30+
2231
### Changed
2332

2433
- moved from `measurable_structure.v` to `classical_sets.v`:

‎classical/unstable.v‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ Set Implicit Arguments.
3535
Unset Strict Implicit.
3636
Unset Printing Implicit Defensive.
3737

38-
Import Order.TTheory GRing.Theory Num.Theory.
38+
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
3939
Local Open Scope ring_scope.
4040

4141
Section IntervalNumDomain.
@@ -592,3 +592,10 @@ Proof. exact: real_ltr_bound. Qed.
592592

593593
Lemma ltrNbound {R : archiRealDomainType} (x : R) : - x < (Num.bound x)%:R.
594594
Proof. exact: real_ltrNbound. Qed.
595+
596+
Lemma floor_nat (R : archiNumDomainType) n : absz (floor (n%:R : R)) = n.
597+
Proof.
598+
apply: (can_inj absz_nat).
599+
rewrite gez0_abs; first by rewrite real_floor_ge0.
600+
by apply /(@intr_inj R) /eqP; rewrite -[_ == _]intrEfloor.
601+
Qed.

‎reals/real_interval.v‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -322,3 +322,24 @@ Proof.
322322
rewrite -subTset => x _ /=; exists (Num.bound x) => //=.
323323
by rewrite in_itv lteifNl 2?lteifS// (ltr_bound, ltrNbound).
324324
Qed.
325+
326+
Lemma itvzz_bnd_bigcupD1 (R : realType) (x y : int) :
327+
(x <= y)%R ->
328+
`[x%:~R, y%:~R[%classic =
329+
(\bigcup_(i < `|(y - x)%R|)
330+
`[(x + i%:R)%:~R, (x + i.+1%:R)%:~R[)%classic :> set R.
331+
Proof.
332+
rewrite predeqE => xy z/=. rewrite in_itv/=.
333+
split=> [/andP[xz zy]|[] i /=]; last first.
334+
rewrite -(ltr_nat int) [(`|_|%:R)%R]natz gez0_abs ?subr_ge0//.
335+
rewrite -lezD1 natr1 => iyx; rewrite in_itv/= => /andP[xz zx].
336+
apply/andP; split; first by apply: (le_trans _ xz); rewrite ler_int lerDl.
337+
by apply: (lt_le_trans zx); rewrite ler_int -lerBrDl.
338+
exists (`|floor (z - x%:~R)|)%N => /=.
339+
rewrite -(ltr_nat int) !natz !gez0_abs ?floor_ge0 ?subr_ge0//.
340+
rewrite -(ltr_int R) intrB.
341+
by apply/(le_lt_trans (floor_le _)); rewrite ltrD2r.
342+
rewrite -natr1 natz gez0_abs; first by rewrite floor_ge0 subr_ge0.
343+
rewrite -[X in X \in _](subrK x%:~R) addrC in_itv/= 2!intrD.
344+
by rewrite lerD2l ltrD2l floor_itv.
345+
Qed.

‎theories/lebesgue_integral_theory/lebesgue_integrable.v‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -445,6 +445,45 @@ apply: le_lt_trans ifoo; apply: ge0_subset_integral => //.
445445
exact: measurableT_comp.
446446
Qed.
447447

448+
Lemma integrable_setU (E D : set T) (f : T -> \bar R) :
449+
d.-measurable E ->
450+
d.-measurable D ->
451+
mu.-integrable (E `|` D) f <-> mu.-integrable E f /\ mu.-integrable D f.
452+
Proof.
453+
move=> ??; split=> [fi|[]].
454+
by split; apply: (integrableS _ _ _ fi) => //; apply: measurableU.
455+
move=> /integrableP[] fmE fiE /integrableP[] fmD fiD.
456+
apply/integrableP; split; first exact/measurable_funU.
457+
have ED: E `|` D = E `|` (D `\` E).
458+
by rewrite -(setDUK (@subsetUl _ E D)) setDUD setDv set0U.
459+
rewrite ED ge0_integral_setU//.
460+
- exact: measurableD.
461+
- apply: (measurable_comp measurableT) => //.
462+
by rewrite -ED; apply/measurable_funU.
463+
- by apply/disj_setPRL; apply: subIsetr.
464+
apply: lte_add_pinfty => //.
465+
apply/(le_lt_trans _ fiD); apply/ge0_subset_integral => //.
466+
exact: measurableD.
467+
exact: (measurable_comp measurableT).
468+
Qed.
469+
470+
(* TOTHINK: The equivalence is painful to state because I need to filter s.
471+
However, the reciprocal is a consequence of `integrableS`, so maybe we do
472+
not care. *)
473+
Lemma integrable_bigsetU (I : Type) (s : seq I) (P : pred I) (D : I -> set T)
474+
(f : T -> \bar R) :
475+
(forall i, P i -> d.-measurable (D i)) ->
476+
(forall i, P i -> mu.-integrable (D i) f) ->
477+
mu.-integrable (\big[setU/set0]_(i <- s | P i) D i) f.
478+
Proof.
479+
move=> Dm fi.
480+
elim: s => [|i s IHs]; first by rewrite big_nil; apply: integrable_set0.
481+
rewrite big_cons; case: ifP => // iP.
482+
apply/integrable_setU; first exact: Dm.
483+
by apply: bigsetU_measurable.
484+
by split=> //; apply: fi.
485+
Qed.
486+
448487
Lemma integrable_mkcond D f : measurable D ->
449488
mu.-integrable D f <-> mu.-integrable setT (f \_ D).
450489
Proof.

‎theories/showcase/pnt.v‎

Lines changed: 225 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11
From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval.
22
#[warning="-warn-library-file-internal-analysis"]
3-
From mathcomp Require Import unstable.
4-
From mathcomp Require Import classical_sets boolp topology.
5-
From mathcomp Require Import ereal sequences reals.
3+
From mathcomp Require Import archimedean mathcomp_extra unstable.
4+
From mathcomp Require Import classical_sets boolp topology measure_function.
5+
From mathcomp Require Import set_interval normed_module.
6+
From mathcomp Require Import pseudometric_normed_Zmodule measurable_function.
7+
From mathcomp Require Import measurable_realfun measurable_structure .
8+
From mathcomp Require Import derive lebesgue_measure lebesgue_integral ftc.
9+
From mathcomp Require Import ereal sequences reals realfun real_interval.
610
Import Order.POrderTheory GRing.Theory Num.Theory.
711

812
(**md**************************************************************************)
@@ -23,6 +27,10 @@ Set Implicit Arguments.
2327
Unset Strict Implicit.
2428
Unset Printing Implicit Defensive.
2529

30+
Import Num.Def.
31+
Local Open Scope ring_scope.
32+
Local Open Scope ereal_scope.
33+
Local Open Scope order_scope.
2634
Local Open Scope classical_set_scope.
2735
Local Open Scope set_scope.
2836
Local Open Scope nat_scope.
@@ -452,3 +460,217 @@ apply: (@cardG R); first by move: Rklthalf; rewrite /un div1r.
452460
Qed.
453461

454462
End dvg_sum_inv_prime_seq.
463+
464+
Lemma Abel_discrete (R : comPzRingType) (a b : nat -> R) (n p : nat) :
465+
p < n -> let A n := (\sum_(0 <= k < n.+1) a k)%R in
466+
(\sum_(p.+1 <= k < n.+1) (a k) * (b k) = A n * b n - A p * b p.+1
467+
+ \sum_(p.+1 <= k < n) A k * (b k - b k.+1))%R.
468+
Proof.
469+
move=> ngtp A.
470+
rewrite big_nat_cond.
471+
under eq_bigr => k /andP [] /andP [] pk _ _.
472+
rewrite (_ : a k = (A k - A k.-1)%R) ?mulrBl.
473+
by rewrite /A (ltn_predK pk) // big_nat_recr //= [RHS]addrC addKr.
474+
over.
475+
rewrite -big_nat_cond.
476+
under [in RHS]eq_bigr do rewrite mulrBr.
477+
rewrite !big_split !sumrN /= [X in (_ - X)%R]big_add1 -pred_Sn.
478+
under [X in (_ - X)%R]eq_bigr do rewrite -pred_Sn.
479+
by rewrite [RHS](AC (2*2) ((3*1)*(2*4)))/= -big_nat_recr//= -opprD -big_ltn.
480+
Qed.
481+
482+
Local Notation "\int_( x 'in' D ) F" := (\int[lebesgue_measure]_(x in D) F)%R
483+
(at level 36, F at level 36, x, D at level 50).
484+
485+
Lemma Abel_continuous (R : realType) (x y : R^o) (f : R^o -> R^o)
486+
(a : nat -> R) : (0 <= y <= x)%R -> derivable_oo_LRcontinuous f y x ->
487+
{within `[y, x] : set R^o, continuous f^`()} ->
488+
let A := fun x : R => (\sum_(0 <= n < `|floor x|.+1) a n)%R in
489+
(\sum_(`|floor y|.+1 <= n < `|floor x|.+1) a n * f n%:R =
490+
A x * f x - A y * f y - \int_(t in `[y, x]) (A t * f^`() t))%R.
491+
Proof.
492+
move=> /andP [] y0 /[dup] /(le_trans y0) x0 /[dup] yx.
493+
rewrite le_eqVlt => /orP[/eqP <-|yx'] fderivable fC1 A.
494+
by rewrite big_geq// subrr set_itv1 Rintegral_set1 subr0.
495+
have x0' := le_lt_trans y0 yx'.
496+
set p := `|floor y|; set q := `|floor x|.
497+
have floory0: (0 <= floor y)%R by rewrite floor_ge0.
498+
have floorx0: (0 <= floor x)%R by rewrite floor_ge0.
499+
have py : (p%:R <= y)%R.
500+
by rewrite -mulrz_nat natz gez0_abs ?floor_ge0// floor_le.
501+
have yp : (y < p.+1%:R)%R.
502+
by rewrite -natr1 -mulrz_nat natz -intrD1 gez0_abs// floorD1_gt.
503+
have qx : (q%:R <= x)%R.
504+
by rewrite -mulrz_nat natz gez0_abs ?floor_ge0// floor_le.
505+
have xq : (x < q.+1%:R)%R.
506+
by rewrite -natr1 -mulrz_nat natz -intrD1 gez0_abs// floorD1_gt.
507+
have AteqAn: forall n t, (n%:R <= t < n.+1%:R)%R -> A t = A n%:R.
508+
move=> n t /andP [] tb1 tb2.
509+
have: floor t = n.
510+
apply /floor_def /andP. split=> //.
511+
by rewrite -natz natr1 mulrz_nat.
512+
suff: @floor R n%:R = n by rewrite /A => -> ->.
513+
by apply /(@intr_inj R) /eqP; rewrite -[_ == _]intrEfloor.
514+
have pleq: p <= q by apply: lez_abs2 => //; apply: le_floor.
515+
have fi: lebesgue_measure.-integrable `[y, x] (EFin \o f^`()).
516+
by apply: continuous_compact_integrable => //; apply: segment_compact.
517+
have fcontinuous: {in `]y, x[ : set R^o, continuous f}.
518+
rewrite -continuous_open_subspace //. apply: derivable_within_continuous.
519+
by case: fderivable.
520+
have tfct1t2 : forall t1 t2, (y <= t1)%R -> (t1 <= t2)%R -> (t2 <= x)%R ->
521+
\int_(x in `[t1, t2]) f^`() x = (f t2 - f t1)%R.
522+
move=> t1 t2 ylet1.
523+
rewrite /Rintegral le_eqVlt => /orP [/eqP ->|t1ltt2 t2lex].
524+
by rewrite subrr set_itv1 (integral_Sset1 t2).
525+
rewrite (@continuous_FTC2 _ _ f)//.
526+
by apply/(continuous_subspaceW _ fC1)/subset_itv; rewrite bnd_simp.
527+
split.
528+
- apply: (@in1_subset_itv _ _ _ `]y, x[%R); last first.
529+
by case: fderivable.
530+
by apply: subset_itv; rewrite bnd_simp.
531+
- move: ylet1. rewrite le_eqVlt => /orP [/eqP <-|yltn].
532+
by case: fderivable.
533+
apply/cvg_at_right_filter/fcontinuous.
534+
rewrite inE/= in_itv/=. apply/andP. split=> //.
535+
exact: (lt_le_trans t1ltt2).
536+
- move: t2lex. rewrite le_eqVlt => /orP [/eqP ->|t2ltx].
537+
by case: fderivable.
538+
apply: cvg_at_left_filter. apply: fcontinuous.
539+
rewrite inE/= in_itv/=. apply/andP. split=> //.
540+
exact: (le_lt_trans ylet1).
541+
move: pleq. rewrite leq_eqVlt => /orP [/eqP|] pq.
542+
rewrite pq big_geq; first exact: ltnSn.
543+
suff AteqAx t : t \in `[y, x] -> A t = A x.
544+
rewrite (AteqAx y); first by rewrite set_itvcc inE/= lexx.
545+
under eq_Rintegral => t tyx do rewrite AteqAx//.
546+
by rewrite RintegralZl//= -!mulrBr tfct1t2// subrr// mulr0.
547+
rewrite inE/= in_itv/= => /andP[] yt tx.
548+
rewrite !(AteqAn p)// ?[X in X.+1]pq; apply/andP; split=> //.
549+
- exact: (le_trans py yt).
550+
- exact: (le_lt_trans tx xq).
551+
- exact: (le_trans py yx).
552+
have ->: ((\sum_(p.+1 <= n < q.+1) a n * f n%:R)%R =
553+
(A q%:R * f q%:R - A p%:R * f p.+1%:R)%R -
554+
(\sum_(p.+1 <= n < q) A n%:R * (f n.+1%:R - f n%:R)))%R.
555+
rewrite -sumrN /A !floor_nat Abel_discrete//. congr (_ + _)%R.
556+
by under [RHS]eq_bigr do rewrite floor_nat -mulrN opprB.
557+
rewrite big_nat.
558+
under eq_bigr => i /andP [] plti iltq.
559+
have yi : (y <= i%:R)%R by apply/(le_trans (ltW yp)); rewrite ler_nat.
560+
have ix : (i.+1%:R <= x)%R by apply: (le_trans _ qx); rewrite ler_nat.
561+
rewrite -tfct1t2// ?ler_nat//.
562+
have {}fi: lebesgue_measure.-integrable `[i%:R, i.+1%:R] (EFin \o f^`()).
563+
apply: (integrableS _ _ _ fi) => //.
564+
by apply: subset_itv => //=; rewrite bnd_simp.
565+
rewrite -RintegralZl// -Rintegral_itv_bndo_bndc.
566+
apply: eq_integrable; first exact: measurable_itv.
567+
by move=> t _ /=; rewrite EFinM.
568+
apply: integrableZl; first exact: measurable_itv.
569+
apply: (integrableS _ _ _ fi) => //.
570+
by apply: subset_itv => //=; rewrite bnd_simp.
571+
under eq_Rintegral => t.
572+
rewrite set_itvco inE/= => /AteqAn <-.
573+
over.
574+
over.
575+
rewrite -big_nat => /=.
576+
have Afi: lebesgue_measure.-integrable (`[y, x] : set R^o)
577+
(EFin \o (fun x0 : R^o => A x0 * f^`() x0)%R).
578+
have /setIidl <-: `[y, x] `<=` `[p%:R, q.+1%:R[.
579+
by apply: subset_itv; rewrite bnd_simp/=.
580+
rewrite -[p%:R]mulrz_nat -[q.+1%:R]mulrz_nat itvzz_bnd_bigcupD1.
581+
by rewrite ler_nat; apply/ltnW/(ltn_trans pq).
582+
rewrite setI_bigcupr bigcup_mkord.
583+
apply: integrable_bigsetU => i _; first exact: measurableI.
584+
apply: eq_integrable; first exact: measurableI.
585+
move=> t; rewrite inE/= => -[_]; rewrite in_itv/=.
586+
by rewrite -!natrD !mulrz_nat addnS EFinM => /AteqAn ->.
587+
apply: integrableZl; first exact: measurableI.
588+
by apply: (integrableS _ _ _ fi) => //; apply: measurableI.
589+
rewrite /Rintegral big_nat sum_fine => [i /andP[] pi iq//|].
590+
apply: integrable_fin_num => //.
591+
apply: (integrableS _ _ _ Afi) => //.
592+
apply: subset_itv; rewrite bnd_simp.
593+
by apply/ltW/(lt_le_trans yp); rewrite ler_nat.
594+
by apply: (le_trans _ qx); rewrite ler_nat.
595+
rewrite -big_nat -integral_bigsetU_EFin //=; first exact: iota_uniq.
596+
- apply /trivIsetP => i j _ _ /eqP ineqj. rewrite -subset0 => z/=.
597+
rewrite !in_itv/= => -[] /andP[] iz zi /andP[] jz zj.
598+
move: (le_lt_trans iz zj) (le_lt_trans jz zi).
599+
by rewrite !ltr_nat => ij ji; apply/ineqj/anti_leq/andP; split.
600+
- apply: measurable_int.
601+
apply: (integrableS _ _ _ Afi) => //.
602+
exact: bigsetU_measurable.
603+
rewrite (big_addn 0) big_mkord.
604+
rewrite -(bigcup_mkord _ (fun i => `[(i + p.+1)%:R, (i + p.+1).+1%:R[)).
605+
apply: bigcup_sub => i/=; rewrite ltn_subRL addnC => ipq.
606+
apply: subset_itv; rewrite bnd_simp.
607+
by apply/ltW/(lt_le_trans yp); rewrite ler_nat leq_addl.
608+
by apply: (le_trans _ qx); rewrite ler_nat.
609+
rewrite (big_addn 0) big_mkord.
610+
rewrite -(bigcup_mkord _ (fun i => `[(i + p.+1)%:R, (i + p.+1).+1%:R[)).
611+
under eq_bigcupr do
612+
rewrite addnC -addnS -mulrz_nat -[(_ + _.+1)%:R]mulrz_nat !natrD.
613+
rewrite -(absz_nat (q - p.+1)) -natz natrB//.
614+
rewrite -itvzz_bnd_bigcupD1; first by rewrite ler_nat.
615+
rewrite !mulrz_nat -![fine _]/(Rintegral _ _ _).
616+
have itvyq: `[y, p.+1%:R[ `|` `[p.+1%:R, q%:R[ = `[y, q%:R[.
617+
by rewrite -itv_bndbnd_setU// bnd_simp// ?ler_nat// ltW.
618+
have itvyx: `[y, x[ = `[y, p.+1%:R[ `|` `[p.+1%:R, q%:R[ `|` `[q%:R, x[.
619+
rewrite itvyq -itv_bndbnd_setU// bnd_simp.
620+
by apply/ltW/(lt_le_trans yp); rewrite ler_nat.
621+
have ->:
622+
(\int_(t in `[y, x]) (A t * f^`() t) =
623+
\int_(t in `[y, p.+1%:R[) (A t * f^`() t) +
624+
\int_(t in `[p.+1%:R, q%:R[) (A t * f^`() t) +
625+
\int_(t in `[q%:R, x[) (A t * f^`() t))%R.
626+
rewrite /Rintegral -integral_itv_bndo_bndc.
627+
apply: (measurable_int (@lebesgue_measure R)).
628+
apply: (integrableS _ _ _ Afi) => //.
629+
by apply: subset_itv; rewrite bnd_simp//.
630+
rewrite itvyx -![fine _]/(Rintegral _ _ _) !Rintegral_setU //=.
631+
- exact: measurableU.
632+
- rewrite -itvyx.
633+
apply: (integrableS _ _ _ Afi) => //.
634+
by apply: subset_itv; rewrite bnd_simp//.
635+
- apply /disj_setPS => z.
636+
rewrite itvyq => /= -[] /andP [] _ zq /andP [] qz _.
637+
suff: (z < z)%R by rewrite ltxx.
638+
exact: (lt_le_trans zq qz).
639+
- rewrite itvyq.
640+
apply: (integrableS _ _ _ Afi) => //.
641+
by apply: subset_itv; rewrite bnd_simp//.
642+
- apply /disj_setPS => z /= [] /andP [] _ zp /andP [] pz _.
643+
suff: (z < z)%R by rewrite ltxx.
644+
exact: (lt_le_trans zp pz).
645+
under [in RHS]eq_Rintegral => t.
646+
rewrite inE/= in_itv/= => /andP [] /(le_trans py) pt tp.
647+
rewrite (AteqAn p) ?pt//.
648+
over.
649+
under [X in (_ = _ - (_ + _ + X))%R]eq_Rintegral => t.
650+
rewrite inE/= in_itv/= => /andP [] qt tx.
651+
rewrite (AteqAn q); first by rewrite qt; apply: (lt_trans tx).
652+
over.
653+
rewrite !RintegralZl //=.
654+
- apply: (integrableS _ _ _ fi) => //.
655+
apply: subset_itv; rewrite bnd_simp//=.
656+
by apply: (le_trans _ qx); rewrite ler_nat.
657+
- apply: (integrableS _ _ _ fi) => //.
658+
apply: subset_itv; rewrite bnd_simp//=.
659+
by apply: (le_trans (ltW yp)); rewrite ler_nat.
660+
rewrite /Rintegral [in RHS]integral_itv_bndo_bndc.
661+
apply: (measurable_int (@lebesgue_measure R)).
662+
apply: (integrableS _ _ _ fi) => //.
663+
apply: subset_itv; rewrite bnd_simp//=.
664+
by apply: (le_trans _ qx); rewrite ler_nat.
665+
rewrite [X in (A q%:R * fine X)%R]integral_itv_bndo_bndc.
666+
apply: (measurable_int (@lebesgue_measure R)).
667+
apply: (integrableS _ _ _ fi) => //.
668+
apply: subset_itv; rewrite bnd_simp//=.
669+
by apply: (le_trans (ltW yp)); rewrite ler_nat.
670+
rewrite -![fine _]/(Rintegral _ _ _) !tfct1t2 //.
671+
- exact: ltW.
672+
- by apply: (le_trans _ qx); rewrite ler_nat.
673+
- by apply: (le_trans (ltW yp)); rewrite ler_nat.
674+
rewrite (AteqAn q x) ?qx// (AteqAn p y) ?py// !opprD !mulrBr !opprB !addrA.
675+
by rewrite (AC 7 ((1*7)*(3*2)*6*4*5))/= !subrr !add0r.
676+
Qed.

0 commit comments

Comments
 (0)