proposition: Lemma FindCrossingPointIncr : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (a b eta alpha : CRcarrier (RealT (ElemFunc IS))) (aPos : 0 < a) (ltab : a < b) (aeta : 0 < a - eta < a) (beta : 0 < b < b + eta) (n i j : nat), ((i <= 2 ^ n)%nat * ((i = (2 ^ n)%nat) + (StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n (S i) < alpha)) * (alpha < StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n i)) -> ((j <= 2 ^ S n)%nat * ((j = (2 ^ S n)%nat) + (StepApproxDiscretize f fInt a b eta aPos ltab aeta beta (S n) (S j) < alpha)) * (alpha < StepApproxDiscretize f fInt a b eta aPos ltab aeta beta (S n) j)) -> BinarySubdiv a b n i <= BinarySubdiv a b (S n) j + (b-a) * CRpow (CR_of_Q _ (1#2)) (S n).
proof: Proof. intros. destruct H,H0,p,p0. destruct s0. - subst j. rewrite BinarySubdivRight. apply (CRle_trans _ (b+0)). rewrite CRplus_0_r. apply BinarySubdivInside. apply CRlt_asym, ltab. exact l. apply CRplus_le_compat_l. apply CRmult_le_0_compat. apply CRlt_asym, CRlt_minus, ltab. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. apply CRlt_asym, ltab. - destruct s. subst i. rewrite BinarySubdivRight. 2: apply CRlt_asym, ltab. destruct (le_lt_dec (2^S n) (S j)). + unfold BinarySubdiv. apply (CRplus_le_reg_l (-a)). rewrite <- CRplus_assoc, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite <- (CRmult_comm (b-a)), <- (CRmult_1_r (-a+b)). rewrite CRmult_assoc, <- CRmult_plus_distr_l, CRplus_comm. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltab. rewrite <- (CRmult_1_l (CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S n))). rewrite <- CRmult_plus_distr_r. apply (CRmult_le_reg_r (CRpow (CR_of_Q _ (Z.of_nat 2 # 1)) (S n))). apply CRpow_gt_zero. apply CR_of_Q_pos. reflexivity. rewrite CRmult_1_l, CRmult_assoc, CRpow_mult. rewrite (CRpow_proper (CR_of_Q (RealT (ElemFunc IS)) (/ 2) * CR_of_Q (RealT (ElemFunc IS)) (Z.of_nat 2 # 1)) 1). rewrite CRpow_one, <- pow_nat, CRmult_1_r. rewrite <- CR_of_Q_plus. apply CR_of_Q_le. unfold Qplus, Qle, Qnum, Qden. do 4 rewrite Z.mul_1_r. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add. apply Nat2Z.inj_le. rewrite Nat.add_comm. exact l1. reflexivity. rewrite <- CR_of_Q_mult. apply CR_of_Q_morph. reflexivity. + exfalso. pose proof (CRlt_trans _ _ _ c1 c). apply (StepApproxDiscretizeRefineIncr f fInt a b eta aPos ltab aeta beta n (S j) (2^n)). 2: exact H. unfold lt in l1. replace (2*2^n)%nat with (2 ^ S n)%nat. exact l1. reflexivity. + pose proof (CRlt_trans _ _ _ c1 c) as H. destruct (le_lt_dec (S (S j)) (2*i)). * exfalso. exact (StepApproxDiscretizeRefineIncr f fInt a b eta aPos ltab aeta beta n (S j) i l1 H). * apply le_S_n in l1. unfold BinarySubdiv. rewrite CRplus_assoc. apply CRplus_le_compat_l. do 2 rewrite <- (CRmult_comm (b-a)), CRmult_assoc. rewrite <- CRmult_plus_distr_l. rewrite <- (CRmult_1_l (CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) (S n))). rewrite <- CRmult_plus_distr_r. simpl (CRpow (CR_of_Q (RealT (ElemFunc IS)) (/ 2)) (S n)). apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltab. rewrite <- CRmult_assoc. apply CRmult_le_compat_r. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. rewrite <- CR_of_Q_plus, <- CR_of_Q_mult. apply CR_of_Q_le. apply Qle_shift_div_l. reflexivity. unfold Qplus, Qmult, Qle, Qnum, Qden. do 4 rewrite Z.mul_1_r. replace 2%Z with (Z.of_nat 2). rewrite <- Nat2Z.inj_mul. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add. apply Nat2Z.inj_le. rewrite Nat.add_comm, Nat.mul_comm. exact l1. reflexivity. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia