proposition: Lemma StepApproxDiscretizeRefineDecr : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (a b eta : CRcarrier (RealT (ElemFunc IS))) (aPos : 0 < a) (ltab : a < b) (aeta : 0 < a - eta < a) (beta : 0 < b < b + eta) (n i j : nat), le (2*j) i -> StepApproxDiscretize f fInt a b eta aPos ltab aeta beta (S n) i <= StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n j.
proof: Proof. intros. unfold StepApproxDiscretize. destruct j,i. - apply CRle_refl. - clear H. destruct (le_lt_dec (S (2 ^ S n)) (S i)). apply StepApproxIntegralIncr. apply (CRle_trans _ a). apply CRlt_asym, (snd aeta). apply CRlt_asym, ltab. apply (CRle_trans _ b). apply CRlt_asym, ltab. apply CRlt_asym, (snd beta). apply StepApproxIntegralIncr. apply (CRle_trans _ a). apply CRlt_asym, (snd aeta). apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n in l. apply (Nat.le_trans _ (S i)). apply le_S, Nat.le_refl. exact l. apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n, l. - exfalso. inversion H. - destruct (le_lt_dec (S (2 ^ n)) (S j)), (le_lt_dec (S (2 ^ S n)) (S i)). + apply CRle_refl. + exfalso. apply le_S_n in l0. apply (Nat.le_trans _ _ _ H) in l0. clear H. apply (Nat.mul_le_mono_pos_l _ _ 2) in l0. apply (Nat.le_trans _ _ _ l) in l0. apply (proj1 (Nat.le_ngt _ _) l0 (Nat.le_refl _)). apply le_n_S, Nat.le_0_l. + apply StepApproxIntegralIncr. apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n in l. apply (Nat.le_trans _ (S j)). apply le_S, Nat.le_refl. exact l. apply (CRle_trans _ b). apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n, l. apply CRlt_asym, (snd beta). + apply StepApproxIntegralIncr. apply CRplus_le_compat_l. do 2 rewrite <- (CRmult_comm (b-a)), CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltab. simpl (CRpow (CR_of_Q (RealT (ElemFunc IS)) (/ 2)) (S n)). rewrite <- CRmult_assoc. apply CRmult_le_compat_r. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. rewrite <- CR_of_Q_mult. apply CR_of_Q_le. apply Qle_shift_div_l. reflexivity. unfold Qmult, Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. replace 2%Z with (Z.of_nat 2). 2: reflexivity. rewrite <- Nat2Z.inj_mul. apply Nat2Z.inj_le. apply le_S_n. apply (Nat.le_trans _ (2*S j)). 2: exact H. rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r, Nat.add_succ_r. apply le_S, Nat.le_refl. apply CRplus_le_compat_l. do 2 rewrite <- (CRmult_comm (b-a)), CRmult_assoc. apply CRmult_le_compat_l. apply CRlt_asym, CRlt_minus, ltab. simpl (CRpow (CR_of_Q (RealT (ElemFunc IS)) (/ 2)) (S n)). rewrite <- CRmult_assoc. apply CRmult_le_compat_r. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. rewrite <- CR_of_Q_mult. apply CR_of_Q_le. apply Qle_shift_div_l. reflexivity. unfold Qmult, Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. replace 2%Z with (Z.of_nat 2). 2: reflexivity. rewrite <- Nat2Z.inj_mul. apply Nat2Z.inj_le. apply (Nat.le_trans _ (2*S j)). 2: exact H. rewrite Nat.mul_comm. apply Nat.le_refl. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia