]
qed.
-theorem le_B_exp: \forall n.S O < n \to
+theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
intros.
apply (le_times_to_le (exp (fact n) (S(S O))))
]
qed.
-theorem le_A_SSO_A: \forall n.
-A((S(S O))*n) \le
- pi_p (S ((S(S O))*n)) primeb (λp:nat.p)*A n.
-unfold A.intros.
-cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
+theorem le_B_exp: \forall n.
+B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+intro.cases n
+ [apply le_n
+ |cases n1
+ [simplify.apply le_S.apply le_S.apply le_n
+ |apply lt_SO_to_le_B_exp.
+ apply le_S_S.apply lt_O_S.
+ ]
+ ]
+qed.
+
+theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
+exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+intros.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+ [apply lt_O_exp.
+ apply lt_O_fact
+ |rewrite < assoc_times in ⊢ (? ? %).
+ rewrite > sym_times in ⊢ (? ? (? % ?)).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite < eq_fact_B
+ [rewrite < sym_times.
+ apply fact3.
+ apply lt_to_le.assumption
+ |assumption
+ ]
+ ]
+qed.
+
+theorem le_exp_B: \forall n. O < n \to
+exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+intros.
+elim H
+ [apply le_n
+ |apply lt_SO_to_le_exp_B.
+ apply le_S_S.assumption
+ ]
+qed.
+
+theorem eq_A_SSO_n: \forall n.O < n \to
+A((S(S O))*n) =
+ pi_p (S ((S(S O))*n)) primeb
+ (\lambda p.(pi_p (log p ((S(S O))*n) )
+ (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
+ *A n.
+intro.
+rewrite > eq_A_A'.rewrite > eq_A_A'.
+unfold A'.intros.
+cut (
+ pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
+ = pi_p (S ((S(S O))*n)) primeb
+ (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))
[rewrite > Hcut.
rewrite < times_pi_p.
- apply le_pi_p.intros.
- lapply (prime_to_lt_SO ? (primeb_true_to_prime ? H1)) as H2.
- change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
- apply le_exp
- [apply lt_to_le.assumption
- |apply (trans_le ? (log i (i*n)))
- [apply le_log
- [assumption
- |apply not_le_to_lt.intro.
- apply (lt_to_not_le ? ? H).
- apply (trans_le ? (S O))
- [apply le_S_S.assumption
- |apply lt_to_le.assumption
- ]
- |apply le_times_l.
- assumption
+ apply eq_pi_p1;intros
+ [reflexivity
+ |rewrite < times_pi_p.
+ apply eq_pi_p;intros
+ [reflexivity
+ |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
+ [simplify.rewrite < times_n_SO.apply times_n_SO
+ |simplify.rewrite < plus_n_O.apply times_n_SO
]
- |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
- rewrite > log_exp
- [apply le_n
- |assumption
- |apply not_le_to_lt.intro.
- apply (lt_to_not_le ? ? H).
- apply (le_n_O_elim ? H3).
- apply lt_to_le.
- assumption
- ]
]
]
- |apply sym_eq.
- apply or_false_eq_SO_to_eq_pi_p
- [apply le_S_S.
- apply le_times_n.
- apply lt_O_S
- |intros.right.
- change with (exp i (log i n) = (exp i O)).
- apply eq_f.
- apply antisymmetric_le
- [cut (O < n)
- [apply le_S_S_to_le.
- apply (lt_exp_to_lt i)
- [apply (le_to_lt_to_lt ? n);assumption
- |apply (le_to_lt_to_lt ? n)
- [apply le_exp_log.
+ |apply (trans_eq ? ? (pi_p (S n) primeb
+ (\lambda p:nat.pi_p (log p n) (\lambda i:nat.true) (\lambda i:nat.(p)\sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
+ [apply eq_pi_p1;intros
+ [reflexivity
+ |apply eq_pi_p1;intros
+ [reflexivity
+ |rewrite > lt_to_leb_false
+ [simplify.apply times_n_SO
+ |apply le_S_S.
+ apply (trans_le ? (exp x (log x n)))
+ [apply le_exp
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ assumption
+ |assumption
+ ]
+ |apply le_exp_log.
assumption
- |rewrite < exp_n_SO.
+ ]
+ ]
+ ]
+ ]
+ |apply (trans_eq ? ?
+ (pi_p (S ((S(S O))*n)) primeb
+ (λp:nat.pi_p (log p n) (λi:nat.true)
+ (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
+ [apply sym_eq.
+ apply or_false_eq_SO_to_eq_pi_p
+ [apply le_S_S.
+ simplify.
+ apply le_plus_n_r
+ |intros.right.
+ rewrite > lt_to_log_O
+ [reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |apply eq_pi_p1;intros
+ [reflexivity
+ |apply sym_eq.
+ apply or_false_eq_SO_to_eq_pi_p
+ [apply le_log
+ [apply prime_to_lt_SO.
+ apply primeb_true_to_prime.
assumption
+ |assumption
+ |simplify.
+ apply le_plus_n_r
+ ]
+ |intros.right.
+ rewrite > le_to_leb_true
+ [simplify.reflexivity
+ |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
+ [apply lt_exp_log.
+ apply prime_to_lt_SO.
+ apply primeb_true_to_prime.
+ assumption
+ |apply le_exp
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ assumption
+ |apply le_S_S.assumption
+ ]
+ ]
]
]
- |apply not_le_to_lt.intro.
- apply (lt_to_not_le ? ? H1).
- generalize in match H.
- apply (le_n_O_elim ? H2).
- intro.assumption
]
- |apply le_O_n
]
]
]
qed.
-
-(* so far so good
-
-theorem le_A_BA: \forall n.
+
+theorem le_A_BA1: \forall n. O < n \to
A((S(S O))*n) \le B((S(S O))*n)*A n.
-(*
- [simplify.reflexivity
- |rewrite > times_SSO.
- rewrite > times_SSO.
- unfold A.
-apply (trans_le ? ((pi_p (S ((S(S O))*n)) primeb (λp:nat.p))*A n))
- [apply le_A_SSO_A
- |apply le_times_l.
+intros.
+rewrite > eq_A_SSO_n
+ [apply le_times_l.
unfold B.
apply le_pi_p.intros.
-*)
-intro.unfold A.unfold B.
-cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
- [rewrite > Hcut.
- rewrite < times_pi_p.
apply le_pi_p.intros.
- apply le_trans i.
-
-
- change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
apply le_exp
[apply prime_to_lt_O.
apply primeb_true_to_prime.
assumption
- |apply (trans_le ? (log i (i*n)))
- [apply le_log
- [apply prime_to_lt_SO.
- apply primeb_true_to_prime.
- assumption
- |apply not_le_to_lt.intro.
- apply (lt_to_not_le ? ? H).
- apply (trans_le ? (S O))
- [apply le_S_S.assumption
- |apply prime_to_lt_O.
+ |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
+ [simplify in ⊢ (? % ?).
+ cut ((S(S O))*n/i\sup(S i1) = S O)
+ [rewrite > Hcut.apply le_n
+ |apply (div_mod_spec_to_eq
+ ((S(S O))*n) (exp i (S i1))
+ ? (mod ((S(S O))*n) (exp i (S i1)))
+ ? (minus ((S(S O))*n) (exp i (S i1))) )
+ [apply div_mod_spec_div_mod.
+ apply lt_O_exp.
+ apply prime_to_lt_O.
apply primeb_true_to_prime.
- assumption
- ]
- |apply le_times_l.
- apply prime_to_lt_SO.
- apply primeb_true_to_prime.
- assumption
+ assumption
+ |cut (i\sup(S i1)≤(S(S O))*n)
+ [apply div_mod_spec_intro
+ [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
+ apply lt_plus_to_lt_minus
+ [assumption
+ |simplify in ⊢ (? % ?).
+ rewrite < plus_n_O.
+ apply lt_plus
+ [apply leb_true_to_le.assumption
+ |apply leb_true_to_le.assumption
+ ]
+ ]
+ |rewrite > sym_plus.
+ rewrite > sym_times in ⊢ (? ? ? (? ? %)).
+ rewrite < times_n_SO.
+ apply plus_minus_m_m.
+ assumption
+ ]
+ |apply (trans_le ? (exp i (log i ((S(S O))*n))))
+ [apply le_exp
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ assumption
+ |assumption
+ ]
+ |apply le_exp_log.
+ rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ ]
+ ]
+ ]
]
- |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
- rewrite > log_exp
- [apply le_n
- |apply prime_to_lt_SO.
- apply primeb_true_to_prime.
+ |apply le_O_n
+ ]
+ ]
+ |assumption
+ ]
+qed.
+
+theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
+intros.cases n
+ [apply le_n
+ |apply le_A_BA1.apply lt_O_S
+ ]
+qed.
+
+theorem le_A_exp: \forall n.
+A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
+intro.
+apply (trans_le ? (B((S(S O))*n)*A n))
+ [apply le_A_BA
+ |apply le_times_l.
+ apply le_B_exp
+ ]
+qed.
+
+theorem le_A_exp1: \forall n.
+A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
+intro.elim n
+ [simplify.apply le_S_S.apply le_O_n
+ |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
+ apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
+ [apply le_A_exp
+ |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
+ [apply le_times_r.
+ assumption
+ |rewrite < exp_plus_times.
+ simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
+ apply le_n
+ ]
+ ]
+ ]
+qed.
+
+theorem monotonic_A: monotonic nat le A.
+unfold.intros.
+elim H
+ [apply le_n
+ |apply (trans_le ? (A n1))
+ [assumption
+ |unfold A.
+ cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
+ ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
+ [apply (bool_elim ? (primeb (S n1)));intro
+ [rewrite > (true_to_pi_p_Sn ? ? ? H3).
+ rewrite > times_n_SO in ⊢ (? % ?).
+ rewrite > sym_times.
+ apply le_times
+ [apply lt_O_exp.apply lt_O_S
+ |assumption
+ ]
+ |rewrite > (false_to_pi_p_Sn ? ? ? H3).
assumption
- |apply not_le_to_lt.intro.
- apply (lt_to_not_le ? ? H).
- apply (le_n_O_elim ? H2).
- apply prime_to_lt_O.
+ ]
+ |apply le_pi_p.intros.
+ apply le_exp
+ [apply prime_to_lt_O.
apply primeb_true_to_prime.
assumption
- ]
- ]
- ]
- |apply sym_eq.
- apply or_false_eq_SO_to_eq_pi_p
- [apply le_S_S.
- apply le_times_n.
- apply lt_O_S
- |intros.right.
- change with (exp i (log i n) = (exp i O)).
- apply eq_f.
- apply antisymmetric_le
- [cut (O < n)
- [apply le_S_S_to_le.
- apply (lt_exp_to_lt i)
- [apply (le_to_lt_to_lt ? n);assumption
- |apply (le_to_lt_to_lt ? n)
- [apply le_exp_log.
+ |apply le_log
+ [apply prime_to_lt_SO.
+ apply primeb_true_to_prime.
+ assumption
+ |apply (lt_to_le_to_lt ? i)
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
assumption
- |rewrite < exp_n_SO.
+ |apply le_S_S_to_le.
assumption
]
+ |apply le_S.apply le_n
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem le_A_exp2: \forall n. O < n \to
+A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
+intros.
+apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
+ [apply monotonic_A.
+ apply lt_to_le.
+ apply lt_exp_log.
+ apply le_n
+ |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
+ [apply le_A_exp1
+ |apply le_exp
+ [apply lt_O_S
+ |rewrite > assoc_times.apply le_times_r.
+ change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
+ apply le_times_r.
+ apply le_exp_log.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+(* example *)
+theorem A_SO: A (S O) = S O.
+reflexivity.
+qed.
+
+theorem A_SSO: A (S(S O)) = S (S O).
+reflexivity.
+qed.
+
+theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
+reflexivity.
+qed.
+
+theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+reflexivity.
+qed.
+
+(* da spostare *)
+theorem or_eq_eq_S: \forall n.\exists m.
+n = (S(S O))*m \lor n = S ((S(S O))*m).
+intro.elim n
+ [apply (ex_intro ? ? O).
+ left.reflexivity
+ |elim H.elim H1
+ [apply (ex_intro ? ? a).
+ right.apply eq_f.assumption
+ |apply (ex_intro ? ? (S a)).
+ left.rewrite > H2.
+ apply sym_eq.
+ apply times_SSO
+ ]
+ ]
+qed.
+
+(* a better result *)
+theorem le_A_exp3: \forall n. S O < n \to
+A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
+intro.
+apply (nat_elim1 n).
+intros.
+elim (or_eq_eq_S m).
+elim H2
+ [elim (le_to_or_lt_eq (S O) a)
+ [rewrite > H3 in ⊢ (? % ?).
+ apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
+ [apply le_A_exp
+ |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
+ ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
+ [apply le_times_r.
+ apply H
+ [rewrite > H3.
+ rewrite > times_n_SO in ⊢ (? % ?).
+ rewrite > sym_times.
+ apply lt_times_l1
+ [apply lt_to_le.assumption
+ |apply le_n
+ ]
+ |assumption
+ ]
+ |rewrite > sym_times.
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ apply (trans_le ?
+ (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+ [rewrite > assoc_times.
+ apply le_times_r.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite < H3.
+ simplify.
+ rewrite < plus_n_O.
+ apply le_S.apply le_S.
+ apply le_n
+ ]
+ |apply le_times_l.
+ rewrite > times_exp.
+ apply monotonic_exp1.
+ rewrite > H3.
+ rewrite > sym_times.
+ cases a
+ [apply le_n
+ |simplify.
+ rewrite < plus_n_Sm.
+ apply le_S.
+ apply le_n
+ ]
]
- |apply not_le_to_lt.intro.
- apply (lt_to_not_le ? ? H1).
- generalize in match H.
- apply (le_n_O_elim ? H2).
- intro.assumption
]
+ ]
+ |rewrite < H4 in H3.
+ simplify in H3.
+ rewrite > H3.
+ simplify.
+ apply le_S_S.apply le_S_S.apply le_O_n
+ |apply not_lt_to_le.intro.
+ apply (lt_to_not_le ? ? H1).
+ rewrite > H3.
+ apply (le_n_O_elim a)
+ [apply le_S_S_to_le.assumption
|apply le_O_n
]
]
+ |elim (le_to_or_lt_eq O a (le_O_n ?))
+ [apply (trans_le ? (A ((S(S O))*(S a))))
+ [apply monotonic_A.
+ rewrite > H3.
+ rewrite > times_SSO.
+ apply le_n_Sn
+ |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
+ [apply le_A_exp
+ |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
+ (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
+ [apply le_times_r.
+ apply H
+ [rewrite > H3.
+ apply le_S_S.
+ simplify.
+ rewrite > plus_n_SO.
+ apply le_plus_r.
+ rewrite < plus_n_O.
+ assumption
+ |apply le_S_S.assumption
+ ]
+ |rewrite > sym_times.
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ apply (trans_le ?
+ (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+ [rewrite > assoc_times.
+ apply le_times_r.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite > times_SSO.
+ rewrite < H3.
+ simplify.
+ rewrite < plus_n_Sm.
+ rewrite < plus_n_O.
+ apply le_n
+ ]
+ |apply le_times_l.
+ rewrite > times_exp.
+ apply monotonic_exp1.
+ rewrite > H3.
+ rewrite > sym_times.
+ apply le_n
+ ]
+ ]
+ ]
+ ]
+ |rewrite < H4 in H3.simplify in H3.
+ apply False_ind.
+ apply (lt_to_not_le ? ? H1).
+ rewrite > H3.
+ apply le_n
+ ]
]
qed.
+theorem eq_sigma_pi_SO_n: \forall n.
+sigma_p n (\lambda i.true) (\lambda i.S O) = n.
+intro.elim n
+ [reflexivity
+ |rewrite > true_to_sigma_p_Sn
+ [rewrite > H.reflexivity
+ |reflexivity
+ ]
+ ]
+qed.
+
+theorem leA_prim: \forall n.
+exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
+intro.
+unfold prim.
+rewrite < (exp_sigma_p (S n) n primeb).
+unfold A.
+rewrite < times_pi_p.
+apply le_pi_p.
+intros.
+rewrite > sym_times.
+change in ⊢ (? ? %) with (exp i (S (log i n))).
+apply lt_to_le.
+apply lt_exp_log.
+apply prime_to_lt_SO.
+apply primeb_true_to_prime.
+assumption.
+qed.
+
+
+(* the inequalities *)
+theorem le_exp_priml: \forall n. O < n \to
+exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
+intros.
+apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
+ [apply le_exp_B.assumption
+ |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
+ apply le_times_r.
+ apply (trans_le ? (A ((S(S O))*n)))
+ [apply le_B_A
+ |apply le_Al
+ ]
+ ]
+qed.
+
+theorem le_priml: \forall n. O < n \to
+(S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
+intros.
+rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
+ [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
+ [apply le_log
+ [apply le_n
+ |apply lt_O_exp.apply lt_O_S
+ |apply le_exp_priml.assumption
+ ]
+ |rewrite > sym_times in ⊢ (? ? %).
+ apply log_exp1.
+ apply le_n
+ ]
+ |apply le_n
+ ]
+qed.
+
+theorem le_exp_primr: \forall n. S O < n \to
+exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
+intros.
+apply (trans_le ? (exp (A n) (S(S O))))
+ [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
+ rewrite < times_n_SO.
+ apply leA_r2
+ |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
+ [apply monotonic_exp1.
+ apply le_A_exp3.
+ assumption
+ |rewrite < times_exp.
+ rewrite > exp_exp_times.
+ rewrite > exp_exp_times.
+ rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
+ rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+ apply le_n
+ ]
+ ]
+qed.
-unfold A.unfold B.
-rewrite > eq_A_A'.rewrite > eq_A_A'.
-unfold A'.unfold B.
(* da spostare *)
theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
a*log a-a+k*log a
+*)
\ No newline at end of file
projects / helm.git / blobdiff