proposition: Lemma CharacFuncStationary : forall {R : ConstructiveReals} (X : Set) (An : nat -> X -> Prop) (x : X) (xn : forall n:nat, Domain (CharacFunc (An n)) x), CR_cauchy R (fun n => partialApply (CharacFunc (An n)) x (xn n)) -> { p : nat | forall n:nat, le p n -> partialApply (CharacFunc (An p)) x (xn p) = partialApply (CharacFunc (An n)) x (xn n) }.
proof: Proof. intros. destruct (H 2%positive) as [p pcv]. auto. exists p. intros. simpl. simpl in pcv. specialize (pcv p n (Nat.le_refl _) H0). assert (CR_of_Q R (1 # 2) < 1). { apply CR_of_Q_lt. reflexivity. } destruct (xn p), (xn n). reflexivity. 3: reflexivity. - exfalso. unfold CRminus in pcv. rewrite CRopp_0, CRplus_0_r, CRabs_right in pcv. contradiction. apply CRlt_asym, CRzero_lt_one. - exfalso. unfold CRminus in pcv. rewrite CRplus_0_l, CRabs_opp, CRabs_right in pcv. contradiction. apply CRlt_asym, CRzero_lt_one. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity