proposition: Lemma FindJumpPointsCountable : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), { s : nat -> CRcarrier (RealT (ElemFunc IS)) & forall x, 0 < x -> (forall n:nat, CRapart _ x (s n)) -> (forall eps, 0 < eps -> StepApproxBound f fInt x x eps (CRle_refl x)) }.
proof: Proof. intros. pose (fun (n:nat) => CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (S n))) as an. pose (fun (n:nat) => CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (2+n) # 1)) as bn. assert (forall n:nat, an n < bn n) as ltabn. { intro n. unfold an, bn. apply (CRle_lt_trans _ (CR_of_Q _ 1)). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos.le_1_l. apply CR_of_Q_lt. unfold Qlt, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply (Nat2Z.inj_lt 1 (2+n)). apply le_n_S, le_n_S, Nat.le_0_l. } assert (forall n:nat, 0 < an n) as anPos. { intro n. apply CR_of_Q_pos. reflexivity. } assert (forall n:nat, 0 < an n - an n * CR_of_Q _ (1#2) < an n) as orderBefore. { split. apply (CRlt_le_trans _ (an n * CR_of_Q _ (1#2))). apply CRmult_lt_0_compat. exact (anPos n). apply CR_of_Q_pos. reflexivity. apply (CRplus_le_reg_r (an n * CR_of_Q (RealT (ElemFunc IS)) (1 # 2))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. setoid_replace ((1 # 2) + (1 # 2))%Q with 1%Q. rewrite CRmult_1_r. apply CRle_refl. reflexivity. apply (CRle_lt_trans _ (an n * CR_of_Q _ (1#2))). apply (CRplus_le_reg_r (an n * CR_of_Q (RealT (ElemFunc IS)) (1 # 2))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus. setoid_replace ((1 # 2) + (1 # 2))%Q with 1%Q. rewrite CRmult_1_r. apply CRle_refl. reflexivity. rewrite <- (CRmult_1_r (an n)), CRmult_assoc. apply CRmult_lt_compat_l. exact (anPos n). rewrite CRmult_1_l. apply CR_of_Q_lt. reflexivity. } assert (forall n:nat, 0 < bn n < bn n + an n*CR_of_Q _ (1#2)) as orderAfter. { split. exact (CRlt_trans _ (an n) _ (anPos n) (ltabn n)). apply (CRle_lt_trans _ (bn n + 0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_lt_compat_l. apply CRmult_lt_0_compat. exact (anPos n). apply CR_of_Q_pos. reflexivity. } pose (fun n:nat => Integral (StepApproxIntegrable f (an n - an n*CR_of_Q _ (1#2)) (an n) (orderBefore n) fInt)) as intBefore. pose (fun n:nat => Integral (StepApproxIntegrable f (bn n) (bn n + an n*CR_of_Q _ (1#2)) (orderAfter n) fInt)) as intAfter. pose (fun (n:nat) => let (k,_) := CRup_nat ((1+ intBefore n - intAfter n) * CRinv _ (CR_of_Q _ (1 # Pos.of_nat n)) (inr (CR_of_Q_pos (1 # Pos.of_nat n) (eq_refl _)))) in k) as qn. assert (forall n:nat, 1 + intBefore n - intAfter n <= CR_of_Q _ (Z.of_nat (qn n) # 1) * CR_of_Q _ (1 # Pos.of_nat n)). { intro n. unfold qn. destruct ( CRup_nat ((1 + intBefore n - intAfter n) * CRinv (RealT (ElemFunc IS)) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat n)) (inr (CR_of_Q_pos (1 # Pos.of_nat n) eq_refl)))). apply CRlt_asym in c. apply (CRmult_le_compat_r (CR_of_Q _ (1 # Pos.of_nat n))) in c. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in c. exact c. apply CR_of_Q_le. discriminate. } assert (forall n:nat, intAfter n <= intBefore n) as orderInt. { intro n. apply (StepApproxIntegralIncr f fInt (an n - an n * CR_of_Q _ (1 # 2)) (an n) (bn n) (bn n + an n * CR_of_Q _ (1 # 2)) (orderBefore n) (orderAfter n)). apply (CRle_trans _ (an n)). apply CRlt_asym, orderBefore. apply CRlt_asym, ltabn. apply (CRle_trans _ (bn n + 0)). rewrite CRplus_0_r. apply CRlt_asym, ltabn. apply CRplus_le_compat_l. apply CRlt_asym, CRmult_lt_0_compat. exact (anPos n). apply CR_of_Q_pos. reflexivity. } assert (forall n:nat, qn n <> O) as qnz. { intro n. unfold qn. destruct ( CRup_nat ((1 + intBefore n - intAfter n) * CRinv (RealT (ElemFunc IS)) (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat n)) (inr (CR_of_Q_pos (1 # Pos.of_nat n) eq_refl)))). apply CRlt_asym in c. intro abs. rewrite abs in c. apply (CRmult_le_compat_r (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat n))) in c. rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_0_l in c. apply (CRplus_le_compat _ _ _ _ (orderInt n)) in c. rewrite CRplus_comm in c. unfold CRminus in c. rewrite CRplus_assoc, CRplus_assoc, CRplus_opp_l, CRplus_comm in c. rewrite CRplus_assoc in c. apply CRplus_le_reg_l in c. rewrite CRplus_0_l in c. apply c. apply CRzero_lt_one. apply CR_of_Q_le. discriminate. } assert (forall n:nat, bn n < bn n + an n*CR_of_Q _ (1#2)). { intro n. apply (CRle_lt_trans _ (bn n + 0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_lt_compat_l. apply CRmult_lt_0_compat. exact (anPos n). apply CR_of_Q_pos. reflexivity. } assert (forall n : nat, StepApproxBound f fInt (an n) (bn n) (1 + intBefore n - intAfter n) (CRlt_asym (an n) (bn n) (ltabn n)) ) as intBound. { intro n. exists (Build_IntervalExtension _ _ _ _ (orderBefore n) (H0 n)). simpl. apply (CRle_lt_trans _ (intBefore n - intAfter n)). apply CRplus_le_compat. unfold intBefore. apply StepApproxIntegralIncr. apply CRle_refl. apply CRle_refl. unfold intAfter. apply CRopp_ge_le_contravar, StepApproxIntegralIncr. apply CRle_refl. apply CRle_refl. rewrite <- (CRplus_0_l (intBefore n - intAfter n)). unfold CRminus. rewrite CRplus_assoc. apply CRplus_lt_compat_r, CRzero_lt_one. } pose proof (fun (n:nat) => FindJumpPointsFinite f fInt (an n) (bn n) (1 + intBefore n - intAfter n) (CR_of_Q _ (1 # Pos.of_nat n)) (anPos n) (ltabn n) (CR_of_Q_pos (1 # Pos.of_nat n) (eq_refl _)) (qn n) (H n) (qnz n) (intBound n)). exists (diagSeq (fun n k => let (s,_) := H1 n in s k)). intros. assert (forall n k : nat, CRapart _ x (let (s, _) := H1 n in s k)). { intros. specialize (H3 (diagPlane n k)). unfold diagSeq in H3. rewrite diagPlaneInject in H3. exact H3. } clear H3. destruct (CRup_nat (CRinv _ eps (inr H4))) as [n nmaj]. assert (CR_cv _ an 0) as stepCv. { unfold an. intro p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (Nat.le_trans _ _ _ H3). apply le_S, Nat.le_refl. discriminate. apply CR_of_Q_le. discriminate. } destruct (CR_cv_open_above an x 0 stepCv H2) as [i imaj]. destruct (CRup_nat x) as [j jmaj]. specialize (imaj (max n (max i j)) (Nat.le_trans _ _ _ (Nat.le_max_l i j) (Nat.le_max_r _ _))). specialize (H5 (max n (max i j))). destruct (H1 (max n (max i j))) as [s a0], a0, H6, H7. destruct (FindInterval s x O (qn (max n (max i j))) H7 H5) as [k kmaj]. split. rewrite H3. exact imaj. rewrite H6. apply (CRlt_le_trans _ _ _ jmaj). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le. apply (Nat.le_trans _ (2+j)). apply le_S, le_S, Nat.le_refl. apply le_n_S, le_n_S. exact (Nat.le_trans _ _ _ (Nat.le_max_r i _) (Nat.le_max_r _ _)). apply Nat.le_refl. destruct (IntervalOpenEta (s k) (s (S k)) x kmaj) as [eta etamaj]. destruct etamaj. assert (0 < x - eta < x). { split. 2: exact (snd p). apply (CRle_lt_trans _ (s k)). 2: exact (fst p). apply (CRle_trans _ (s O)). rewrite H3. apply CRlt_asym, anPos. apply growing_transit. exact H7. apply Nat.le_0_l. } exists (Build_IntervalExtension _ _ _ _ H9 (fst p0)). simpl. apply (CRle_lt_trans _ (CR_of_Q _ (1 # Pos.of_nat n))). specialize (H8 k (x - eta) x x (x + eta) H9). apply (CRle_trans _ (CR_of_Q (RealT (ElemFunc IS)) (1 # Pos.of_nat (max n (max i j))))). apply H8. 2: exact (CRle_refl x). exact (fst p). exact (snd p0). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. rewrite Nat2Pos.inj_max. apply Pos.le_max_l. apply (CRmult_lt_compat_l eps) in nmaj. rewrite CRinv_r in nmaj. destruct n. exfalso. rewrite CRmult_0_r in nmaj. contradict nmaj. apply CRlt_asym, CRzero_lt_one. apply (CRmult_lt_reg_r (CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat (S n) # 1))). apply CR_of_Q_pos. reflexivity. rewrite <- CR_of_Q_mult. setoid_replace ((1 # Pos.of_nat (S n)) * (Z.of_nat (S n) # 1))%Q with 1%Q. exact nmaj. unfold Qmult, Qeq, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l, Z.mul_1_r, Pos.mul_1_r. simpl (Z.of_nat (S n)). apply f_equal. rewrite Pos.of_nat_succ. reflexivity. exact H4. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia