proposition: Lemma wd (from1 from2: Q) (w: bool -> Qpos) (e: bool -> Qpos) (fE: from1 == from2) (wE: QposEq (w true) (w false)): @ball Q_as_MetricSpace (proj1_sig (e true + e false)%Qpos) (approx from1 (w true) (e true)) (approx from2 (w false) (e false)).
proof: Proof. Proof with auto. set (halfe b := (e b * (1 # 2))%Qpos). set (m (b : bool) := intervals (if b then from1 else from2) (w b) (halfe b)). intros. unfold approx. simpl. do 2 rewrite fastΣ_correct. assert ((e true * (1#2))%Qpos = halfe true) by reflexivity. simpl in H. rewrite H. clear H. assert ((e false * (1#2))%Qpos = halfe false) by reflexivity. simpl in H. rewrite H. clear H. replace (intervals from1 (w true) (halfe true)) with (m true) by reflexivity. replace (intervals from2 (w false) (halfe false)) with (m false) by reflexivity. do 2 rewrite Σ_mult. apply Qball_hetero_Σ. unfold Basics.compose, Qdiv. intros. rewrite (Qmult_assoc (/m false)). rewrite (Qmult_assoc (/m true)). setoid_replace (/ m false * (proj1_sig (w true) * / m true)) with (/ m true * (proj1_sig (w false) * / m false)) by (unfold QposEq in wE; rewrite wE; change (Qeq (/ m false * (proj1_sig (w false) * / m true)) (/ m true * (proj1_sig (w false) * / m false))); ring). replace ((/ m true * (proj1_sig (w false) * / m false))%Q) with (proj1_sig (Qpos_inv (m true #1) * (w false * Qpos_inv (m false #1)))%Qpos) by reflexivity. apply (Qball_Qmult_l (((e true) + (e false)) * (1 # m true * m false))%Qpos). assert (QposEq (((e true + e false) * (1 # m true * m false) * Qpos_inv (Qpos_inv (m true #1) * (w false * Qpos_inv (m false #1))))%Qpos) (halfe true * Qpos_inv (w true) + (halfe true * Qpos_inv (w true) + halfe false * Qpos_inv (w false)) + halfe false * Qpos_inv (w false))%Qpos). { unfold QposEq, Qpos_inv; simpl. setoid_replace (1 # m true * m false) with ((1 # m true) * (1# m false)) by reflexivity. setoid_replace (/ (m true#1)) with (1# m true) by reflexivity. setoid_replace (/ (m false#1)) with (1# m false) by reflexivity. unfold QposEq in wE. rewrite wE. field. split. apply Qpos_nonzero. split; discriminate. } unfold QposEq in H0. rewrite H0. clear H0. repeat split; try discriminate... unfold intervals in m. apply (ball_triangle CR (proj1_sig (halfe true * Qpos_inv (w true))%Qpos) (proj1_sig (halfe false * Qpos_inv (w false))%Qpos) _ (f (from2 + i * / (m true * m false)%positive * proj1_sig (w false))) _). rewrite <- fE. unfold QposEq in wE. rewrite <- wE. apply (sampling_over_subdivision from1 i (m false) (halfe true) (w true))... apply ball_sym. rewrite Pmult_comm. apply sampling_over_subdivision. rewrite Pmult_comm... unfold intervals in m. apply (ball_triangle CR (proj1_sig (halfe true * Qpos_inv (w true))%Qpos) (proj1_sig (halfe false * Qpos_inv (w false))%Qpos) _ (f (from2 + i * / (m true * m false)%positive * proj1_sig (w false))) _). rewrite <- fE. unfold QposEq in wE. rewrite <- wE. apply (sampling_over_subdivision from1 i (m false) (halfe true) (w true))... apply ball_sym. rewrite Pmult_comm. apply sampling_over_subdivision. rewrite Pmult_comm... Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal CoRN.stdlib_omissions.List Coq.Unicode.Utf8 Coq.QArith.QArith Coq.QArith.Qabs CoRN.model.totalorder.QposMinMax CoRN.util.Qsums CoRN.model.metric2.Qmetric CoRN.model.setoids.Qsetoid CoRN.reals.fast.CRArith QnonNeg CoRN.util.Qgcd Coq.Program.Program CoRN.reals.fast.uneven_CRplus CoRN.stdlib_omissions.P CoRN.stdlib_omissions.Z CoRN.stdlib_omissions.Q CoRN.tactics.Qauto CoRN.ode.metric CoRN.ode.FromMetric2 MathClasses.implementations.stdlib_rationals