proposition: Lemma SliceBar : forall {R : ConstructiveReals} {X : Set} (x : CRcarrier R) (nk : nat -> nat), (forall n:nat, lt (nk n) (nk (S n))) -> nk O = O -> 0 <= x -> series_cv (fun n : nat => CRmin (INR (nk (S n) - nk n)) (x - CRmin x (INR (nk n)))) x.
proof: Proof. intros. assert (forall k:nat, CRsum (fun n : nat => CRmin (INR (nk (S n) - nk n)) (x - CRmin x (INR (nk n)))) k == CRmin x (INR (nk (S k)))). { induction k. - intros. simpl. rewrite (CRmin_right x (INR (nk 0%nat))). rewrite H0. rewrite CRmin_sym. rewrite Nat.sub_0_r. setoid_replace (x - INR 0) with x. reflexivity. unfold INR. simpl. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. rewrite H0. unfold INR. apply H1. - intros. simpl. rewrite IHk. clear IHk. rewrite CRmin_plus. setoid_replace (CRmin x (INR (nk (S k))) + (x - CRmin x (INR (nk (S k))))) with x. rewrite CRmin_sym, CRplus_comm, CRmin_plus. setoid_replace (@INR R (nk (S (S k)) - nk (S k)) + INR (nk (S k))) with (@INR R (nk (S (S k)))). rewrite CRmin_assoc. rewrite (CRmin_left x). reflexivity. apply (CRle_trans _ (0+x)). rewrite CRplus_0_l. apply CRle_refl. apply CRplus_le_compat. apply CR_of_Q_le. unfold Qle; simpl. rewrite Z.mul_1_r. apply Nat2Z.is_nonneg. apply CRle_refl. unfold INR. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. rewrite <- Nat2Z.inj_add. rewrite Nat.sub_add. reflexivity. specialize (H (S k)). apply (Nat.le_trans _ (S (nk (S k)))). apply le_S, Nat.le_refl. apply H. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. } destruct (CRup_nat x) as [n nmaj]. exists n. intros. rewrite H2. rewrite CRmin_left. unfold CRminus. rewrite CRplus_opp_r, CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. apply (CRle_trans _ (INR n)). apply CRlt_asym, nmaj. apply CR_of_Q_le. unfold Qle; simpl. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le. apply (Nat.le_trans _ _ _ H3). apply (Nat.le_trans _ (S i)). apply le_S, Nat.le_refl. apply growing_infinite. exact H. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity