proposition: Lemma added_summations: Qball (proj1_sig e + proj1_sig e) (Σ (Pos.to_nat (wbints true)) approx0 * (proj1_sig (ww true) / Zpos (wbints true)) + Σ (Pos.to_nat (wbints false)) approx1 * (proj1_sig (ww false) / Zpos (wbints false))) (Σ (Pos.to_nat w01ints) approx01 * (proj1_sig totalw / Zpos w01ints)).
proof: Proof. Proof with auto with *. destruct (Qpos_gcd3 (ww true * (1# wbints true)) (ww false * (1# wbints false)) (totalw * (1# w01ints))) as [x [i [E [j [F [k G]]]]]]. rewrite <- E, <- F, <- G. repeat rewrite Qmult_assoc. rewrite <- Qmult_plus_distr_l. apply (Qball_Qmult_r (e+e)). rewrite <- (inject_nat_convert i), <- (inject_nat_convert j), <- (inject_nat_convert k). do 3 rewrite Qmult_Σ. replace (Pos.to_nat k * Pos.to_nat w01ints)%nat with (Pos.to_nat i * Pos.to_nat (wbints true) + Pos.to_nat j * Pos.to_nat (wbints false))%nat. Focus 2. apply surj_eq. rewrite <- Q.Qeq_Zeq. apply (Q.Qmult_injective_l (proj1_sig x)). apply Qpos_nonzero. rewrite inj_plus, inj_mult, inj_mult, inj_mult. repeat rewrite inject_nat_convert. rewrite Q.Zplus_Qplus. repeat rewrite Q.Zmult_Qmult. rewrite Qmult_plus_distr_l. rewrite (Qmult_comm i). rewrite (Qmult_comm j). rewrite (Qmult_comm k). repeat rewrite <- Qmult_assoc. rewrite E, F, G. simpl. setoid_replace (wbints true #1) with (/ (1#wbints true)) by reflexivity. setoid_replace (wbints false #1) with (/ (1#wbints false)) by reflexivity. setoid_replace (w01ints #1) with (/ (1#w01ints)) by reflexivity. field. repeat split; discriminate. do 2 rewrite <- nat_of_P_mult_morphism. rewrite Nat.add_comm. rewrite Σ_plus_bound. setoid_replace (proj1_sig (e + e)%Qpos / proj1_sig x) with (proj1_sig ((ec true + ec true) * Qpos_inv x + (ec false + ec false) * Qpos_inv x)%Qpos). Focus 2. unfold ec, QposEq. simpl. field. split... apply (Qpos_nonzero (ww true + ww false)). subst approx0 approx1 approx01. unfold flip, Basics.compose. assert (~ proj1_sig (ww true) + proj1_sig (ww false) == 0). apply (Qpos_nonzero (ww true + ww false)). assert (Zpos i == (proj1_sig (ww true) / wbints true / proj1_sig x)) as iE. apply (Qmult_injective_l (proj1_sig x)). apply Qpos_nonzero. rewrite E. simpl. setoid_replace (wbints true #1) with (/ (1#wbints true)) by reflexivity. field. split. discriminate. apply Qpos_nonzero. assert (Zpos j == (proj1_sig (ww false) / wbints false / proj1_sig x)) as jE. { apply (Qmult_injective_l (proj1_sig x)). apply Qpos_nonzero. rewrite F. simpl. setoid_replace (wbints false #1) with (/ (1#wbints false)) by reflexivity. field. split. discriminate. apply Qpos_nonzero. } assert (Zpos k == (proj1_sig totalw / w01ints / proj1_sig x)) as kE. { apply (Qmult_injective_l (proj1_sig x)). apply Qpos_nonzero. rewrite G. simpl. setoid_replace (w01ints #1) with (/ (1#w01ints)) by reflexivity. field. split. discriminate. apply Qpos_nonzero. } apply Qball_plus. apply Σ_Qball_pos_bounds. intros i0 i0E. set (ebit (b : bool) := if b then (ec true * (1 # 2) * Qpos_inv (ww true))%Qpos else (e * (1 # 2) * Qpos_inv totalw)%Qpos). setoid_replace (proj1_sig ((ec true + ec true) * Qpos_inv x)%Qpos * (1# i * wbints true)%positive) with (proj1_sig (ebit true + (ebit true + ebit false) + ebit false)%Qpos). Focus 2. unfold QposEq. simpl. assert (proj1_sig x == (proj1_sig (ww true) / Zpos (wbints true) / Zpos i)) as xE. apply Q.Qmult_injective_r with i... rewrite <- E. simpl. field... rewrite xE. unfold Qpos_mult. simpl. setoid_replace (1 # i * wbints true) with ((/i) * / wbints true) by reflexivity. field. split. apply (Qpos_nonzero (ww true + ww false)). split. apply Qpos_nonzero. split; discriminate. subst ec. simpl in ebit. apply (ball_triangle CR (proj1_sig (ebit true)) (proj1_sig (ebit false)) (f _) (f (a + i0 * (proj1_sig totalw / (Zpos w01ints * Zpos k)))) (f _))... setoid_replace (proj1_sig (ebit true)) with (proj1_sig (ebit false)) by (simpl; field; auto). unfold ebit. setoid_replace (proj1_sig totalw / (w01ints * k))%Q with ((/ (Zpos (wbints true) * Zpos i) * proj1_sig (ww true))) by (unfold Q_eq; rewrite kE, iE; simpl; field; auto). setoid_replace (proj1_sig (e * (1 # 2) * Qpos_inv totalw)%Qpos) with (proj1_sig (e * (ww true * Qpos_inv totalw) * (1 # 2) * Qpos_inv (ww true))%Qpos) by (simpl; field; auto). rewrite <- Pmult_Qmult. rewrite Qmult_assoc. apply sampling_over_subdivision... rewrite Pmult_comm... apply ball_sym. unfold ebit. setoid_replace (i0 * (proj1_sig totalw / (Zpos w01ints * Zpos k))) with (i0 * / Zpos (w01ints * k) * proj1_sig totalw). apply sampling_over_subdivision... rewrite Pmult_comm. apply Nat.lt_trans with (Pos.to_nat (i * wbints true))... apply inj_lt_iff. rewrite Zlt_Qlt. do 2 rewrite ZL9. do 2 rewrite Pmult_Qmult. fold w01ints. rewrite iE. rewrite kE. simpl. field_simplify... apply Qmult_lt_compat_r... apply Qinv_lt_0_compat... rewrite <- Qplus_0_r at 1. apply Qplus_lt_r... rewrite Pmult_Qmult. unfold Qdiv. unfold Q_eq. ring. apply Σ_Qball_pos_bounds. intros i0 i0E. set (ebit (b : bool) := if b then (ec false * (1 # 2) * Qpos_inv (ww false))%Qpos else (e * (1 # 2) * Qpos_inv totalw)%Qpos). assert (QposEq ((ec false + ec false) * Qpos_inv x * (1# j * wbints false)%positive)%Qpos (ebit true + (ebit true + ebit false) + ebit false)%Qpos). { unfold QposEq. simpl. setoid_replace (1 # j * wbints false) with ((/j) * / wbints false) by reflexivity. rewrite jE. simpl. field. split. apply (Qpos_nonzero (ww true + ww false)). split. apply Qpos_nonzero. split. discriminate. apply Qpos_nonzero. } unfold QposEq in H0. rewrite H0. clear H0. apply (ball_triangle CR (proj1_sig (ebit true)) (proj1_sig (ebit false)) _ (f (a + proj1_sig (ww true) + i0 * (proj1_sig totalw / (Zpos w01ints * Zpos k)))) _)... setoid_replace (proj1_sig (ebit true)) with (proj1_sig (ebit false)) by (simpl; field; auto). unfold ebit. setoid_replace (proj1_sig totalw / (Zpos w01ints * Zpos k)) with ((/ (Zpos (wbints false) * Zpos j) * proj1_sig (ww false))) by (rewrite kE, jE; unfold Q_eq; simpl; field; auto). assert (QposEq (e * (1 # 2) * Qpos_inv totalw)%Qpos (e * (ww false * Qpos_inv totalw) * (1 # 2) * Qpos_inv (ww false))%Qpos) by (unfold QposEq; simpl; field; auto). unfold QposEq in H0. rewrite H0. clear H0. rewrite <- Pmult_Qmult. rewrite Qmult_assoc. apply sampling_over_subdivision... rewrite Pmult_comm... apply ball_sym. setoid_replace (a + proj1_sig (ww true) + i0 * (proj1_sig totalw / (Zpos w01ints * Zpos k))) with (a + (i * wbints true + i0) * (proj1_sig totalw / (Zpos w01ints * Zpos k))) by (rewrite iE, kE; unfold Q_eq; simpl; field; auto). rewrite <- Pmult_Qmult. setoid_replace ((Zpos (i * wbints true) + i0) * (proj1_sig totalw / (Zpos w01ints * Zpos k))) with ((Pos.to_nat (i * wbints true) + i0)%nat * / Zpos (intervals lmu a totalw (e * (1#2)) * k) * proj1_sig totalw). apply (sampling_over_subdivision f a (Pos.to_nat (i * wbints true) + i0) k (e*(1#2)) totalw). fold w01ints. apply Nat.lt_le_trans with (Pos.to_nat (i * wbints true) + Pos.to_nat (j * wbints false)%positive)%nat... apply inj_le_iff. rewrite Zle_Qle. rewrite inj_plus. rewrite Zplus_Qplus. do 3 rewrite ZL9. do 3 rewrite Pmult_Qmult. rewrite iE, jE, kE. simpl. field_simplify... unfold Qdiv. rewrite (Qmult_comm (proj1_sig totalw)). rewrite inj_plus, Zplus_Qplus. rewrite <- Pmult_Qmult. rewrite Qmult_assoc. rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. reflexivity. 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