Skip to content

Instantly share code, notes, and snippets.

@zeng-y-l

zeng-y-l/elem.v Secret

Created October 10, 2025 03:33
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save zeng-y-l/afdd222e79059ce0d3651fc53c87c98a to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save zeng-y-l/afdd222e79059ce0d3651fc53c87c98a to your computer and use it in GitHub Desktop.
Download ZIP
所有整数数列都有初等通项公式
Raw
elem.v
From Coq Require Import Reals Lra Psatz Field ZArith Lia FinFun Reals.Runcountable Classical Logic.ClassicalChoice Lists.List QArith.
Open Scope R_scope.
Inductive 初等 :=
| Id
| Cst (a : R)
| Opp
| Inv
| Tan
| Atan
| Exp
| Ln
| Add (a b : 初等)
| Mul (a b : 初等)
| Comp (g f : 初等).
Fixpoint eval (f : 初等) x := match f with
| Id => x
| Cst a => a
| Opp => -x
| Inv => /x
| Tan => tan x
| Atan => atan x
| Exp => exp x
| Ln => ln x
| Add a b => eval a x + eval b x
| Mul a b => eval a x * eval b x
| Comp g f => eval g (eval f x)
end.
(* x - 1/2 - 1/pi * atan(tan(pi * (1/2 + x))) *)
Definition 取整 : 初等 :=
Add Id (Add (Cst (-/2)) (Comp Opp (Mul (Cst (/PI))
(Comp Atan (Comp Tan (Mul (Cst PI) (Add (Cst (/2)) Id))))
))).
Theorem 取整取整 : forall x,
x > 0 -> (forall y, x <> INR y) ->
eval 取整 x = IZR (Int_part x).
Proof.
assert (forall (n : nat) x,
INR n - 1 < x < INR n ->
eval 取整 x = IZR (Int_part x)).
{ induction n; intros; simpl in *; unfold Int_part in *.
- rewrite atan_tan. field_simplify. rewrite <- (tech_up x 0).
simpl. lra. lra. lra. apply PI_neq0.
split; apply (Rmult_lt_reg_r (/PI));
try (apply Rinv_0_lt_compat; apply PI_RGT_0);
field_simplify; try apply PI_neq0.
replace (-PI / (2 * PI)) with (-/2).
lra. field. apply PI_neq0. lra.
- assert (INR n - 1 < x - 1 < INR n).
{ inversion H. destruct n; split; try lra; simpl; lra. }
specialize (IHn (x - 1) H0). simpl in IHn.
rewrite minus_IZR in IHn.
replace (up (x - 1)) with (up x - 1)%Z in IHn.
rewrite <- Rtrigo_facts.tan_pi_plus in IHn.
replace (PI + PI * _) with (PI * (/ 2 + x)) in IHn.
apply (Rplus_eq_compat_r 1) in IHn.
field_simplify in IHn. field_simplify. apply IHn.
apply PI_neq0. apply PI_neq0. auto. field.
+ intro. apply cos_eq_0_0 in H1. inversion H1.
assert (x - 1 = IZR x0).
{ replace (IZR x0 * PI + PI / 2) with ((IZR x0 + /2) * PI) in H2.
apply (Rmult_eq_reg_r PI). lra. apply PI_neq0. field. }
rewrite H3 in H0. rewrite INR_IZR_INZ in H0. inversion H0.
replace (IZR _ - 1) with (IZR (Z.of_nat n - 1)) in H4.
apply lt_IZR in H4, H5. lia. apply minus_IZR.
+ destruct (archimed x).
rewrite (tech_up (x - 1) (up x - 1)); auto;
rewrite minus_IZR; lra. }
intros. destruct (archimed x).
destruct (IZN (up x)) as [n]. apply le_IZR. lra.
apply (H n). rewrite H4, <- INR_IZR_INZ in H2, H3. split.
specialize (H1 (n - 1)%nat). rewrite minus_INR in H1. simpl in H1.
lra. destruct n. simpl in H2. lra. lia. lra.
Qed.
Definition pow2 := Comp Exp (Mul Id (Cst (ln 2))).
Theorem pow2Rpower : forall x,
eval pow2 x = Rpower 2 x.
Proof.
intros. simpl. reflexivity.
Qed.
(* floor(c * 2^a) - floor(c * 2^b) * 2^(a - b) - 1
a, b 为自然数 *)
Definition 取一段 (c a b : 初等) :=
Add (Cst (-1)) (Add
(Comp 取整 (Mul c (Comp pow2 a)))
(Comp Opp (Mul
(Comp 取整 (Mul c (Comp pow2 b)))
(Comp pow2 (Add a (Comp Opp b)))))).
(* f(x) 为自然数 *)
Definition 解码 (c f : 初等) :=
取一段 c (Add (Comp f (Add Id (Cst 1))) (Add Id (Cst 2)))
(Add (Comp f Id) (Add Id (Cst 1))).
Definition 因子加 f x a := Rpower 2 (f x + x + a).
Definition 因子 f x := 因子加 f x 1.
Definition 编码项 f a x := (1 + INR (a x)) / 因子 f (INR x + 1).
Definition 编码是 f a := Un_cv (sum_f_R0 (编码项 f a)).
Theorem 几何级数 : Un_cv (sum_f_R0 (fun i => / (2 ^ (S i)))) 1.
Proof.
pose proof (GP_infinite (/ 2)).
unfold Pser, infinite_sum in H.
eapply (CV_mult (fun _ => /2) _ (/2) _) in H. eapply Un_cv_ext in H.
replace (/2 * /(1 - /2)) with 1 in H. apply H. lra.
intros. rewrite scal_sum. apply sum_eq.
intros. simpl. rewrite <- Rinv_pow. field.
clear H0. induction i. lra. simpl. lra. lra.
unfold Un_cv. intros. exists 0%nat. intros. rewrite R_dist_eq. lra.
rewrite Rabs_pos_eq; lra.
Qed.
Theorem 几何级数收敛 : forall n,
sum_f_R0 (fun i => / (2 ^ (S i))) n <= 1.
Proof.
intros. pose proof 几何级数. eapply sum_incr in H.
apply H. intros. rewrite <- Rpower_pow.
apply Rlt_le, Rinv_0_lt_compat, exp_pos. lra.
Qed.
Theorem 常数收敛 : forall x, Un_cv (fun _ => x) x.
Proof.
intros. unfold Un_cv. intros. exists 0%nat. intros.
rewrite R_dist_eq. lra.
Qed.
Theorem 为正 : forall f a n,
编码项 f a n > 0.
Proof.
intros. unfold 编码项, Rpower. apply Rdiv_lt_0_compat.
pose proof (pos_INR (a n)). lra. apply exp_pos.
Qed.
Theorem 增长 : forall f a,
Un_growing (sum_f_R0 (编码项 f a)).
Proof.
unfold Un_growing. intros. simpl.
assert (编码项 f a (S n) > 0). 2:lra. apply 为正.
Qed.
Definition 能索引 f a := forall n,
0 <= eval f (INR n) <= eval f (INR n + 1) /\
1 + INR (a n) <=
Rpower 2 (eval f (INR n + 1) - eval f (INR n) - 1) /\
(exists x, eval f (INR n) = INR x).
Theorem 编码项范围 : forall f a n, 能索引 f a ->
编码项 (eval f) a n <= (/ 因子加 (eval f) (INR n) 3).
Proof.
intros. unfold 编码项.
destruct (H n) as [H1 [H2 _]].
eapply (Rmult_le_reg_r (因子 (eval f) (INR n + 1))).
apply exp_pos. field_simplify. unfold 因子, 因子加, "x / y".
rewrite <- Rpower_Ropp, <- Rpower_plus.
replace (eval f (INR n + 1) + (INR n + 1) + 1 +
- (eval f (INR n) + INR n + 3))
with (eval f (INR n + 1) - eval f (INR n) - 1).
rewrite Rplus_comm. apply H2. lra.
apply Rgt_not_eq; apply exp_pos.
apply Rgt_not_eq. apply exp_pos.
Qed.
Theorem 有编码 : forall f a,
能索引 f a -> exists c, 编码是 (eval f) a c.
Proof.
intros. unfold 编码是. edestruct Rseries_CV_comp.
2:{ eexists. apply 几何级数. }
2:{ exists x. apply u. }
intros. split. apply Rlt_le, 为正.
eapply Rle_trans. apply 编码项范围. auto.
rewrite <- Rpower_pow. apply Rinv_le_contravar. apply exp_pos.
apply Rle_Rpower. lra. rewrite S_INR.
eapply (Rplus_le_reg_r (-1)). field_simplify.
destruct (H n) as []. lra. lra.
Qed.
Theorem 编码为正 : forall f a c,
能索引 f a -> 编码是 (eval f) a c -> c > 0.
Proof.
intros. unfold 编码是 in H0.
eapply (Rlt_le_trans _ (sum_f_R0 _ 0) _). simpl. apply 为正.
apply sum_incr. apply H0. intros. apply Rlt_le. apply 为正.
Qed.
Theorem 加法单调 : forall f a n m,
能索引 f a -> eval f (INR n) <= eval f (INR (n + m)).
Proof.
intros. induction m.
- simpl. rewrite plus_0_r. lra.
- destruct (H (n + m)%nat) as [[_] _].
rewrite <- plus_n_Sm, S_INR. lra.
Qed.
Theorem 编码非整数 : forall f a n l,
能索引 f a ->
Un_cv (sum_f_R0 (fun i =>
编码项 (eval f) a (i + n) * 因子 (eval f) (INR n))) l ->
0 < l < 1.
Proof.
intros. split.
- eapply Rlt_le_trans; try eapply (sum_incr _ 0); try apply H0;
intros; simpl; try apply Rlt_le; apply Rmult_gt_0_compat;
try apply 为正; apply exp_pos.
- eapply Rle_lt_trans. eapply Rle_cv_lim. 2:apply H0.
2:{ eapply (CV_mult (fun _ => /2) _ (/2) _).
unfold Un_cv. intros. exists 0%nat. intros.
rewrite R_dist_eq. lra. apply 几何级数. }
intros. simpl. rewrite scal_sum.
apply sum_Rle. intros. clear H1 n0.
replace (/ (2 * 2 ^ n1) * / 2) with (/Rpower 2 (INR n1 + 2)).
apply (Rmult_le_reg_r (/ 因子 (eval f) (INR n))).
apply Rinv_0_lt_compat. apply exp_pos. field_simplify.
eapply Rle_trans. apply 编码项范围. auto.
unfold 因子, 因子加. rewrite <- Rpower_plus.
unfold "x / y". rewrite Rmult_1_l. apply Rinv_le_contravar.
apply exp_pos. apply Rle_Rpower. lra. rewrite plus_INR.
assert (eval f (INR n) <= eval f (INR n1 + INR n)).
{ rewrite <- plus_INR, plus_comm. eapply 加法单调. eauto. }
pose proof (plus_INR n1 n). lra.
split; apply Rgt_not_eq, exp_pos. apply Rgt_not_eq, exp_pos.
replace (INR n1 + 2) with (INR (S (S n1))).
rewrite Rpower_pow. simpl. field.
rewrite <- Rpower_pow. apply Rgt_not_eq, exp_pos. lra. lra.
repeat rewrite S_INR. lra. lra.
Qed.
Theorem 编码是整数 : forall f a n,
能索引 f a -> exists x,
INR x = 因子 (eval f) (INR n) *
(sum_f_R0 (编码项 (eval f) a) n - 编码项 (eval f) a n).
Proof.
intros. assert (forall m, exists x,
因子 (eval f) (INR m) * Rpower 2 (INR x)
= 因子 (eval f) (INR m + 1)).
{ intros. unfold 因子, 因子加.
destruct (H m) as [[_] [_ []]], (H (S m)) as [_ [_ []]].
rewrite <- S_INR, H1, H2 in H0. apply INR_le in H0.
rewrite S_INR in H2.
exists (S (x0 - x))%nat. rewrite <- Rpower_plus. f_equal.
rewrite S_INR, minus_INR, H1, H2. lra. auto. }
induction n.
- unfold 编码项, 因子, 因子加. simpl.
exists 0%nat. simpl. lra.
- destruct IHn, (H n) as [[_] [_ []]], (H0 n).
exists (x * 2 ^ x1 + (1 + a n))%nat.
rewrite S_INR, tech5, plus_INR. field_simplify.
replace (sum_f_R0 (编码项 (eval f) a) n)
with (let x := 编码项 (eval f) a in
sum_f_R0 x n - x n + x n).
rewrite Rmult_plus_distr_l. f_equal.
+ rewrite <- H4, mult_INR, H1, pow_INR, <- Rpower_pow.
replace (INR 2) with 2. repeat rewrite S_INR. lra.
auto. simpl. lra.
+ rewrite plus_INR. unfold 编码项, 因子, 因子加.
field_simplify. simpl. lra.
apply Rgt_not_eq. apply exp_pos.
+ lra.
Qed.
Theorem 编码分割 : forall f a c n,
能索引 f a -> 编码是 (eval f) a c ->
Un_cv (sum_f_R0 (fun i =>
编码项 (eval f) a (i + n) * 因子 (eval f) (INR n)))
((c - sum_f_R0 (编码项 (eval f) a) n + 编码项 (eval f) a n)
* 因子 (eval f) (INR n)).
Proof.
intros. unfold 编码是 in H0.
apply (let a :=
-sum_f_R0 (编码项 (eval f) a) n + 编码项 (eval f) a n in
CV_plus (fun _ => a) _ a _) in H0.
apply (CV_shift' _ n) in H0.
apply (let a := 因子 (eval f) (INR n) in
CV_mult (fun _ => a) _ a _) in H0.
eapply (Un_cv_ext _ (sum_f_R0 (fun i =>
编码项 (eval f) a (i + n)
* 因子 (eval f) (INR n)))) in H0.
2:{ intros. rewrite <- scal_sum. f_equal.
destruct n0. simpl. lra.
erewrite (tech2 (编码项 (eval f) a) n (S n0 + n)).
field_simplify. replace (S n0 + n - S n)%nat with n0.
rewrite (decomp_sum _ (S n0)). simpl. f_equal.
apply sum_eq. intros. f_equal. lia. lia. lia. lia. }
replace (c - _ + _) with (
- sum_f_R0 (编码项 (eval f) a) n + 编码项 (eval f) a n + c).
rewrite Rmult_comm. apply H0.
- lra.
- unfold Un_cv. intros. exists 0%nat. intros.
rewrite R_dist_eq. lra.
- unfold Un_cv. intros. exists 0%nat. intros.
rewrite R_dist_eq. lra.
Qed.
Theorem 编码取整 : forall f a c n,
能索引 f a -> 编码是 (eval f) a c ->
IZR (Int_part (因子 (eval f) (INR n) * c))
= 因子 (eval f) (INR n) *
(sum_f_R0 (编码项 (eval f) a) n - 编码项 (eval f) a n).
Proof.
intros. pose proof (编码分割 f a c n H H0).
edestruct (编码非整数 f a n). apply H. apply H1.
destruct (编码是整数 f a n). auto.
unfold Int_part. rewrite <- (up_tech _ (Z.of_nat x)).
- replace (Z.of_nat x + 1 - 1)%Z with (Z.of_nat x).
rewrite <- INR_IZR_INZ. auto. lia.
- rewrite <- INR_IZR_INZ, H4. lra.
- rewrite plus_IZR, <- INR_IZR_INZ, H4. lra.
Qed.
Theorem 编码乘法非整数 : forall f a c n x,
能索引 f a -> 编码是 (eval f) a c ->
c * 因子 (eval f) (INR n) <> INR x.
Proof.
intros. intro. pose proof (编码分割 f a c n H H0).
destruct (编码是整数 f a n H).
replace (c - _ + _) with (
c - (sum_f_R0 (编码项 (eval f) a) n - 编码项 (eval f) a n)
) in H2. 2:lra.
rewrite Rmult_minus_distr_r, H1, Rmult_comm, <- H3,
(INR_IZR_INZ x), (INR_IZR_INZ x0), <- minus_IZR in H2.
edestruct (编码非整数 f a n). apply H. apply H2.
apply lt_IZR in H4, H5. lia.
Qed.
Theorem 编解码 : forall f a c i,
能索引 f a -> 编码是 (eval f) a c ->
INR (a i) = eval (解码 (Cst c) f) (INR i).
Proof.
intros. unfold 解码, 取一段.
remember 取整 as 取整'. remember pow2 as pow2'.
simpl. subst 取整'. repeat rewrite 取整取整;
simpl; subst pow2'; repeat rewrite pow2Rpower; simpl.
- replace (c * Rpower 2 (eval f (INR i + 1) + (INR i + 2)))
with (因子 (eval f) (INR (S i)) * c).
2:{ unfold 因子, 因子加. rewrite Rmult_comm, S_INR.
f_equal. f_equal. lra. }
replace (c * Rpower 2 (eval f (INR i) + (INR i + 1)))
with (因子 (eval f) (INR i) * c).
2:{ unfold 因子, 因子加. rewrite Rmult_comm.
f_equal. f_equal. lra. }
repeat rewrite (编码取整 f a); auto.
rewrite (Rmult_comm _ (sum_f_R0 _ i - _)), Rmult_assoc.
unfold 因子, 因子加. rewrite S_INR, <- Rpower_plus.
(* replace (INR i + 1 + 1) with (INR i + 2). 2:lra. *)
replace (Rpower 2 (_ + (_ + - _)))
with (Rpower 2 (eval f (INR i + 1) + (INR i + 1) + 1)).
2:{ f_equal. field_simplify. lra. }
rewrite Rmult_comm, Ropp_mult_distr_l, <- Rmult_plus_distr_r.
simpl. field_simplify. unfold 编码项, 因子, 因子加.
field. apply Rgt_not_eq, exp_pos.
- apply Rmult_gt_0_compat. eapply 编码为正.
eauto. auto. apply exp_pos.
- intros.
replace (Rpower 2 (eval f (INR i) + (INR i + 1)))
with (因子 (eval f) (INR i)). eapply 编码乘法非整数.
apply H. auto. unfold 因子, 因子加. f_equal. lra.
- apply Rmult_gt_0_compat. eapply 编码为正.
eauto. auto. apply exp_pos.
- intros. replace (Rpower 2 (eval f (INR i + 1) + (INR i + 2)))
with (因子 (eval f) (INR (S i))). eapply 编码乘法非整数.
apply H. auto. unfold 因子, 因子加. f_equal.
rewrite S_INR. lra.
Qed.
Theorem 能索引则有通项 : forall a,
(exists f, 能索引 f a) ->
exists f, forall n, INR (a n) = eval f (INR n).
Proof.
intros a [f]. destruct (有编码 f a) as [c]. auto.
exists (解码 (Cst c) f). intros. apply 编解码; auto.
Qed.
Theorem 不用单调也行 : forall f a,
(forall n, 1 + INR (a n) <=
Rpower 2 (eval f (INR n + 1) - eval f (INR n) - 1) /\
(exists x, eval f (INR n) = INR x)) -> 能索引 f a.
Proof.
intros. assert (forall n,
eval f (INR n) <= eval f (INR n + 1)).
{ intros. destruct (H n) as [H0 _].
assert (0 <= eval f (INR n + 1) - eval f (INR n) - 1).
{ apply Rnot_lt_le. intro. apply (Rpower_lt 2) in H1.
rewrite Rpower_O in H1. pose proof (pos_INR (a n)).
lra. lra. lra. } lra. }
split; auto; split; auto.
destruct (H n) as [_ []]. rewrite H1. apply pos_INR.
Qed.
Theorem max更大 : forall f n m,
Rmax_N f n <= Rmax_N f (n + m).
Proof.
intros. induction m.
- rewrite plus_0_r. lra.
- rewrite <- plus_n_Sm. simpl.
eapply Rle_trans. eauto. apply Rmax_r.
Qed.
Theorem max大 : forall f n,
f n <= Rmax_N f n.
Proof.
intros. induction n.
- simpl. lra.
- simpl. apply Rmax_l.
Qed.
Theorem Req : exists Req : R -> R -> bool, forall x y,
(x = y <-> Req x y = true) /\ (x <> y <-> Req x y = false).
Proof.
assert (forall x : R * R, exists b,
fst x = snd x /\ b = true \/ fst x <> snd x /\ b = false).
{ intros. destruct (Req_dec (fst x) (snd x)); eauto. }
apply choice in H. destruct H as [Req].
exists (fun x y => Req (x, y)).
intros. split; split; intros;
destruct (H (x, y)) as [[]|[]];
simpl in *; try congruence; auto.
Qed.
Theorem 不重复的 : forall (f : nat -> R), exists f', forall n,
(forall i, f' (S i + n)%nat <> f' n) /\
(exists i, f n = f' i).
Proof.
intros. destruct Req as [Req].
pose (重复了 n := existsb (fun x => Req x (f (S n)))).
pose (f' := fix f' n := match n with
| 0 => (f 0%nat, f 0%nat :: nil)
| S n =>
let cur := if 重复了 n (snd (f' n))
then RList.MaxRlist (snd (f' n)) + 1
else f (S n) in
(cur, cur :: snd (f' n))
end).
assert (forall n x,
In x (snd (f' n)) <->
exists i, (i <= n)%nat /\ fst (f' i) = x).
{ intros. split; intros.
- induction n.
+ simpl in H0. destruct H0. eauto. inversion H0.
+ destruct H0. eauto. destruct IHn as [i []]. auto.
exists i. split. lia. auto.
- destruct H0 as [i []]. induction H0; simpl; auto.
induction i; simpl; auto. }
exists (fun n => fst (f' n)).
intros. split.
- intros. simpl.
assert (In (fst (f' n)) (snd (f' (i + n)%nat))).
{ induction i; simpl. apply H0. eauto. auto. }
destruct (
重复了 (i + n) (snd (f' (i + n))))%nat eqn:H2.
+ apply RList.MaxRlist_P1 in H1. lra.
+ assert (~In (f (S (i + n))) (snd (f' (i + n)%nat))).
{ intro. apply Bool.not_true_iff_false in H2.
apply H2. apply existsb_exists.
pose (a := f (S (i + n))). exists a. split. auto.
apply (H a a). auto. }
clear H2. intro. apply H3. rewrite H2. apply H0.
exists n. split. lia. auto.
- induction n.
{ exists 0%nat. simpl. auto. }
destruct (重复了 n (snd (f' n))) eqn:H1.
+ apply existsb_exists in H1. destruct H1 as [x []].
apply H0 in H1. destruct H1 as [i []]. subst.
apply (H (fst (f' i)) (f (S n))) in H2. eauto.
+ exists (S n). simpl. rewrite H1. auto.
Qed.
Theorem 有不同的 : forall (f : nat -> R), exists x, forall n,
f n <> x.
Proof.
intros. apply NNPP. intro.
destruct (不重复的 f) as [f'].
apply (R_uncountable f'). unfold Bijective.
assert (forall x, exists n, f' n = x).
{ intros. eapply not_ex_all_not, not_all_ex_not in H.
destruct H. apply NNPP in H. destruct (H0 x0) as [_ []].
eexists. rewrite <- H1. apply H. }
apply choice in H1. destruct H1 as [g].
exists g. split; auto. intros.
assert (forall n m, n <> m -> f' n <> f' m).
{ intros. destruct (gt_eq_gt_dec n m) as [[|]|].
- destruct (H0 n). specialize (H3 (m - S n)%nat).
replace (S (m - S n) + n)%nat with m in H3. auto. lia.
- auto.
- destruct (H0 m). specialize (H3 (n - S m)%nat).
replace (S (n - S m) + m)%nat with n in H3. auto. lia. }
apply NNPP. intro. apply H2 in H3. apply H3. apply H1.
Qed.
Theorem 总有非整数 : forall f, exists s, forall (n : nat) x,
0 < s < 1 /\ f n + s <> INR x.
Proof.
intros. destruct Req as [Req].
pose (f' n := let x := frac_part (f n) in
if Req x 0 then 0 else ln (/x - 1)).
destruct (有不同的 f').
pose (s := 1 - / (exp x + 1)). exists s.
assert (0 < s < 1).
{ assert (0 < / (exp x + 1) < 1). split.
- apply Rinv_0_lt_compat. pose proof (exp_pos x). lra.
- pose proof (exp_pos x). replace 1 with (/1).
apply Rinv_lt_contravar. lra. lra. lra.
- unfold s. destruct H1. lra. }
intros. split. auto. intro.
specialize (H0 n). unfold f' in H0.
destruct (Req (frac_part (f n)) 0) eqn:H3; apply H in H3.
- apply fp_nat in H3. destruct H3 as [fn].
apply (Rplus_eq_compat_r (-f n)) in H2.
field_simplify in H2. rewrite H2 in H1.
rewrite H3, INR_IZR_INZ, <- opp_IZR, <- plus_IZR in H1.
destruct H1. apply lt_IZR in H1, H4. lia.
- assert (1 - frac_part (f n) <> s).
{ unfold s. intro.
apply Rplus_eq_reg_l, Ropp_eq_compat in H4.
repeat rewrite Ropp_involutive in H4.
rewrite H4, Rinv_involutive in H0.
replace (exp x + 1 - 1) with (exp x) in H0.
apply H0. apply ln_exp. lra.
pose proof (exp_pos x). lra. }
apply (Rplus_eq_compat_r (-s)) in H2. field_simplify in H2.
apply H4. rewrite H2. unfold frac_part. field_simplify.
rewrite plus_Int_part2, plus_IZR, Int_part_INR, INR_IZR_INZ.
apply (Rplus_eq_reg_r (-s)). field_simplify.
unfold Int_part. rewrite minus_IZR. field_simplify.
apply IZR_eq. symmetry. apply tech_up. lra. lra.
replace (frac_part (INR x0)) with 0.
destruct (base_fp (-s)). lra.
unfold frac_part. rewrite Int_part_INR, INR_IZR_INZ. lra.
Qed.
Theorem 不用整数也行 : forall f a,
(forall n, 0 <= eval f (INR n) /\ 1 + INR (a n) <=
Rpower 2 (eval f (INR n + 1) - eval f (INR n) - 1)) ->
exists f', 能索引 f' a.
Proof.
intros. destruct (总有非整数 (fun n => eval f (INR n))) as [s].
pose (f' := Add
(Comp 取整 (Add f (Cst (s + 1)))) ((Add Id Id))).
exists f'. apply 不用单调也行. intros.
remember 取整. simpl. subst.
destruct (H0 0 0)%nat as [H1 _]. repeat rewrite 取整取整. split.
- eapply Rle_trans. apply (H n). apply Rle_Rpower. lra.
field_simplify.
pose proof (base_Int_part (eval f (INR n + 1) + (s + 1))).
pose proof (base_Int_part (eval f (INR n) + (s + 1))). lra.
- remember (eval f (INR n) + s) as fns.
destruct (Z_of_nat_complete
(Int_part (eval f (INR n) + (s + 1)))).
replace (eval f (INR n) + (s + 1)) with (fns + 1).
rewrite plus_Int_part2. replace (Int_part 1) with 1%Z.
assert (Int_part fns >= -1)%Z.
{ apply Z.le_ge, le_IZR. destruct (base_Int_part fns).
destruct (H n). lra. }
lia. replace 1 with (INR 1).
rewrite Int_part_INR. auto. auto.
replace (frac_part 1) with 0. pose proof (base_fp fns). lra.
unfold frac_part. replace 1 with (INR 1).
rewrite Int_part_INR. simpl. lra. auto. lra.
exists (x + n + n)%nat.
rewrite H2, plus_INR, plus_INR, <- INR_IZR_INZ. lra.
- destruct (H n). lra.
- intros. destruct (H n).
destruct y. simpl. lra.
destruct (H0 n y). rewrite S_INR. lra.
- destruct (H (S n)). rewrite <- S_INR. lra.
- intros. destruct (H (S n)). rewrite <- S_INR.
destruct y. simpl (INR 0). lra.
destruct (H0 (S n) y). rewrite (S_INR y). lra.
Qed.
Theorem 指数更大 : forall x,
x < Rpower 2 x.
Proof.
assert (forall x, 0 <= x -> 1 <= Rpower 2 x).
{ intros. replace 1 with (Rpower 2 0).
apply Rle_Rpower; lra. apply Rpower_O. lra. }
assert (forall n, INR n + 1 <= Rpower 2 (INR n)).
{ intros. induction n.
- simpl. rewrite Rpower_O; lra.
- rewrite S_INR, Rpower_plus, Rpower_1.
pose proof (H (INR n) (pos_INR _)). lra. lra. }
intros. replace x with (IZR (Int_part x) + frac_part x).
destruct (Z.le_decidable 0 (Int_part x)).
- apply IZN in H1. destruct H1. destruct (base_fp x).
rewrite H1, <- INR_IZR_INZ, Rpower_plus.
pose proof (H _ (Rge_le _ _ H2)). pose proof (H0 x0).
pose proof (H (INR x0) (pos_INR _)). nra.
- apply (Rlt_trans _ 0).
+ apply Z.nle_gt, Ztac.Zlt_le_add_1, IZR_le in H1.
rewrite plus_IZR in H1. destruct (base_fp x). lra.
+ apply exp_pos.
- unfold frac_part. field.
Qed.
Theorem 有能控制的 : forall a',
(forall n, eval a' (INR n) >= 0) ->
(exists f, forall n,
0 <= eval f (INR n) /\ 1 + eval a' (INR n) <=
Rpower 2 (eval f (INR n + 1) - eval f (INR n) - 1)).
Proof.
destruct Req as [Req HReq].
pose (idxof := fix idxof f n x := match n with
| 0 => 0%nat
| S n => if Req (f (S n)) x then S n else idxof f n x
end).
intros. pose (a n := eval a' (INR n)).
pose (b n := idxof a n (Rmax_N a n)).
destruct (能索引则有通项 b) as [b'].
{ assert (forall a n x, idxof a n x <= n)%nat.
{ intros. induction n. auto.
simpl. destruct (Req (a0 (S n)) x); lia. }
apply (不用整数也行 (Add Id (Mul Id Id))).
intros. simpl. split.
- pose proof (pos_INR n). nra.
- apply (Rle_trans _ (Rpower 2 (1 + 2 * INR n))).
2:{ apply Rle_Rpower. lra. field_simplify. lra. }
apply (Rle_trans _ (1 + 2 * INR n)).
assert (INR (b n) <= INR n). { apply le_INR. apply H0. }
pose proof (pos_INR n). lra.
apply Rlt_le, 指数更大. }
assert (forall n, a (b n) = Rmax_N a n).
{ intros. induction n. reflexivity.
unfold b. remember (Rmax_N a (S n)).
simpl. destruct (Req (a (S n)) r) eqn:H1; apply HReq in H1.
auto. simpl in Heqr. unfold Rmax in Heqr.
destruct (Rle_dec (a (S n)) (Rmax_N a n)).
subst. apply IHn. congruence. }
pose (c := Add (Add Id Id) (Mul Id (Comp a' b'))).
exists c. intros. split.
- induction n.
+ simpl. replace (eval b' 0) with (INR (b 0))%nat.
destruct (H (b 0%nat)). lra. lra. apply H0.
+ rewrite S_INR. simpl. rewrite <- S_INR.
specialize (H (b (S n))). rewrite <- H0.
pose proof (pos_INR (S n)). nra.
- assert (1 + eval a' (INR n) <=
eval c (INR n + 1) - eval c (INR n) - 1).
{ simpl. field_simplify. fold (a n).
rewrite <- S_INR, <- H0, <- H0.
fold (a (b n)). fold (a (b (S n))). rewrite H1, H1.
pose proof (max更大 a n 1).
rewrite <- plus_n_Sm, plus_0_r in H2.
pose proof (max大 a n). pose proof (pos_INR n). nra. }
apply (Rle_trans _ (Rpower 2 (1 + eval a' (INR n)))).
apply Rlt_le, 指数更大. apply Rle_Rpower. lra. auto.
Qed.
Theorem 够大就行 : forall a,
(exists f, forall n, INR (a n) <= eval f (INR n)) ->
exists f', 能索引 f' a.
Proof.
intros a [f].
destruct (总有非整数 (fun n => eval f (INR n))) as [s].
pose (f' := Comp 取整 (Add f (Cst (s + 1)))).
assert (forall n, INR (a n) <= eval f' (INR n)).
{ intros. unfold f'. remember 取整. simpl. subst.
destruct (H0 n 0)%nat. specialize (H n).
destruct (base_Int_part (eval f (INR n) + (s + 1))).
pose proof (pos_INR (a n)). rewrite 取整取整. lra. lra.
intros. destruct y. simpl. lra. intro. apply (H0 n y).
rewrite S_INR in H6. field_simplify in H6.
apply Rplus_eq_reg_r in H6. auto. }
destruct (有能控制的 f') as [d].
{ intros. specialize (H1 n). pose proof (pos_INR (a n)). lra. }
apply (不用整数也行 d). intros. split. apply H2.
eapply Rle_trans. apply Rplus_le_compat_l, H1. apply H2.
Qed.
Definition 取小 := Add Id (Comp Opp 取整).
Theorem 取小取小 : forall x,
x > 0 -> (forall y, x <> INR y) ->
eval 取小 x = frac_part x.
Proof.
intros. unfold 取小, frac_part. remember 取整.
simpl. subst. rewrite 取整取整; auto.
Qed.
Theorem 删除一位更小 : forall x,
frac_part (2 * x) / 2 <= frac_part x.
Proof.
intros. unfold frac_part.
apply (Rplus_le_reg_l (-x)), (Rmult_le_reg_r 2),
Ropp_le_cancel. lra. field_simplify.
rewrite <- mult_IZR. apply IZR_le, Zlt_succ_le, lt_IZR.
rewrite mult_IZR, succ_IZR.
destruct (base_Int_part x).
destruct (base_Int_part (2 * x)). lra.
Qed.
Theorem 大的up更大 : forall x y,
x <= y -> (up x <= up y)%Z.
Proof.
intros.
destruct (for_base_fp x).
destruct (for_base_fp y).
apply Zlt_succ_le, lt_IZR.
rewrite succ_IZR. lra.
Qed.
Theorem 都有更大的 : forall a, exists f, forall n,
eval f (INR n) > INR (a n).
Proof.
intros.
pose (b n := (n + 1 + sum_nat_f_O a n)%nat).
assert (forall n m, n >= m -> b n >= b m)%nat as b递增.
{ intros. unfold b. induction H; simpl; lia. }
assert (forall n m, n > m -> b n > b m)%nat as b严格递增.
{ intros. unfold b. induction H; simpl; lia. }
assert (forall n, b n > n)%nat as b大于n.
{ intros. unfold b. lia. }
assert (forall n, b n > a n)%nat as b大于a.
{ intros. unfold b. induction n; simpl; lia. }
pose (c := (fix c n := match n with
| 0 => 1 + b 0
| S n => 1 + b (c n)
end)%nat).
assert (forall n m, n > m -> c n > c m)%nat as c严格递增.
{ intros. induction H; simpl.
- pose proof (b大于n (c m)). lia.
- pose proof (b大于n (c m0)). lia. }
assert (forall n m, n >= m -> c n >= c m)%nat as c递增.
{ intros. induction H; simpl. lia.
pose proof (b大于n (c m0)). lia. }
assert (forall n, c n > n)%nat as c大于n.
{ intros. induction n; simpl. lia.
pose proof (b大于n (c n)). lia. }
assert (forall n, c n > b n)%nat as c大于b.
{ intros. induction n; simpl. lia.
pose proof (b递增 (c n) (S n)). pose proof (c大于n n). lia. }
assert (forall n m, c (n + m) >= n + c m)%nat as c大线性.
{ intros. induction n; simpl. auto.
pose proof (b大于n (c (n + m)%nat)). lia. }
assert (forall n, n >= c 0 -> exists k,
c k <= n < c (S k))%nat as 总有c之间.
{ intros.
assert (exists k, n < c k)%nat.
{ exists n. specialize (c大于n n). lia. }
apply dec_inh_nat_subset_has_unique_least_element in H0.
destruct H0 as [k [[]]]. destruct k. lia.
exists k. split; auto. apply Nat.le_ngt. intro.
specialize (H1 k H3). lia. intros. lia. }
assert (exists C, Un_cv (sum_f_R0 (
fun n => / 2 ^ c n)) C) as [C HC].
{ edestruct Rseries_CV_comp.
2:{ eexists. apply 几何级数. }
2:{ exists x. apply u. }
intros. split.
- rewrite <- Rpower_pow.
apply Rlt_le, Rinv_0_lt_compat, exp_pos. lra.
- repeat rewrite <- Rpower_pow; try lra.
apply Rinv_le_contravar. apply exp_pos.
apply Rle_Rpower. lra. apply le_INR.
pose proof (c大于n n). lia. }
assert (C > 0) as C为正.
{ eapply Rlt_le_trans.
2:{ eapply (sum_incr _ 0). apply HC. intros.
simpl. apply Rlt_le, Rinv_0_lt_compat, pow_lt. lra. }
simpl. apply Rinv_0_lt_compat.
pose proof (pow_lt 2 (a 0)%nat). lra. }
assert (forall n, exists x,
INR x = 2 ^ c n * sum_f_R0 (fun i => / 2 ^ c i) n) as 整数部分.
{ intros. erewrite scal_sum, sum_eq.
2:{ intros. rewrite <- Rpower_pow, <- Rpower_pow,
<- Rpower_Ropp, <- Rpower_plus.
replace (- INR (c i) + INR (c n)) with (INR (c n - c i)).
rewrite Rpower_pow. reflexivity. lra.
rewrite minus_INR. lra. pose proof (c递增 n i). lia.
lra. lra. }
induction n.
- exists 1%nat. simpl. rewrite Nat.sub_diag, pow_O. lra.
- destruct IHn. exists (2 ^ (c (S n) - c n) * x + 1)%nat.
remember c as c'. simpl. rewrite Nat.sub_diag, pow_O.
rewrite plus_INR, mult_INR, H, scal_sum.
f_equal. apply sum_eq. intros.
rewrite pow_INR, <- pow_add. f_equal. subst.
assert (c (S n) > c n)%nat. { apply c严格递增. lia. }
apply c递增 in H0. lia. }
assert (forall n l, Un_cv (sum_f_R0 (fun i =>
/ 2 ^ (c (n + S i))%nat)) l -> 0 < l < / 2 ^ c n) as 小数部分.
{ intros. split.
- eapply Rlt_le_trans.
2:{ eapply (sum_incr _ 0). apply H. intros.
simpl. apply Rlt_le, Rinv_0_lt_compat, pow_lt. lra. }
simpl. apply Rinv_0_lt_compat, pow_lt. lra.
- assert (2 ^ c n > 0). { apply pow_lt. lra. }
eapply Rle_lt_trans. eapply Rle_cv_lim.
2:apply H. 2:{ apply CV_mult, 几何级数.
apply (常数收敛 (/ 2 ^ (S (c n)))). }
intros. simpl. rewrite scal_sum. apply sum_Rle.
intros. assert (2 ^ n1 > 0). { apply pow_lt. lra. }
rewrite <- Rinv_mult_distr. apply Rinv_le_contravar. nra.
apply (Rle_trans _ (2 ^ (S (S (n1 + c n))))).
simpl. rewrite pow_add. lra.
apply Rle_pow. lra.
replace (n + S n1)%nat with (n1 + S n)%nat.
eapply le_trans. 2:apply c大线性. simpl.
pose proof (b大于n (c n)). lia. lia. lra. lra.
assert (/ 2 ^ c n > 0). { apply Rinv_0_lt_compat, H0. }
simpl. rewrite Rinv_mult_distr. lra. lra. lra. }
assert (forall n, Un_cv (sum_f_R0 (
fun i => / 2 ^ c (n + S i)%nat))
(frac_part (C * 2 ^ c n) / 2 ^ c n)) as C取小.
{ intros. destruct (整数部分 n).
apply (CV_shift' _ (S n)) in HC.
apply (f_equal (fun x => x / 2 ^ c n)) in H.
field_simplify in H; try (pose proof (pow_lt 2 (c n)); lra).
eapply CV_plus in HC. 2:apply (常数收敛 (-(INR x / 2^c n))).
apply (Un_cv_ext _ (sum_f_R0 (fun i =>
/ 2 ^ c (n + S i)%nat))) in HC.
2:{ intros. rewrite H, (tech2 _ n (n0 + S n)).
field_simplify. replace (n0 + S n - S n)%nat with n0.
apply sum_eq. intros. f_equal. f_equal. f_equal.
lia. lia. lia. }
replace (frac_part (C * 2 ^ c n) / 2 ^ c n)
with (- (INR x / 2 ^ c n) + C). auto.
destruct (小数部分 _ _ HC). pose proof (pow_lt 2 (c n)).
apply (Rmult_lt_compat_r (2 ^ c n)) in H0, H1; try lra.
field_simplify in H0; try lra. field_simplify in H1; try lra.
pose proof (pow_lt 2 (c n)). unfold frac_part.
apply (Rplus_eq_reg_r (-C)). field_simplify; try lra.
f_equal. f_equal. unfold Int_part.
rewrite <- (up_tech _ (Z.of_nat x)), INR_IZR_INZ.
- f_equal. lia.
- rewrite <- INR_IZR_INZ. lra.
- rewrite plus_IZR, <- INR_IZR_INZ. lra. }
assert (forall n x, INR x <> C * 2 ^ c n) as Cc非整数.
{ intros. pose (ofs := -sum_f_R0 (fun i => / 2 ^ c i) n).
destruct (小数部分 n (C + ofs)).
{ eapply (CV_shift' _ (S n)), CV_plus, (Un_cv_ext _
(sum_f_R0 (fun i => / 2 ^ c (n + S i)%nat))) in HC.
3:apply (常数收敛 ofs).
2:{ intros. unfold ofs.
rewrite (tech2 _ n (n0 + S n))%nat. field_simplify.
replace (n0 + S n - S n)%nat with n0.
apply sum_eq. intros. f_equal. f_equal. f_equal.
lia. lia. lia. }
rewrite Rplus_comm in HC. apply HC. }
assert (exists y, INR y = -ofs * 2 ^ c n).
{ unfold ofs. clear H H0 ofs. induction n.
- exists 1%nat. simpl. field.
apply Rgt_not_eq, pow_lt. lra.
- destruct IHn. exists (x0 * 2 ^ (c (S n) - c n) + 1)%nat.
rewrite plus_INR, mult_INR, H, pow_INR.
replace (INR 2 ^ (c (S n) - c n))
with (INR 2 ^ c (S n) / 2 ^ c n).
remember c as c'. simpl. field_simplify. auto.
apply Rgt_not_eq, pow_lt. lra.
apply Rgt_not_eq, pow_lt. lra.
repeat rewrite <- Rpower_pow; try (simpl; lra).
rewrite minus_INR. unfold "_ - _", "_ / _".
rewrite Rpower_plus, Rpower_Ropp. auto.
apply c递增. lia. }
assert (2 ^ c n > 0). { apply pow_lt. lra. }
destruct H1. intro. replace (C + ofs) with
(IZR (Z.of_nat x - Z.of_nat x0)%Z / 2 ^ c n) in H, H0.
apply (Rmult_lt_compat_r (2 ^ c n)) in H, H0.
field_simplify in H. field_simplify in H0.
apply lt_IZR in H, H0. lia.
lra. lra. lra. lra. lra.
rewrite minus_IZR, <- INR_IZR_INZ, <- INR_IZR_INZ, H1, H3.
field. lra. }
assert (forall n x, INR x <> C * 2 ^ n) as C非整数.
{ intros. intro. apply (Cc非整数 n (x * 2 ^ (c n - n))%nat).
rewrite mult_INR, pow_INR, H.
replace (INR 2 ^ (c n - n)) with (2 ^ c n / 2 ^ n).
field. apply Rgt_not_eq, pow_lt. lra.
repeat rewrite <- Rpower_pow. rewrite minus_INR.
unfold "_ - _". rewrite Rpower_plus, Rpower_Ropp. auto.
pose proof (c大于n n). lia. simpl. lra. lra. lra. }
assert (forall m, C * 2 ^ m > 0) as C乘为正.
{ intros. pose proof (pow_lt 2 m). nra. }
assert (forall m, frac_part (C * 2 ^ m) <> 0) as C乘小数非0.
{ intros. intro. apply fp_nat in H. destruct H.
specialize (C乘为正 m).
rewrite H in C乘为正. apply lt_IZR in C乘为正.
destruct (IZN x). lia. subst.
eapply C非整数. rewrite INR_IZR_INZ. eauto. }
assert (forall m, frac_part (C * 2 ^ m) > 0) as C乘小数为正.
{ intros. destruct (base_fp (C * 2 ^ m)).
specialize (C乘小数非0 m). lra. }
(* 2^(n + 1) / 取小(2^n * C) *)
pose (d := Mul (Mul (Cst 2) pow2)
(Comp Inv (Comp 取小 (Mul (Comp pow2 Id) (Cst C))))).
assert (forall n,
eval d (INR (c n)) > INR (c (S n))) as dc大于cS.
{ intros. unfold d. remember 取小. remember pow2.
remember c as c'. simpl. subst.
rewrite pow2Rpower, 取小取小, Rpower_pow.
2:lra. 2:apply Rmult_gt_0_compat; auto; apply exp_pos.
rewrite (Rmult_comm _ C). remember (C * 2 ^ c n).
assert (2 ^ c n > 0) as 指数为正. { apply pow_lt. lra. }
assert (2 ^ c (S n) > 0) as S指数为正. { apply pow_lt. lra. }
assert (r > 0) as r为正. { subst. apply C乘为正. }
assert (frac_part r > 0) as r小数为正.
{ subst. apply C乘小数为正. }
apply (Rge_gt_trans _ (2 * 2 ^ (c n) / frac_part r)).
{ apply Rmult_le_compat_r.
apply Rlt_le, Rinv_0_lt_compat. lra. lra. }
apply (Rge_gt_trans _ (2 ^ (c (S n)))).
{ remember c as c'. rewrite <- Rinv_involutive.
replace (2 * 2 ^ (c' n) / frac_part r)
with (/ (/2 * (frac_part r / 2 ^ c' n))).
apply Rle_ge, Rinv_le_contravar.
{ apply Rinv_0_lt_compat in 指数为正. nra. }
eapply Rle_cv_lim.
2:{ apply CV_mult. apply 常数收敛. subst. apply C取小. }
2:{ rewrite <- Rmult_1_l. eapply CV_mult.
apply 几何级数. apply 常数收敛. }
intros. simpl. rewrite scal_sum, Rmult_comm, scal_sum.
apply sum_Rle. intros.
assert (2 ^ n1 * 2 ^ c' (S n) <= 2 ^ c' (n + S n1)%nat).
{ rewrite <- pow_add. apply Rle_pow. lra.
replace (n + S n1)%nat with (n1 + S n)%nat. 2:lia.
apply c大线性. }
assert (2 ^ n1 > 0). { apply pow_lt. lra. }
repeat rewrite <- Rinv_mult_distr; try lra.
apply Rinv_le_contravar. nra. lra.
apply Rgt_not_eq, pow_lt. lra. field. split; lra. lra. }
rewrite <- Rpower_pow. apply 指数更大. lra.
intros. rewrite Rpower_pow. rewrite Rmult_comm.
intro. eapply Cc非整数. eauto. lra. }
assert (forall n,
eval d (INR n) <= eval d (INR n + 1)) as d单调.
{ intros. unfold d. remember 取小. remember pow2. simpl.
subst. repeat rewrite pow2Rpower, 取小取小.
repeat rewrite <- S_INR. repeat rewrite Rpower_pow.
rewrite (Rmult_comm _ C), (Rmult_comm _ C),
<- (Rinv_involutive ((2 * 2 ^ n) * _)),
<- (Rinv_involutive ((2 * 2 ^ S n) * _)).
apply Rinv_le_contravar.
{ apply Rinv_0_lt_compat. specialize (C乘小数为正 (S n)).
apply Rinv_0_lt_compat in C乘小数为正.
pose proof (pow_lt 2 (S n)). nra. }
field_simplify; try (split;
[apply C乘小数非0 | apply Rgt_not_eq, pow_lt; lra]).
simpl. apply (Rmult_le_reg_r (2 * 2 ^ n)).
{ pose proof (pow_lt 2 n). lra. }
field_simplify; try (apply Rgt_not_eq, pow_lt; lra).
replace (C * (2 * 2 ^ n)) with (2 * (C * 2 ^ n)).
apply 删除一位更小. lra.
specialize (C乘小数为正 (S n)). pose proof (pow_lt 2 (S n)).
apply Rinv_0_lt_compat in C乘小数为正. nra.
specialize (C乘小数为正 n). pose proof (pow_lt 2 n).
apply Rinv_0_lt_compat in C乘小数为正. nra.
lra. lra.
apply Rmult_gt_0_compat. apply exp_pos. auto.
intros. rewrite <- S_INR, Rpower_pow.
pose proof (C非整数 (S n) y). lra. lra.
apply Rmult_gt_0_compat. apply exp_pos. auto.
intros. rewrite Rpower_pow.
pose proof (C非整数 n y). lra. lra. }
assert (forall n, 0 < eval d (INR n)) as d为正.
{ intros. unfold d. remember 取小. remember pow2. simpl.
subst. repeat rewrite pow2Rpower, 取小取小.
apply Rmult_gt_0_compat.
apply Rmult_gt_0_compat. lra. apply exp_pos.
apply Rinv_0_lt_compat. rewrite Rpower_pow, Rmult_comm.
apply C乘小数为正. lra.
rewrite Rpower_pow, Rmult_comm. apply C乘为正. lra.
intros. rewrite Rpower_pow, Rmult_comm.
specialize (C非整数 n y). lra. lra. }
pose (e n :=
(1 + (n + 1) * Z.to_nat (up (eval d (INR n))))%nat).
destruct (能索引则有通项 e) as [e' He'].
{ apply 够大就行. exists (Add (Cst 1)
(Mul (Add Id (Cst 1)) (Add d (Cst 1)))).
intros. remember d as d'. unfold e.
rewrite plus_INR, mult_INR, plus_INR. simpl.
apply Rplus_le_compat_l, Rmult_le_compat_l.
{ pose proof (pos_INR n). lra. }
destruct (for_base_fp (eval d' (INR n))).
rewrite INR_IZR_INZ, Z2Nat.id. lra.
apply le_IZR. specialize (d为正 n). lra. }
assert (forall n, e (S n) > e n)%nat as e严格递增S.
{ intros. unfold e. apply plus_lt_compat_l.
remember (eval d) as d'. rewrite S_INR. simpl.
assert (up (d' (INR n)) <= up (d' (INR n + 1)%R))%Z.
{ apply 大的up更大. apply d单调. }
assert (0 < up (d' (INR n + 1)%R))%Z.
{ rewrite <- S_INR. apply lt_IZR.
destruct (for_base_fp (d' (INR (S n)))).
specialize (d为正 (S n)). lra. }
rewrite <- Z2Nat.id, <- (Z2Nat.id (up (_ (INR n)))) in H.
apply Z2Nat.inj_lt in H0. simpl in H0. nia.
lia. lia. 2:lia.
apply le_IZR. destruct (for_base_fp (d' (INR n))).
specialize (d为正 n). lra. }
assert (forall n m, n < m -> e n < e m)%nat as e严格递增.
{ intros. induction H. apply e严格递增S.
pose proof (e严格递增S m). lia. }
assert (forall n m, n <= m -> e n <= e m)%nat as e递增.
{ intros. apply le_lt_or_eq in H. destruct H.
apply e严格递增 in H. lia. subst. auto. }
assert (forall n,
eval e' (INR n) > eval d (INR n)) as e大于d.
{ intros. rewrite <- He'. unfold e.
apply (Rgt_ge_trans _
(INR (Z.to_nat (up (eval d (INR n)))))).
apply lt_INR. lia.
rewrite INR_IZR_INZ, Z2Nat.id.
destruct (for_base_fp (eval d (INR n))). lra.
apply le_IZR. destruct (for_base_fp (eval d (INR n))).
specialize (d为正 n). lra. }
assert (forall n, e (c n) > c (S n))%nat as ec大于cS.
{ intros. eapply INR_lt, Rgt_trans.
rewrite He'. apply e大于d. apply dc大于cS. }
pose (f := Comp e' e').
assert (forall n,
eval f (INR (c n)) > INR (b (c (S n)))) as fc大于bcS.
{ intros. remember c as c'. simpl. repeat rewrite <- He'.
apply lt_INR, (lt_trans _ (e (c' (S n)))).
- eapply gt_trans. apply ec大于cS. subst. simpl. lia.
- apply e严格递增. apply ec大于cS. }
assert (forall n m, (n >= m)%nat ->
eval f (INR n) >= eval f (INR m)) as f递增.
{ intros. remember c as c'. simpl. repeat rewrite <- He'.
apply Rle_ge, le_INR, e递增, e递增. auto. }
assert (forall n, 0 < eval f (INR n)) as f为正.
{ intros. simpl. rewrite <- He'.
eapply Rgt_trans. apply e大于d. apply d为正. }
assert (forall n, (n >= c 0)%nat ->
eval f (INR n) > INR (a n)) as f大于a.
{ intros. apply 总有c之间 in H. destruct H as [k []].
apply (Rge_gt_trans _ (eval f (INR (c k)))).
{ apply f递增. auto. }
eapply Rgt_trans. apply fc大于bcS.
apply lt_INR, (lt_trans _ (b n)).
apply b大于a. apply b严格递增. auto. }
assert (forall n,
n < c 0 -> a n < b (c 0))%nat as a小于bc0.
{ intros. eapply lt_trans. apply b大于a.
apply b严格递增. auto. }
exists (Add f (Cst (INR (b (c 0%nat))))).
intros. remember f as f'. remember c as c'. simpl.
destruct (le_lt_dec (c 0%nat) n).
- subst. eapply Rlt_le_trans. apply f大于a. auto.
pose proof (pos_INR (b (c 0%nat))). lra.
- subst. specialize (f为正 n). specialize (a小于bc0 n l).
apply lt_INR in a小于bc0. lra.
Qed.
Theorem 自然数数列都有初等通项 : forall a, exists f, forall n,
INR (a n) = eval f (INR n).
Proof.
intros. apply 能索引则有通项, 够大就行.
destruct (都有更大的 a) as [f].
exists f. intros. apply Rlt_le, H.
Qed.
Theorem 整数数列都有初等通项 : forall a, exists f, forall n,
IZR (a n) = eval f (INR n).
Proof.
intros.
destruct (自然数数列都有初等通项
(fun n => Z.abs_nat (a n))) as [f_abs].
destruct (自然数数列都有初等通项
(fun n => Z.to_nat (Z.sgn (a n) + 1)%Z)) as [f_sgn].
exists (Mul f_abs (Add f_sgn (Cst (-1)))).
intros. simpl. rewrite <- H, <- H0,
INR_IZR_INZ, INR_IZR_INZ, <- plus_IZR, <- mult_IZR,
Zabs2Nat.id_abs, Z2Nat.id.
replace (Z.sgn (a n) + 1 + -1)%Z with (Z.sgn (a n)).
rewrite Z.abs_sgn. auto.
lia. destruct (a n); lia.
Qed.
Theorem 有理数数列都有初等通项 : forall a, exists f, forall n,
Q2R (a n) = eval f (INR n).
Proof.
intros.
destruct (整数数列都有初等通项
(fun n => Qnum (a n))) as [f_num].
destruct (整数数列都有初等通项
(fun n => QDen (a n))) as [f_den].
exists (Mul f_num (Comp Inv f_den)).
intros. simpl. rewrite <- H, <- H0.
unfold Q2R. auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment