proposition: Lemma sampling_over_subdivision (fr: Q) (i: nat) (t: positive) (he wb: Qpos) : (i < Pos.to_nat (intervals fr wb he * t))%nat -> ball (proj1_sig (he * Qpos_inv wb)%Qpos) (f (fr + plus_half_times (i / Pos.to_nat t)%nat (proj1_sig wb * / Zpos (intervals fr wb he)))) (f (fr + i * / Zpos (intervals fr wb he * t) * proj1_sig wb)).
proof: Proof. Proof with auto. intro ile. unfold plus_half_times. apply ball_sym. assert (A1 : Qball (proj1_sig wb) fr (fr + i * / Zpos (intervals fr wb he * t) * proj1_sig wb)). { rewrite <- (Qplus_0_r fr) at 1. apply Qball_plus_r. apply in_Qball. split. apply Qle_trans with 0... unfold Qminus. rewrite Qplus_0_l. apply (Qopp_le_compat 0). apply Qpos_nonneg. apply Qmult_le_0_compat. auto. apply Qpos_nonneg. rewrite Qplus_0_l. apply (Qle_trans _ (1 * `wb)). apply Qmult_le_compat_r. 2: apply Qpos_nonneg. 2: rewrite Qmult_1_l; apply Qle_refl. apply Qmult_le_r with (Zpos (intervals fr wb he * t))... rewrite <- Qmult_assoc. rewrite Qmult_inv_r. rewrite Qmult_1_r. rewrite Qmult_1_l. rewrite <- Zle_Qle. rewrite <- ZL9. apply inj_le; auto with arith. intro. assert (0 < / (intervals fr wb he * t)%positive). apply Qinv_lt_0_compat... revert H0. rewrite H. apply (Qlt_irrefl 0). } assert (A2 : mspc_ball (lmu fr (proj1_sig wb) (proj1_sig he / proj1_sig wb)) (fr + i / ((intervals fr wb he * t) #1) * proj1_sig wb) (fr + ((i / Pos.to_nat t)%nat * (proj1_sig wb / ((intervals fr wb he)#1)) + (1 # 2) * (proj1_sig wb / ((intervals fr wb he)#1))))). unfold intervals. destruct (lmu fr (proj1_sig wb) (proj1_sig he / proj1_sig wb)) as [q |] eqn:L; [| apply mspc_inf]. unfold mspc_ball, msp_mspc_ball. assert (q_pos : 0 < q). { change (Qinf.lt 0 q). rewrite <- L. apply (uc_pos (restrict f fr (proj1_sig wb))). apply UC. apply (Qpos_ispos (he * Qpos_inv wb)). } set (q' := exist _ q q_pos : Qpos). change q with (proj1_sig q'). apply ball_sym, Qball_plus_r. change ((1 # 2) * proj1_sig wb / proj1_sig q')%Q with (proj1_sig ((1 # 2) * wb * Qpos_inv q')%Qpos). set (mym := QposCeiling (proj1_sig ((1 # 2) * wb * Qpos_inv q')%Qpos)). apply ball_weak_le with (proj1_sig (wb * (1#2) * Qpos_inv (mym#1))%Qpos). simpl. rewrite (Qmult_comm (proj1_sig wb)). subst mym. rewrite QposCeiling_Qceiling. apply Qle_shift_div_r... apply Qlt_le_trans with (proj1_sig ((1#2) * wb * Qpos_inv q')%Qpos)... apply Qround.Qle_ceiling. setoid_replace ((1#2) * proj1_sig wb) with (proj1_sig (q' * ((1#2) * wb * Qpos_inv q'))%Qpos). apply Qmult_le_l. exact q_pos. apply Qround.Qle_ceiling. simpl. field. intro abs. clear q'. rewrite abs in q_pos. exact (Qlt_irrefl 0 q_pos). apply Qball_Qdiv_inv with (Qpos_inv (mym#1) * wb)%Qpos. simpl. field_simplify... unfold Qdiv. rewrite Qmult_plus_distr_l. field_simplify... try rewrite Qdiv_1_r. setoid_replace (proj1_sig wb * (1 # 2) * / (mym#1) * / (/ (mym#1) * proj1_sig wb))%Q with (1#2). Focus 2. simpl. field. split; try discriminate... rewrite Nat2Z.inj_div... rewrite Q.Zdiv_Qdiv. setoid_replace ((mym # 1) * i / ((mym * t)%positive # 1)) with (i / t). rewrite positive_nat_Z. apply (Qfloor_ball (i/t)). unfold Qeq; simpl. destruct i. reflexivity. simpl. do 2 rewrite Pos.mul_1_r. rewrite Pos.mul_assoc. rewrite (Pos.mul_comm mym). reflexivity. discriminate. split. discriminate. split. 2: apply Qpos_nonzero. unfold Qeq; discriminate. split. discriminate. apply Qpos_nonzero. assert (A3 : Qball (proj1_sig wb) fr (fr + ((i / Pos.to_nat t)%nat * (proj1_sig wb * / Zpos (intervals fr wb he)) + (1 # 2) * (proj1_sig wb * / Zpos (intervals fr wb he))))). { set (n := intervals fr wb he). rewrite <- (Qplus_0_r fr) at 1. apply Qball_plus_r. apply in_Qball; unfold Qminus; rewrite !Qplus_0_l; split. apply Qle_trans with (y := 0). apply (Qopp_le_compat 0), Qpos_nonneg. Qauto_nonneg. rewrite <- Qmult_plus_distr_l, (Qmult_comm (proj1_sig wb)), Qmult_assoc. apply (Qle_trans _ (1 * proj1_sig wb)). 2: simpl; rewrite Qmult_1_l; apply Qle_refl. apply Qmult_le_compat_r; [| auto]. apply Qdiv_le_1. split. Qauto_nonneg. rewrite <- (positive_nat_Z n). apply Qlt_le_weak. apply Q.nat_lt_Qlt. apply Nat.div_lt_upper_bound. apply Pos2Nat_nonneg. rewrite <- (Pos2Nat.inj_mul t n). rewrite (Pos.mul_comm t n). apply ile. apply Qpos_nonneg. } apply ball_mspc_ball. eapply luc with (a := fr) (r := proj1_sig wb); [apply UC | | | |]. apply Qpos_ispos. apply A1. apply A3. apply A2. 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