proposition: Lemma CSUCUnitTrapezeInt : forall {R : ConstructiveReals} (a b eta : CRcarrier R) (etaPos : 0 < eta) (leab : a <= b), UC_integral (CSUCUnitTrapeze a b eta etaPos) (a-eta) (b+eta) _ (CSUCUnitTrapeze_cont a b eta etaPos leab) (TrapezeLe a b eta etaPos leab) == eta + b - a.
proof: Proof. intros. assert (a-eta <= a). { apply (CRle_trans _ (a-0)). apply CRplus_le_compat_l, CRopp_ge_le_contravar, CRlt_asym, etaPos. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. } assert (b <= b+eta) as H1. { apply (CRplus_le_reg_l (-b)). rewrite CRplus_opp_l, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRlt_asym, etaPos. } assert (a <= b+eta). { apply (CRle_trans _ b _ leab). exact H1. } rewrite (UC_integral_chasles (a-eta) a (b+eta) (CSUCUnitTrapeze a b eta etaPos) _ _ H H0). rewrite (UC_integral_chasles a b (b+eta) (CSUCUnitTrapeze a b eta etaPos) _ _ leab H1). assert (forall t:CRcarrier R, UniformCont (fun x => x + t) (fun eps epsPos => eps)) as H2. { intro t. apply (UC_translate_horizontal (fun x=>x) t). apply UC_x. } rewrite (UC_integral_extens _ (fun x:CRcarrier R => CRinv R eta (inr etaPos) * (x + (eta - a))) (a - eta) a _ _ _ (UC_scale _ _ _ (H2 _)) H H). rewrite (UC_integral_extens _ (fun x:CRcarrier R => 1) a b _ (fun eps epsPos => 1) _ (UC_constant _) leab leab). rewrite (UC_integral_extens _ (fun x:CRcarrier R => (-CRinv R eta (inr etaPos)) * (x + (- b - eta))) b (b+eta) _ _ _ (UC_scale _ _ (-CRinv R eta (inr etaPos)) (H2 _)) H1 H1). - rewrite (UC_integral_scale _ (a-eta) a (CRinv R eta (inr etaPos)) (fun (eps : CRcarrier R) (_ : 0 < eps) => eps)). rewrite (UC_integral_plus _ _ (a-eta) a _ _ _ UC_x (UC_constant (eta-a)) _ _ H). rewrite (UC_integral_scale _ b (b+eta) _ (fun eps epsPos => eps)). rewrite (UC_integral_plus _ _ b (b+eta) _ _ _ UC_x (UC_constant (-b -eta)) _ _ H1). rewrite (UC_integral_constant _ a b 1). 2: intros; reflexivity. rewrite CRmult_1_r. rewrite x_RiemannInt. rewrite (UC_integral_constant _ (a-eta) a (eta-a)). rewrite x_RiemannInt. rewrite (UC_integral_constant _ b (b+eta) (-b-eta)). unfold CRminus. rewrite (CRplus_assoc eta). rewrite CRplus_comm, CRplus_assoc, (CRplus_comm eta (b+-a)). apply CRplus_morph. reflexivity. rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r. rewrite <- CRmult_plus_distr_l. apply (CRmult_eq_reg_l eta). right. exact etaPos. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l. setoid_replace (b + eta + - b) with eta. setoid_replace (a + - (a + - eta)) with eta. rewrite CRopp_plus_distr. rewrite (CRopp_mult_distr_r eta). rewrite CRopp_plus_distr, CRopp_involutive, CRopp_involutive. rewrite CRopp_mult_distr_l, CRopp_plus_distr, CRopp_involutive. setoid_replace (a * a + - ((a + - eta) * (a + - eta))) with (CR_of_Q R 2*a*eta - eta*eta). setoid_replace (- ((b + eta) * (b + eta)) + b * b) with (-CR_of_Q R 2*b*eta - eta*eta). setoid_replace ((- CR_of_Q R 2 * b * eta - eta * eta) * CR_of_Q R (1 # 2)) with (- eta*eta *CR_of_Q R (1#2) + -(eta*b)). setoid_replace ((CR_of_Q R 2 * a * eta - eta * eta) * CR_of_Q R (1 # 2)) with ( - eta*eta *CR_of_Q R (1#2) + eta*a). do 2 rewrite CRplus_assoc. rewrite CRmult_plus_distr_l. do 2 rewrite <- (CRplus_assoc (-(eta*b))). rewrite CRplus_opp_l, CRplus_0_l. rewrite (CRplus_comm (eta) (-a)), CRmult_plus_distr_l. rewrite CRplus_assoc, <- (CRplus_assoc (eta*a)). rewrite <- (CRopp_mult_distr_r eta a), CRplus_opp_r, CRplus_0_l. rewrite (CRplus_comm (eta*eta)), <- CRplus_assoc, <- CRplus_assoc. rewrite <- CRmult_plus_distr_l, <- CR_of_Q_plus, Qinv_plus_distr. setoid_replace (1+1#2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r, <- CRopp_mult_distr_l. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. unfold CRminus. rewrite CRmult_comm, CRmult_plus_distr_l. rewrite <- CRmult_assoc, <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q. rewrite CRmult_1_l. rewrite CRplus_comm, CRmult_comm, CRopp_mult_distr_l, (CRmult_comm a eta). reflexivity. reflexivity. unfold CRminus. rewrite CRmult_comm, CRmult_plus_distr_l. rewrite <- CR_of_Q_opp, <- CRmult_assoc, <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1#2)*-(2))%Q with (-(1))%Q. rewrite CR_of_Q_opp, <- CRopp_mult_distr_l, CRmult_1_l. rewrite CRplus_comm, CRmult_comm, CRopp_mult_distr_l. rewrite (CRopp_mult_distr_r eta b), (CRmult_comm eta (-b)). reflexivity. reflexivity. rewrite CRmult_plus_distr_l, CRmult_plus_distr_r. rewrite CRplus_comm, CRopp_plus_distr, CRopp_plus_distr, <- CRplus_assoc. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite CRmult_plus_distr_r, CRopp_plus_distr, <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite (CR_of_Q_plus R 1 1). rewrite <- (CRopp_mult_distr_l), CRmult_plus_distr_r, CRmult_1_l. rewrite <- (CRopp_mult_distr_l), CRmult_plus_distr_r. rewrite CRopp_plus_distr, (CRmult_comm eta). reflexivity. rewrite CRmult_plus_distr_l, CRmult_plus_distr_r. rewrite CRopp_plus_distr, CRopp_plus_distr. rewrite <- CRplus_assoc, <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite CRmult_plus_distr_r, CRopp_plus_distr. rewrite CRopp_mult_distr_l, CRopp_involutive. rewrite CRopp_mult_distr_r, CRopp_involutive. rewrite CRopp_mult_distr_l, CRopp_involutive, <- CRplus_assoc. apply CRplus_morph. rewrite (CR_of_Q_plus R 1 1). rewrite CRmult_plus_distr_r, CRmult_1_l, CRmult_plus_distr_r. rewrite (CRmult_comm eta a). reflexivity. rewrite CRopp_mult_distr_r. reflexivity. rewrite CRopp_plus_distr, CRopp_involutive, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l. reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. intro. reflexivity. intros. reflexivity. - intros. unfold CSUCUnitTrapeze. rewrite UCHeavisideIn. unfold UCUnitHeaviside. rewrite (CRinv_morph (b + eta - b) eta _ (inr etaPos)). rewrite CRmax_right. rewrite CRmin_right. apply (CRmult_eq_reg_l eta). right. apply etaPos. rewrite <- CRmult_assoc, <- CRopp_mult_distr_r, CRinv_r. unfold CRminus. rewrite (CRmult_plus_distr_l eta), CRmult_1_r. rewrite <- CRopp_mult_distr_r, <- CRmult_assoc, CRmult_comm, <- CRmult_assoc. rewrite CRinv_l, CRmult_1_l. rewrite <- CRopp_mult_distr_l, CRmult_1_l, CRopp_plus_distr, CRopp_plus_distr. rewrite CRopp_plus_distr, CRopp_involutive, CRopp_involutive. rewrite CRplus_comm, CRplus_assoc. reflexivity. apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm. apply H3. apply CRmin_glb. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. rewrite <- (CRplus_opp_r b). apply CRplus_le_compat_r. apply H3. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. apply (CRle_trans _ b _ leab). apply H3. - intros. rewrite CSUCTrapezePlateau. reflexivity. exact H3. - intros. unfold CSUCUnitTrapeze, UCUnitHeaviside. rewrite (CRinv_morph (a - (a- eta)) eta _ (inr etaPos)). rewrite (CRinv_morph (b + eta - b) eta _ (inr etaPos)). rewrite CRmax_right, CRmin_right. rewrite CRmax_left. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRmult_comm. apply CRmult_morph. reflexivity. apply CRplus_morph. reflexivity. rewrite CRplus_comm. rewrite CRopp_plus_distr, CRopp_involutive. reflexivity. apply (CRle_trans _ _ _ (CRmin_r _ _)). apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_0_l. apply (CRle_trans _ a). apply H3. exact leab. apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. apply (CRplus_le_reg_r (a - eta)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply H3. apply CRmin_glb. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_0_l. apply (CRplus_le_reg_r (a - eta)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_0_l. unfold CRminus. apply H3. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l. apply CRplus_0_l. unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive. apply CRplus_0_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont