Module FormalML.utils.Sums

Require Import Coquelicot.Coquelicot.
Set Bullet Behavior "Strict Subproofs".
Require Import Morphisms.
Require Import Program.
Require Import Coq.Reals.Rbase.
Require Import Coq.Reals.Rfunctions.
Require Import List.
Require Import EquivDec Nat Lia Lra.
Require Import Reals.R_sqrt.
Require Import PushNeg.
Require Import Reals.Sqrt_reg.

Require FinFun.

Require Import LibUtils ListAdd RealAdd.
Import ListNotations.

Local Open Scope R.

Section sum'.
  Fixpoint sum_f_R0' (f : nat -> R) (N : nat) {struct N} : R :=
    match N with
    | 0%nat => 0%R
    | S i => sum_f_R0' f i + f i
    end.

  Lemma sum_f_R0_sum_f_R0' f N :
    sum_f_R0 f N = sum_f_R0' f (S N).

  Lemma sum_f_R0'_ext (f1 f2:nat->R) n :
    (forall x, (x < n)%nat -> f1 x = f2 x) ->
    sum_f_R0' f1 n = sum_f_R0' f2 n.

  Lemma sum_f_R0'_split f n m :
    (m <= n)%nat ->
    sum_f_R0' f n =
    sum_f_R0' f m +
    sum_f_R0' (fun x => f (x+m)%nat) (n-m).

  Lemma sum_f_R0'_split_on f n m :
    (m < n)%nat ->
    sum_f_R0' f n =
    sum_f_R0' f m +
    f m +
    sum_f_R0' (fun x => f (x+S m)%nat) (n- S m).

  Lemma sum_f_R0_peel f n :
    sum_f_R0 f (S n) = sum_f_R0 f n + f (S n).

  Lemma sum_f_R0_ext (f1 f2:nat->R) n :
    (forall x, (x <= n)%nat -> f1 x = f2 x) ->
    sum_f_R0 f1 n = sum_f_R0 f2 n.

  Lemma sum_f_R0_split f n m:
    (m < n)%nat ->
    sum_f_R0 f n =
    sum_f_R0 f m +
    sum_f_R0 (fun x => f (x+S m))%nat (n-S m).

    Lemma sum_f_R0_le (f g : nat -> R) n :
      (forall (i:nat), (i<=n)%nat -> (f i) <= (g i)) ->
      sum_f_R0 f n <= sum_f_R0 g n.

    Lemma sum_f_R0_nneg f N :
      (forall n, (n<=N)%nat -> 0 <= f n) ->
      0 <= sum_f_R0 f N.

   Lemma sum_f_R0_pos_incr f :
      (forall i, 0 <= f i) ->
      forall n : nat, sum_f_R0 f n <= sum_f_R0 f (S n).

  Lemma sum_f_R0_split_on f n m:
    (S m < n)%nat ->
    sum_f_R0 f n =
    sum_f_R0 f m +
    f (S m) +
    sum_f_R0 (fun x => f (x+S (S m)))%nat (n-S (S m)).

  Lemma sum_f_R0'_chisel f N n :
  (n < N)%nat ->
  sum_f_R0' f N = sum_f_R0' (fun x : nat => if equiv_dec x n then 0 else f x) N + (f n).

  Lemma sum_f_R0'_const c n: sum_f_R0' (fun _ : nat => c) n = (c * INR n)%R.

    
  Lemma sum_f'_as_fold_right f (n:nat) s :
    sum_f_R0' (fun x : nat => f (x + s)%nat) n = fold_right (fun a b => f a + b) 0 (seq s n).

  Lemma sum_f_R0'_as_fold_right f (n:nat) :
    sum_f_R0' f n = fold_right (fun a b => f a + b) 0 (seq 0 n).

  Lemma sum_f_R0'_plus f1 f2 n :
    sum_f_R0' (fun x => f1 x + f2 x) n = sum_f_R0' f1 n + sum_f_R0' f2 n.

  Lemma sum_f_R0'_mult_const f1 n c :
    sum_f_R0' (fun x => c * f1 x) n = c * sum_f_R0' f1 n.

  Lemma sum_f_R0_mult_const f1 n c :
    sum_f_R0 (fun x => c * f1 x) n = c * sum_f_R0 f1 n.

  Lemma sum_f_R0'_le f n :
    (forall n, (0 <= f n)) ->
    0 <= sum_f_R0' f n.

  Lemma sum_f_R0'_plus_n f n1 n2 : sum_f_R0' f (n1 + n2) =
                                   sum_f_R0' f n1 +
                                   sum_f_R0' (fun x => f (n1+x))%nat n2.

  Lemma sum_f_R0'_le_f (f g:nat->R) n :
    (forall i, (i < n)%nat -> f i <= g i) ->
    sum_f_R0' f n <= sum_f_R0' g n.

End sum'.

Section inf_sum'.

  Definition infinite_sum' (s : nat -> R) (l : R) : Prop
    := forall eps : R,
      eps > 0 ->
      exists N : nat,
        forall n : nat,
          (n >= N)%nat ->
          R_dist (sum_f_R0' s n) l < eps.

  Theorem infinite_sum_infinite_sum' (s : nat -> R) (l : R) :
    infinite_sum s l <-> infinite_sum' s l.

  Lemma infinite_sum'_ext (s1 s2 : nat -> R) (l : R) :
    (forall x, s1 x = s2 x) ->
    infinite_sum' s1 l <-> infinite_sum' s2 l.
    

  Lemma infinite_sum'_prefix s l n :
    infinite_sum' s (l + (sum_f_R0' s n)) <->
    infinite_sum' (fun x => s (x + n))%nat l.
    
    Lemma infinite_sum'_split n s l :
      infinite_sum' s l <->
      infinite_sum' (fun x => s (x + n))%nat (l - (sum_f_R0' s n)).


    Lemma R_dist_too_small_impossible_lt r l1 l2 :
      l1 < l2 ->
      R_dist r l1 < R_dist l1 l2 / 2 ->
      R_dist r l2 < R_dist l1 l2 / 2 -> False.
             
    Lemma R_dist_too_small_impossible_neq r l1 l2 :
      l1 <> l2 ->
      R_dist r l1 < R_dist l1 l2 / 2 ->
      R_dist r l2 < R_dist l1 l2 / 2 -> False.
                                                     
    Lemma infinite_sum'_unique {f l1 l2} :
      infinite_sum' f l1 ->
      infinite_sum' f l2 ->
      l1 = l2.

    Lemma infinite_sum'_const_shift {c d} :
      infinite_sum' (fun _ => c) d ->
      (infinite_sum' (fun _ => c) (d+c)).

    Lemma infinite_sum'_const0 {d} :
      infinite_sum' (fun _ : nat => 0) d ->
      d = 0.

    Lemma infinite_sum'_const1 {c d} :
      infinite_sum' (fun _ => c) d -> c = 0.

    Lemma infinite_sum'_const {c d} :
      infinite_sum' (fun _ => c) d -> c = 0 /\ d = 0.

    Lemma infinite_sum'_const2 {c d} :
      infinite_sum' (fun _ => c) d -> d = 0.

  Hint Resolve Nat.le_max_l Nat.le_max_r : arith.
    
  Lemma infinite_sum'_plus {f1 f2} {sum1 sum2} :
    infinite_sum' f1 sum1 ->
    infinite_sum' f2 sum2 ->
    infinite_sum' (fun x => f1 x + f2 x) (sum1 + sum2).

  Lemma infinite_sum'0 : infinite_sum' (fun _ : nat => 0) 0.
        
  Lemma infinite_sum'_mult_const {f1} {sum1} c :
    infinite_sum' f1 sum1 ->
    infinite_sum' (fun x => c * f1 x) (c * sum1).
     
  Lemma Rabs_pos_plus_lt x y :
    x > 0 ->
    y > 0 ->
    y < Rabs (x + y).

  Lemma infinite_sum'_pos f sum :
    infinite_sum' f sum ->
    (forall n, (0 <= f n)) ->
    0 <= sum.

  Lemma infinite_sum'_le f1 f2 sum1 sum2 :
    infinite_sum' f1 sum1 ->
    infinite_sum' f2 sum2 ->
    (forall n, (f1 n <= f2 n)) ->
    sum1 <= sum2.
  
End inf_sum'.

Section harmonic.

  Lemma pow_le1 n : (1 <= 2 ^ n)%nat.

  Lemma Sle_mult_gt1 a n :
    (n > 0)%nat ->
    (a > 1)%nat ->
    (S n <= a * n)%nat.

  Lemma pow_exp_gt a b :
    (a > 1)%nat ->
    (a ^ b > b)%nat.
  Lemma sum_f_R0'_eq2 n :
    sum_f_R0' (fun _:nat => 1 / INR (2^(S n))) (2^n)%nat = 1/2.
  
  Lemma sum_f_R0'_bound2 (n:nat) : sum_f_R0' (fun i:nat => 1 / INR (S i)) (2^n)%nat >= 1+(INR n)/2.

  Lemma harmonic_diverges' l : ~ infinite_sum' (fun i:nat => 1 / INR (S i)) l.

  
  Definition diverges (f:nat->R)
    := forall l, ~ infinite_sum f l.
  
  Theorem harmonic_diverges : diverges (fun i:nat => 1 / INR (S i)).

End harmonic.

Section coquelicot.
Lemma infinite_sum_is_lim_seq (f:nat->R) (l:R) : is_lim_seq (fun i => sum_f_R0 f i) l <-> infinite_sum f l.

Lemma is_lim_seq_list_sum (l:list (nat->R)) (l2:list R) :
  Forall2 is_lim_seq l (map Finite l2) ->
  is_lim_seq (fun n => list_sum (map (fun x => x n) l)) (list_sum l2).

End coquelicot.

Lemma infinite_sum'_one f n l :
  (forall n', n' <> n -> f n' = 0%R) ->
  infinite_sum' f l <-> l = f n.

Lemma infinite_sum'_pos_prefix_le f l n:
  infinite_sum' f l ->
  (forall n, 0 <= f n) ->
  sum_f_R0' f n <= l.

Lemma infinite_sum'_pos_one_le f l n:
  infinite_sum' f l ->
  (forall n, 0 <= f n) ->
  f n <= l.

Lemma sum_f_R0'_list_sum f n :
  sum_f_R0' f n = list_sum (map f (seq 0 n)).

Lemma list_sum_pos_sublist_le l1 l2 :
  (forall x, In x l2 -> 0 <= x) ->
  sublist l1 l2 ->
  list_sum l1 <= list_sum l2.

Lemma list_sum_Rabs_triangle l :
  Rabs (list_sum l) <= list_sum (map Rabs l).

Lemma bijective_injective {B C} (f:B->C) : FinFun.Bijective f -> FinFun.Injective f.

Theorem infinite_sum'_perm (g:nat->nat) (f:nat -> R) l:
  FinFun.Bijective g ->
  (exists l2, infinite_sum' (fun x => Rabs (f x)) l2) ->
  infinite_sum' f l ->
  infinite_sum' (fun n => f (g n)) l.

Corollary infinite_sum'_pos_perm (g:nat->nat) (f:nat -> R) l:
  FinFun.Bijective g ->
  (forall x, 0 <= f x) ->
  infinite_sum' f l ->
  infinite_sum' (fun n => f (g n)) l.

Lemma sum_f_R0_0_inv (a:nat->R) :
  (forall n : nat, sum_f_R0 a n = 0) ->
  forall n, a n = 0.


Section sum_n.


    Lemma sum_n_le_loc (a b : nat -> R) (k : nat) :
  (forall n : nat, (n <= k)%nat -> a n <= b n) ->
  sum_n a k <= sum_n b k.

Lemma sum_n_m_le_loc_alt (a b : nat -> R) (j k : nat) :
  (forall n : nat, (j <= n <= j + k)%nat -> a n <= b n) ->
  sum_n_m a j (j + k)%nat <= sum_n_m b j (j + k)%nat.

Lemma sum_n_m_le_loc (a b : nat -> R) (j k : nat) :
  (j <= k)%nat ->
  (forall n : nat, (j <= n <= k)%nat -> a n <= b n) ->
  sum_n_m a j k <= sum_n_m b j k.
Lemma sum_n_m_fold_right_seq (f:nat->R) n m:
  sum_n_m (fun n0 : nat => f n0) m n =
  fold_right Rplus 0 (map f (List.seq m (S n - m))).

Lemma sum_n_fold_right_seq (f:nat->R) n :
  sum_n (fun n0 : nat => f n0) n =
  fold_right Rplus 0 (map f (seq 0 (S n))).

Lemma list_sum_sum_n (l:list R) :
  list_sum l =
  @Hierarchy.sum_n Hierarchy.R_AbelianGroup (fun i:nat => match nth_error l i with
                                                          | Some x => x
                                                          | None => 0%R
                                                          end) (length l).


Lemma sum_n_m_shift (α : nat -> R) (k n0 : nat) :
  sum_n_m α k (n0 + k)%nat = sum_n (fun n1 : nat => α (n1 + k)%nat) n0.

Lemma sum_n_m_pos a n1 n2 :
  (forall n, (n1 <= n <= n2)%nat -> 0 <= a n) ->
  0 <= (sum_n_m a n1 n2).


Lemma sum_n_pos_incr a n1 n2 : (forall n, (n1 < n <= n2)%nat -> 0 <= a n) ->
                               (n1 <= n2)%nat -> sum_n a n1 <= sum_n a n2.

End sum_n.


Section Sequences.

  Global Instance is_lim_seq_proper:
    Proper (pointwise_relation _ eq ==> eq ==> iff) (is_lim_seq).

  Global Instance Lim_seq_proper:
    Proper (pointwise_relation _ eq ==> eq) (Lim_seq).

  Global Instance ex_lim_seq_proper:
    Proper (pointwise_relation _ eq ==> iff) (ex_lim_seq).


  Lemma sup_seq_pos (f : nat -> R) :
    (forall n, 0 <= f n) ->
    Rbar_le 0 (Sup_seq f).

  Lemma ex_finite_lim_seq_bounded (f : nat -> R) :
    ex_finite_lim_seq f ->
    exists (M:R),
    forall n, Rabs (f n) <= M.

  Lemma ex_finite_lim_seq_plus (f g : nat -> R) :
    ex_finite_lim_seq f ->
    ex_finite_lim_seq g ->
    ex_finite_lim_seq (fun n => f n + g n).

 Lemma ex_finite_lim_seq_ext (f g : nat -> R) :
    (forall n, f n = g n) ->
    ex_finite_lim_seq f <-> ex_finite_lim_seq g.

  Lemma ex_finite_lim_seq_S (f : nat -> R) :
    ex_finite_lim_seq f <-> ex_finite_lim_seq (fun n => f (S n)).

Lemma ex_finite_lim_seq_incr_n (f : nat -> R) (N : nat) :
  ex_finite_lim_seq f <-> ex_finite_lim_seq (fun n => f (N + n)%nat).

 Lemma is_lim_seq_max (f g : nat -> R) (l : Rbar) :
   is_lim_seq f l ->
   is_lim_seq g l ->
   is_lim_seq (fun n => Rmax (f n) (g n)) l.


End Sequences.

Section Series.

Global Instance Series_proper :
  Proper (pointwise_relation _ eq ==> eq) (Series).

Global Instance ex_series_proper (K : AbsRing) (V : NormedModule K):
  Proper (pointwise_relation _ eq ==> iff) (@ex_series K V).
  Lemma sum_f_R0_nonneg_le_Series {x : nat -> R}(hx1 : ex_series x) (hx2 : forall n, 0 <= x n) :
    forall N, sum_f_R0 x N <= Series x.


  Lemma lim_0_nneg (a : nat -> R) :
    is_series a 0 ->
    (forall n, 0 <= a n) ->
    forall n, a n = 0.

  Lemma ex_series_nneg_bounded (f g : nat -> R) :
    (forall n, 0 <= f n) ->
    (forall n, f n <= g n) ->
    ex_series g ->
    ex_series f.

    Lemma ex_series_bounded (f : nat -> R) :
    ex_series f ->
    exists (M:R),
      forall n, Rabs (sum_n f n) <= M.

  Lemma ex_series_pos_bounded (f : nat -> R) (B:R) :
    (forall n, 0 <= f n) ->
    (forall n, sum_n f n <= B) ->
    ex_series f.

  Lemma Abel_descending_convergence (a b : nat -> R) :
    ex_series b ->
    (forall n, a n >= a (S n)) ->
    (exists M, forall n, a n >= M) ->
    ex_series (fun n => a n * b n).

  Lemma Abel_ascending_convergence (a b : nat -> R) :
    ex_series b ->
    (forall n, a n <= a (S n)) ->
    (exists M, forall n, a n <= M) ->
    ex_series (fun n => a n * b n).

  Lemma sum_n_m_Series_alt (f : nat -> R) (n m : nat) :
     (n <= m)%nat ->
     ex_series f ->
     sum_n_m f n m = Series (fun i => f (n + i)%nat) -
                     Series (fun i => f (S m + i)%nat).

   Lemma sum_n_m_Series1 (f : nat -> R) (n m : nat) :
     (0 < n <= m)%nat ->
     ex_series f ->
     sum_n_m f n m = Series (fun i => f (n + i)%nat) -
                     Series (fun i => f (S m + i)%nat).


   Lemma sum_n_m_Series (f : nat -> R) (n m : nat) :
     (n <= m)%nat ->
     ex_series f ->
     sum_n_m f n m = Series (fun i => f (n + i)%nat) -
                     Series (fun i => f (S m + i)%nat).

   Lemma Rmax_list_sum_series_eps (f : nat -> R) :
     ex_series f ->
     forall (eps : posreal),
     exists (NN : nat),
     forall (n N : nat),
       (N >= NN)%nat ->
       (n >= N)%nat ->
        Rmax_list
          (map
             (fun k : nat =>
                Rabs (sum_n_m f k n))
             (seq N (S (n - N)))) < eps.

   Lemma Rmax_list_sum_series_eps2(f : nat -> R) :
     ex_series f ->
     forall (eps : posreal),
     exists (NN : nat),
     forall (n N : nat),
       (N >= NN)%nat ->
       (n > (S N))%nat ->
        Rmax_list
          (map
             (fun k : nat =>
                Rabs (sum_n_m f (S k) (n-1)%nat))
             (seq N (S ((n-1) - N)))) < eps.
End Series.



Section tails.


  Definition tail_series (a : nat -> R) := fun n => Series(fun k => a((n+k)%nat)).

   Lemma tail_succ_sub {a : nat -> R} (ha : ex_series a) :
      forall n, a n = tail_series a n - tail_series a (S n).

  Lemma tail_series_nonneg_le {a : nat -> R}(ha : ex_series a)(ha' : forall n, 0 <= a n):
    forall n, 0 <= tail_series a (S n) <= tail_series a n.


  Lemma tail_series_pos_lt {a : nat -> R}(ha : ex_series a)(ha' : forall n, 0 < a n):
    forall n, 0 < tail_series a (S n) < tail_series a n.

  Lemma tail_series_nonneg_eventually_pos (a : nat -> R) :
    (forall n, 0 <= a n) ->
    (forall n, exists h, 0 < a (n + h)%nat) ->
    ex_series a ->
    forall n, 0 < tail_series a n.

  Lemma rudin_12_b_aux1_nonneg {a : nat -> R} (ha : ex_series a)(ha' : forall n, 0 <= a n)
        (ha'' : forall n, exists h, 0 < a (n + h)%nat):
    forall n, R_sqrt.sqrt(tail_series a n) + R_sqrt.sqrt(tail_series a (S n)) <= 2*R_sqrt.sqrt(tail_series a n).

  Lemma rudin_12_b_aux2_nonneg {a : nat -> R} (ha : ex_series a)(ha' : forall n, 0 <= a n):
      forall n, a n = (sqrt(tail_series a n) + sqrt(tail_series a (S n)))*(sqrt(tail_series a n) - sqrt(tail_series a (S n))).

  Lemma rudin_12_b_aux3_nonneg {a : nat -> R}(ha : ex_series a) (ha' : forall n, 0 <= a n)
    (ha'' : forall n, exists h, 0 < a (n + h)%nat) :
    forall n, a n*/sqrt(tail_series a n) <= 2*(sqrt(tail_series a n) - sqrt(tail_series a (S n))).

  Lemma rudin_12_b_aux4_nonneg {a : nat -> R}(ha : ex_series a) (ha' : forall n, 0 <= a n)
   (ha'' : forall n, exists h, 0 < a (n + h)%nat):
    forall m, sum_f_R0 (fun n => a n */ sqrt(tail_series a n)) m <= 2*(sqrt(tail_series a 0%nat) - sqrt(tail_series a(S m))).

  Lemma is_lim_seq_inv_pos_p_infty {a : nat -> R}(ha: is_lim_seq a 0) (ha' : forall n, 0 < a n):
    is_lim_seq (fun n => / a n) p_infty.


   Lemma no_worst_converge_nonneg (a: nat -> R) :
     (forall n, 0 <= a n) ->
         (forall n, exists h, 0 < a (n + h)%nat) ->
    ex_series a ->
    exists (b : nat -> R),
      (forall n, 0 < b n) /\
      is_lim_seq b p_infty /\
      ex_series (fun n => a n * b n).


 Lemma no_worst_converge_pos (a: nat -> R) :
   (forall n, 0 < a n) ->
    ex_series a ->
    exists (b : nat -> R),
      (forall n, 0 < b n) /\
      is_lim_seq b p_infty /\
      ex_series (fun n => a n * b n).

 Definition eventually_pos_dec (a : nat -> R) :
   {forall n : nat, exists h : nat, 0 < a (n + h)%nat} +{~(forall n : nat, exists h : nat, 0 < a (n + h)%nat)}.

 Theorem no_worst_converge_iff (a : nat -> R):
   (forall n, 0 <= a n) ->
   ex_series a <->
   exists (b : nat -> R),
     (forall n, 0 < b n) /\
     is_lim_seq b p_infty /\
     ex_series (fun n => a n * b n).

  Lemma no_best_diverge_pos (gamma : nat -> R) :
   0 < gamma 0%nat ->
   (forall n, 0 <= gamma n) ->
   is_lim_seq (sum_n gamma) p_infty ->
   exists (rho : nat -> posreal),
     is_lim_seq rho 0 /\ is_lim_seq (sum_n (fun n => rho n * gamma n)) p_infty.

  Lemma sum_shift_diff (X : nat -> R) (m a : nat) :
     sum_n X (a + S m) - sum_n X m =
     sum_n (fun n0 : nat => X (n0 + S m)%nat) a.

 Lemma is_lim_seq_sum_shift_inf1 (f : nat -> R) (N : nat) :
   is_lim_seq (sum_n f) p_infty <->
   is_lim_seq (sum_n (fun n => f (n + (S N))%nat)) p_infty.

 Lemma is_lim_seq_sum_shift_inf (f : nat -> R) (N : nat) :
   is_lim_seq (sum_n f) p_infty <->
   is_lim_seq (sum_n (fun n => f (n + N)%nat)) p_infty.

  Lemma no_best_diverge (gamma : nat -> R) :
   (forall n, 0 <= gamma n) ->
   is_lim_seq (sum_n gamma) p_infty ->
   exists (rho : nat -> posreal),
     is_lim_seq rho 0 /\ is_lim_seq (sum_n (fun n => rho n * gamma n)) p_infty.

  Theorem no_best_diverge_iff (gamma : nat -> R) :
   (forall n, 0 <= gamma n) ->
   is_lim_seq (sum_n gamma) p_infty <->
   exists (rho : nat -> posreal),
     is_lim_seq rho 0 /\ is_lim_seq (sum_n (fun n => rho n * gamma n)) p_infty.

   Lemma no_worst_converge_div (a : nat -> R) :
    (forall n, 0 <= a n) ->
    ex_series a ->
    exists (b : nat -> R),
      (forall n, 0 < b n) /\
      is_lim_seq b 0 /\
      ex_series (fun n => a n / Rsqr (b n)).


 End tails.