proposition: Lemma L1Norm_Zero : forall s, (L1Norm s <= 0)%Q -> s == (constStepF (0:QS)).
proof: Proof. intros s. intros Hs. induction s. apply: Qle_antisym. eapply Qle_trans;[apply Qle_Qabs|assumption]. rewrite <- (Qopp_involutive x). change 0 with (- (- 0))%Q. apply Qopp_le_compat. eapply Qle_trans;[apply Qle_Qabs|]. rewrite -> Qabs_opp. assumption. unfold L1Norm, StepQabs in *. rewrite MapGlue in Hs. rewrite -> Integral_glue in Hs. apply glue_StepF_eq. apply IHs1. unfold L1Norm. setoid_replace 0 with (0/o); [| simpl; field; auto with *]. apply Qle_shift_div_l; auto with *. rewrite -> Qmult_comm. apply Qle_trans with (-((1 - o) * IntegralQ (QabsS ^@> s2)))%Q. rewrite -> Qle_minus_iff. rewrite -> Qle_minus_iff in Hs. replace RHS with (0 + - (o * IntegralQ (QabsS ^@> s1) + (1 - o) * IntegralQ (QabsS ^@> s2)))%Q by simpl; ring. assumption. change 0 with (-0)%Q. apply Qopp_le_compat. apply: mult_resp_nonneg; simpl; auto with *. apply: L1Norm_nonneg. apply IHs2. unfold L1Norm. setoid_replace 0 with (0/(1-o)); [| simpl; field; auto with *]. apply Qle_shift_div_l; auto with *. rewrite -> Qmult_comm. apply Qle_trans with (-(o * IntegralQ (QabsS ^@> s1)))%Q. rewrite -> Qle_minus_iff. rewrite -> Qle_minus_iff in Hs. replace RHS with (0 + - (o * IntegralQ (QabsS ^@> s1) + (1 - o) * IntegralQ (QabsS ^@> s2)))%Q by simpl; ring. assumption. change 0 with (-0)%Q. apply Qopp_le_compat. apply: mult_resp_nonneg; simpl; auto with *. apply L1Norm_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac