proposition: Lemma StepApproxDiscretizeDecr : 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 i j -> StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n j <= StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n i.
proof: Proof. induction j. - intros. inversion H. apply CRle_refl. - intros. apply Nat.le_succ_r in H. destruct H. 2: subst i; apply CRle_refl. apply (CRle_trans _ (StepApproxDiscretize f fInt a b eta aPos ltab aeta beta n j)). 2: exact (IHj H). destruct j. + unfold StepApproxDiscretize. destruct (le_lt_dec (S (2 ^ n)) 1). exfalso. apply le_S_n in l. inversion l. pose proof (Nat.pow_gt_lin_r 2 n (Nat.le_refl _)). rewrite H1 in H0. inversion H0. apply StepApproxIntegralIncr. apply (CRle_trans _ a). apply CRlt_asym, (snd aeta). apply BinarySubdivInside. apply CRlt_asym, ltab. apply Nat.le_0_l. apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n, l. + unfold StepApproxDiscretize. destruct (le_lt_dec (S (2 ^ n)) (S (S j))), (le_lt_dec (S (2 ^ n)) (S j)). apply CRle_refl. apply StepApproxIntegralIncr. apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n in l0. apply (Nat.le_trans _ (S j)). apply le_S, Nat.le_refl. exact l0. apply (CRle_trans _ b). apply BinarySubdivInside. apply CRlt_asym, ltab. apply le_S_n, l0. apply CRlt_asym, (snd beta). exfalso. pose proof (Nat.lt_le_trans _ _ _ l l0). apply (proj1 (Nat.lt_nge _ _) H0). apply le_S, Nat.le_refl. apply StepApproxIntegralIncr. apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab). apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia