proposition: Lemma SupDistanceToLinear_trans : forall x y a b (H:a < b), StepFSupBall (proj1_sig (SupDistanceToLinear x H + SupDistanceToLinear y H)%Qpos) x y.
proof: Proof. apply: StepF_ind2. intros s s0 t t0 Hs Ht H a b Hab. apply StepF_eq_change_base_setoid in Hs. apply StepF_eq_change_base_setoid in Ht. rewrite <- Hs, <- Ht at 2. setoid_replace (proj1_sig (SupDistanceToLinear s0 Hab + SupDistanceToLinear t0 Hab)%Qpos) with (proj1_sig (SupDistanceToLinear s Hab + SupDistanceToLinear t Hab)%Qpos). apply H. unfold QposEq. apply Qplus_wd; apply SupDistanceToLinear_wd2. apply StepF_eq_change_base_setoid in Hs. symmetry. exact Hs. apply StepF_eq_change_base_setoid in Ht. symmetry. exact Ht. intros x x0 a b H. unfold StepFSupBall, StepFfoldProp. simpl. rewrite -> Qball_Qabs. unfold SupDistanceToLinear. simpl. apply Qabs_case; intros H0. setoid_replace (x - x0)%Q with ((x - a) + (a - b) + (b - x0))%Q; [| now simpl; ring]. apply: plus_resp_leEq_both; simpl; auto with *. replace RHS with (Qmax (x-a) (b-x) + 0)%Q by simpl; ring. apply: plus_resp_leEq_both; simpl; auto with *. apply Qlt_le_weak. rewrite -> Qlt_minus_iff in *. replace RHS with (b + -a)%Q by simpl; ring. assumption. setoid_replace (-(x - x0))%Q with ((b - x) + - (b - a) + (x0 - a))%Q; [| now simpl; ring]. apply: plus_resp_leEq_both; simpl; auto with *. replace RHS with (Qmax (x-a) (b-x) + 0)%Q by simpl; ring. apply: plus_resp_leEq_both; simpl; auto with *. apply Qlt_le_weak. rewrite -> Qlt_minus_iff in *. replace RHS with (b + -a)%Q by simpl; ring. assumption. intros o s s0 t t0 H0 H1 a b H. assert (X:forall (o : OpenUnit) (l r : StepQ) (a b : Q) (H : a < b), QposEq (SupDistanceToLinear (glue o l r) H) (Qpos_max (SupDistanceToLinear l (affineCombo_gt (OpenUnitDual o) H)) (SupDistanceToLinear r (affineCombo_lt (OpenUnitDual o) H)))%Q). { intros. unfold QposEq. autorewrite with QposElim. apply SupDistanceToLinear_glue. } assert (QposEq (SupDistanceToLinear (glue o s s0) H + SupDistanceToLinear (glue o t t0) H) (Qpos_max (SupDistanceToLinear s (affineCombo_gt (OpenUnitDual o) H)) (SupDistanceToLinear s0 (affineCombo_lt (OpenUnitDual o) H)) + Qpos_max (SupDistanceToLinear t (affineCombo_gt (OpenUnitDual o) H)) (SupDistanceToLinear t0 (affineCombo_lt (OpenUnitDual o) H)))) as balleq. { unfold QposEq. unfold QposEq in X. simpl. do 2 rewrite X. reflexivity. } apply (@StepFSupBall_wd _ _ _ balleq _ _ (reflexivity _) _ _ (reflexivity _)). clear balleq. rewrite -> (StepFSupBallGlueGlue _ _ o s s0 t t0). split. - eapply ball_weak_le;[|simpl; apply H0]. simpl. do 2 rewrite Q_Qpos_max. apply Qplus_le_compat; apply Qmax_ub_l. - eapply ball_weak_le;[|simpl; apply H1]. simpl. do 2 rewrite Q_Qpos_max. apply Qplus_le_compat; apply Qmax_ub_r. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.IntegrableFunction CoRN.model.metric2.BoundedFunction CoRN.model.metric2.CRmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.ftc.Integral CoRN.model.structures.StepQsec CoRN.model.structures.OpenUnit CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetric CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.model.metric2.Qmetric CoRN.reals.fast.ContinuousCorrect CoRN.ftc.IntegrationRules CoRN.ftc.MoreIntegrals CoRN.tactics.CornTac CoRN.model.metric2.LinfDistMonad