proposition: Lemma IntegralDistance_triang : forall { IS : IntegrationSpace } (f g h : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g) (hInt : IntegrableFunction h), IntegralDistance fInt hInt <= IntegralDistance gInt fInt + IntegralDistance gInt hInt.
proof: Proof. intros. unfold IntegralDistance. rewrite <- IntegralPlus. apply IntegralNonDecreasing. intros x xdf xdg. destruct xdf, xdg. rewrite applyXabs, (applyXplus _ _ x d1 d2). rewrite (applyXminus f h x d d0). setoid_replace (partialApply f x d - partialApply h x d0) with (partialApply f x d - partialApply g x (fst d2) + (partialApply g x (fst d2) - partialApply h x d0)). apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply CRplus_le_compat. rewrite CRabs_minus_sym. rewrite applyXabs. destruct d1. rewrite (applyXminus g f x d1 d3), (DomainProp g x (fst d2) d1). rewrite (DomainProp f x d3 d). apply CRle_refl. rewrite applyXabs. destruct d2. rewrite (applyXminus g h x d2 d3), (DomainProp h x d3 d0). apply CRle_refl. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase