proposition: Lemma CompactTotalBoundNotFar : forall (s:Compact X) (e:Qpos), @ball (FinEnum (Complete X)) ((3#5)*proj1_sig e) (map Cunit (approximate s ((1#5)*e)%Qpos)) (CompactTotalBound s e).
proof: Proof. intros s e. unfold CompactTotalBound. generalize (CompactTotallyBoundedNotFar s (1#4)%Qpos ((1#5)*e) ((1#5)*e) QuarterLeHalf). generalize (CompactTotallyBounded_fun s (1 # 4) ((1 # 5) * e) ((1 # 5) * e) QuarterLeHalf). induction (approximate s ((1 # 5) * e)%Qpos) as [|a s0]; intros H L. - apply ball_refl. apply (Qpos_nonneg ((3#5)*e)). - unfold Qdiv in L. split. apply (Qpos_nonneg ((3#5)*e)). split; intros x Hx. + apply FinSubset_ball_orC in Hx. destruct Hx as [G | Hx | Hx] using orC_ind. auto using existsC_stable. apply existsWeaken. exists (H a (InFinEnumC_weaken X a (a :: s0) (or_introl eq_refl))). split. intro abs; contradict abs. exists (H a (InFinEnumC_weaken X a (a :: s0) (or_introl eq_refl))). split. left. reflexivity. reflexivity. rewrite -> Hx. setoid_replace ((3 # 5) * proj1_sig e) with (((5 # 4) * proj1_sig ((1 # 5) * e)%Qpos + proj1_sig ((1 # 5) * e)%Qpos) * (4 # 3)) by (simpl; ring). apply L. set (H':=(fun pt (Hpt : InFinEnumC pt s0) => H pt (FinSubset_ball_cons Hpt))). assert (L':forall (pt : X) (Hpt : InFinEnumC pt s0), ball (m:=Complete X) (((1 + proj1_sig (1 # 4)%Qpos) * proj1_sig ((1 # 5) * e)%Qpos + proj1_sig ((1 # 5) * e)%Qpos) * / (1 - proj1_sig (1 # 4)%Qpos)) (Cunit pt) (H' pt Hpt)). { intros pt Hpt. apply L. } destruct (IHs0 H' L') as [_ [A _]]. destruct (A x Hx) as [G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split; auto. exact (FinSubset_ball_cons Hy0). + apply FinSubset_ball_orC in Hx. destruct Hx as [G | Hx | Hx] using orC_ind. auto using existsC_stable. apply existsWeaken. exists (Cunit a). split. intro abs; contradict abs. exists (Cunit a). split. left. reflexivity. reflexivity. rewrite -> Hx. setoid_replace ((3 # 5) * proj1_sig e) with (((5 # 4) * proj1_sig ((1 # 5) * e)%Qpos + proj1_sig ((1 # 5) * e)%Qpos) * (4 # 3)) by (simpl; ring). apply ball_sym, L. set (H':=(fun pt (Hpt : InFinEnumC pt s0) => H pt (FinSubset_ball_cons Hpt))). assert (L':forall (pt : X) (Hpt : InFinEnumC pt s0), ball (m:=Complete X) (((1 + proj1_sig (1 # 4)%Qpos) * proj1_sig ((1 # 5) * e)%Qpos + proj1_sig ((1 # 5) * e)%Qpos) * / (1 - proj1_sig (1 # 4)%Qpos)) (Cunit pt) (H' pt Hpt)). intros pt Hpt. apply L. destruct (IHs0 H' L') as [_ [_ A]]. destruct (A x Hx) as [G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split; auto. exact (FinSubset_ball_cons Hy0). Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround