Library Stdlib.Reals.Rprod

From Stdlib Require Import Compare.
From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import Rseries.
From Stdlib Require Import PartSum.
From Stdlib Require Import Binomial.
From Stdlib Require Import Lia.
From Stdlib Require Import Arith.Factorial.
From Stdlib Require Import Peano_dec.
Local Open Scope R_scope.

Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
  match N with
    | O => f O
    | S p => prod_f_R0 f p * f (S p)
  end.

Notation prod_f_SO := (fun An N => prod_f_R0 (fun n => An (S n)) N).

Lemma prod_SO_split :
  forall (An:nat -> R) (n k:nat),
    (k < n)%nat ->
    prod_f_R0 An n =
    prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1).

Lemma prod_SO_pos :
  forall (An:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_R0 An N.

Lemma prod_SO_Rle :
  forall (An Bn:nat -> R) (N:nat),
    (forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
    prod_f_R0 An N <= prod_f_R0 Bn N.

Lemma fact_prodSO :
  forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat =>
     (match (eq_nat_dec k 0) with
          | left _ => 1%R
          | right _ => INR k
                        end)) n.

Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat.

Lemma RfactN_fact2N_factk :
  forall N k:nat,
    (k <= 2 * N)%nat ->
    Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k).

Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n).

Lemma C_maj : forall N k:nat, (k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N.