proposition: Lemma SupDistanceToLinear_scale : forall x c a b (H:a < b) (H0:c*a < c*b), (c*proj1_sig (SupDistanceToLinear x H) == proj1_sig (SupDistanceToLinear (constStepF (c:QS) * x) H0))%Q.
proof: Proof. intros x c a b H H0. assert (X:0 < c). rewrite -> Qlt_minus_iff in *|-. apply: (mult_cancel_less _ 0 c (b + - a))%Q; simpl; auto with *. replace LHS with 0 by simpl; ring. replace RHS with (c* b + - (c*a))%Q by simpl; ring. assumption. revert c a b H H0 X. induction x. intros; unfold SupDistanceToLinear; simpl. autorewrite with QposElim. rewrite -> Qmax_mult_pos_distr_r; auto with *. apply Qmax_compat; ring. intros c a b H H0 X. change (constStepF (X:=QS) c * glue o x1 x2) with (glue o (constStepF (c:QS) * x1) (constStepF (c:QS) * x2)). do 2 rewrite -> SupDistanceToLinear_glue. eapply Seq_trans. apply Q_Setoid. apply Qmax_mult_pos_distr_r; auto with *. set (A:=(affineCombo_gt (OpenUnitDual o) H)). apply Qmax_compat. eapply Seq_trans. apply Q_Setoid. apply (IHx1 c _ _ A (mult_resp_less_lft _ _ _ _ A X)); auto with *. apply SupDistanceToLinear_wd1; try reflexivity. unfold affineCombo; ring. set (B:=(affineCombo_lt (OpenUnitDual o) H)). eapply Seq_trans. apply Q_Setoid. apply (IHx2 c _ _ B (mult_resp_less_lft _ _ _ _ B X)); auto with *. apply SupDistanceToLinear_wd1; try reflexivity. unfold affineCombo; ring. 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