proposition: Lemma UC_integral_chasles_rat : forall {R : ConstructiveReals} (a b c : Q) (f : CRcarrier R -> CRcarrier R) (cont_mod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f cont_mod) (leab : (CR_of_Q R a) <= (CR_of_Q R b)) (lebc : (CR_of_Q R b) <= (CR_of_Q R c)) (leac : (CR_of_Q R a) <= (CR_of_Q R c)), UC_integral f (CR_of_Q R a) (CR_of_Q R c) cont_mod fCont leac == UC_integral f (CR_of_Q R a) (CR_of_Q R b) cont_mod fCont leab + UC_integral f (CR_of_Q R b) (CR_of_Q R c) cont_mod fCont lebc.
proof: Proof. intros. unfold UC_integral. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n : nat => (CR_of_Q R a + (CR_of_Q R c - CR_of_Q R a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) (fun n : nat => (CR_of_Q R a + (CR_of_Q R c - CR_of_Q R a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last)))) last) (UC_integral_cauchy f (CR_of_Q R a) (CR_of_Q R c) cont_mod fCont leac)) as [l lcv]. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n : nat => CR_of_Q R a + (CR_of_Q R b - CR_of_Q R a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => CR_of_Q R a + (CR_of_Q R b - CR_of_Q R a) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy f (CR_of_Q R a) (CR_of_Q R b) cont_mod fCont leab)) as [lab H]. destruct (CR_complete R (fun last : nat => IntegralFiniteSum f (fun n : nat => CR_of_Q R b + (CR_of_Q R c - CR_of_Q R b) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) (fun n : nat => CR_of_Q R b + (CR_of_Q R c - CR_of_Q R b) * CR_of_Q R (Z.of_nat n # Pos.of_nat (S last))) last) (UC_integral_cauchy f (CR_of_Q R b) (CR_of_Q R c) cont_mod fCont lebc)) as [lbc H0]. apply (CR_cv_unique _ _ _ lcv). intros n. assert (0 < 1+CR_of_Q R c - CR_of_Q R a) as invStepPos. { apply (CRlt_le_trans _ (1 + 0)). rewrite CRplus_0_r. apply CRzero_lt_one. unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite <- (CRplus_opp_r (CR_of_Q R a)). apply CRplus_le_compat. exact leac. apply CRle_refl. } assert (0 < CR_of_Q R (1 # 4*n) * CRinv R (1+CR_of_Q R c - CR_of_Q R a) (inr invStepPos)) as stepPos. { apply CRmult_lt_0_compat. apply CR_of_Q_lt; reflexivity. apply CRinv_0_lt_compat. exact invStepPos. } destruct (CRup_nat ((CR_of_Q R c-CR_of_Q R a) * CRinv R (cont_mod _ stepPos) (inr ((fst fCont) _ stepPos)))) as [p pmaj]. destruct (CRup_nat ((CR_of_Q R b-CR_of_Q R a) * CRinv R (cont_mod _ stepPos) (inr ((fst fCont) _ stepPos)))) as [q qmaj]. destruct (CRup_nat ((CR_of_Q R c-CR_of_Q R b) * CRinv R (cont_mod _ stepPos) (inr ((fst fCont) _ stepPos)))) as [r rmaj]. specialize (H (4*n)%positive) as [i imaj]. specialize (H0 (4*n)%positive) as [j jmaj]. exists p. intros i0 H. pose (IntervalPartitionConcat (IntervalEquiPartition (CR_of_Q R a) (CR_of_Q R b) (max i q) leab) (IntervalEquiPartition (CR_of_Q R b) (CR_of_Q R c) (max j r) lebc)) as conc. setoid_replace (IntegralFiniteSum f (fun n0 : nat => CR_of_Q R a + (CR_of_Q R c - CR_of_Q R a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S i0))) (fun n0 : nat => CR_of_Q R a + (CR_of_Q R c - CR_of_Q R a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S i0))) i0 - (lab + lbc)) with (IntegralFiniteSum f (fun n0 : nat => CR_of_Q R a + (CR_of_Q R c - CR_of_Q R a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S i0))) (fun n0 : nat => CR_of_Q R a + (CR_of_Q R c - CR_of_Q R a) * CR_of_Q R (Z.of_nat n0 # Pos.of_nat (S i0))) i0 - IntegralFiniteSum f (ipt_seq conc) (ipt_seq conc) (ipt_last conc) + (IntegralFiniteSum f (ipt_seq conc) (ipt_seq conc) (ipt_last conc) - (lab + lbc))). apply (CRle_trans _ _ _ (CRabs_triang _ _)). setoid_replace (CR_of_Q R (1 # n)) with (CR_of_Q R (1 # 2*n) + CR_of_Q R (1 # 2*n)). apply CRplus_le_compat. - apply (CRle_trans _ ((CR_of_Q R (1# 4*n) * CRinv R (1+CR_of_Q R c - CR_of_Q R a) (inr invStepPos) + CR_of_Q R (1# 4*n) * CRinv R (1+CR_of_Q R c - CR_of_Q R a) (inr invStepPos)) * (CR_of_Q R c-CR_of_Q R a))). destruct (CommonRationalRefinement (CR_of_Q R a) (CR_of_Q R c) (IntervalEquiPartition (CR_of_Q R a) (CR_of_Q R c) i0 leac) conc) as [ccr_subseqP0 [ccr_subseqQ0 [ccr_refinement0 [ccr_refineP0 ccr_refineQ0]]]]. apply EquiPartitionRational. apply PartitionRationalConcat. apply EquiPartitionRational. apply EquiPartitionRational. apply (UC_compare_integrals f (CR_of_Q R a) (CR_of_Q R c) _ _ cont_mod (IntervalEquiPartition (CR_of_Q R a) (CR_of_Q R c) i0 leac) conc ccr_refinement0 stepPos stepPos ccr_subseqP0 ccr_subseqQ0 fCont ccr_refineP0 ccr_refineQ0). + rewrite EquiPartitionMesh. apply (CRmult_lt_compat_r (cont_mod _ stepPos)) in pmaj. 2: apply (fst fCont). rewrite CRmult_assoc, CRinv_l, CRmult_1_r in pmaj. apply (CRmult_lt_reg_r (CR_of_Q R (Z.of_nat (S i0) # 1))). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # Pos.of_nat (S i0)) * (Z.of_nat (S i0) # 1))%Q with 1%Q. rewrite CRmult_1_r. apply (CRlt_le_trans _ _ _ pmaj). rewrite CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, (fst fCont). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, H. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_l. rewrite Z.mul_1_r, Pos.mul_1_r. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. reflexivity. discriminate. + assert (PartitionMesh (ipt_seq conc) (S (ipt_last conc)) == CRmax ((CR_of_Q R b- CR_of_Q R a) * CR_of_Q R (1# Pos.of_nat (S (max i q)))) ((CR_of_Q R c- CR_of_Q R b) * CR_of_Q R (1# Pos.of_nat (S (max j r))))). { unfold conc. rewrite PartitionMeshConcat. apply CRmax_morph; apply EquiPartitionMesh. } rewrite H0. apply CRmax_lub_lt. apply (CRmult_lt_compat_r (cont_mod _ stepPos)) in qmaj. 2: apply (fst fCont). rewrite CRmult_assoc, CRinv_l, CRmult_1_r in qmaj. apply (CRmult_lt_reg_r (CR_of_Q R (Z.of_nat (S (Init.Nat.max i q)) # 1))). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # Pos.of_nat (S (Init.Nat.max i q))) * (Z.of_nat (S (Init.Nat.max i q)) # 1))%Q with 1%Q. rewrite CRmult_1_r. apply (CRlt_le_trans _ _ _ qmaj). rewrite CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, (fst fCont). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_max_r. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_l. rewrite Z.mul_1_r, Pos.mul_1_r. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. reflexivity. discriminate. apply (CRmult_lt_compat_r (cont_mod _ stepPos)) in rmaj. 2: apply (fst fCont). rewrite CRmult_assoc, CRinv_l, CRmult_1_r in rmaj. apply (CRmult_lt_reg_r (CR_of_Q R (Z.of_nat (S (Init.Nat.max j r)) # 1))). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # Pos.of_nat (S (Init.Nat.max j r))) * (Z.of_nat (S (Init.Nat.max j r)) # 1))%Q with 1%Q. rewrite CRmult_1_r. apply (CRlt_le_trans _ _ _ rmaj). rewrite CRmult_comm. apply CRmult_le_compat_l. apply CRlt_asym, (fst fCont). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_max_r. unfold Qmult, Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_l. rewrite Z.mul_1_r, Pos.mul_1_r. rewrite <- positive_nat_Z. rewrite Nat2Pos.id. reflexivity. discriminate. + rewrite <- (CRmult_1_r (CR_of_Q R (1 # 4 * n) * CRinv R (1 + CR_of_Q R c - CR_of_Q R a) (inr invStepPos))). rewrite <- CRmult_plus_distr_l. rewrite (CRmult_comm (CR_of_Q R (1#4*n))). apply (CRmult_le_reg_l (1 + CR_of_Q R c - CR_of_Q R a)). exact invStepPos. do 3 rewrite <- CRmult_assoc. rewrite CRinv_r, CRmult_1_l. setoid_replace (CR_of_Q R (1 # 4 * n) * (1 + 1)) with (CR_of_Q R (1 # 2 * n)). rewrite CRmult_comm. apply CRmult_le_compat_r. apply CR_of_Q_le. discriminate. rewrite <- (CRplus_0_l (CR_of_Q R c - CR_of_Q R a)). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_r. exact (CRlt_asym 0 1 (CRzero_lt_one R)). rewrite <- (CR_of_Q_plus R 1 1), <- CR_of_Q_mult. apply CR_of_Q_morph. unfold Qeq, Qnum, Qden. simpl. rewrite Pos.mul_1_r. reflexivity. - unfold conc. rewrite <- IntervalPartitionConcatSum. unfold IntervalEquiPartition, ipt_seq, ipt_last. setoid_replace (CR_of_Q R (1 # 2 * n)) with (CR_of_Q R (1 # 4 * n) + CR_of_Q R (1 # 4 * n)). assert (forall a b c d : CRcarrier R, CRabs _ (a + b - (c + d)) <= CRabs _ (a - c) + CRabs _ (b - d)). intros. setoid_replace (a0 + b0 - (c0 + d)) with ((a0 - c0) + (b0 - d)). apply CRabs_triang. unfold CRminus. do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite (CRplus_comm (-c0)). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr, CRplus_comm. reflexivity. apply (CRle_trans _ _ _ (H0 _ _ _ _)). apply CRplus_le_compat. apply imaj, Nat.le_max_l. apply jmaj, Nat.le_max_l. rewrite <- CR_of_Q_plus, Qinv_plus_distr. apply CR_of_Q_morph. reflexivity. - rewrite <- CR_of_Q_plus, Qinv_plus_distr. apply CR_of_Q_morph. reflexivity. - unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont