Library hydras.solutions_exercises.F_3
From Coq Require Import Arith.
From hydras Require Import Iterates F_alpha E0.
From Coq Require Import ArithRing Lia Max.
Import Exp2.
From hydras Require Import Compat815.
Open Scope nat_scope.
Lemma LF3 : dominates_from 2 (F_ 3) (fun n ⇒ iterate exp2 n n).
From hydras Require Import Iterates F_alpha E0.
From Coq Require Import ArithRing Lia Max.
Import Exp2.
From hydras Require Import Compat815.
Open Scope nat_scope.
Lemma LF3 : dominates_from 2 (F_ 3) (fun n ⇒ iterate exp2 n n).
Section S1.
Let P alpha := ∀ n, 2 ≤ n → exp2 (F_ alpha n) ≤ F_ alpha (S n).
Remark F_3_eqn : ∀ n, F_ 3 n = iterate (F_ 2) (S n) n.
deprecated, not replaced yet
Successor case
Section Successor.
Variable alpha: E0.
Hypothesis H_alpha : P alpha.
Remark R1: ∀ n, 2 ≤ n →
∀ p, n < p →
exp2 (F_ alpha n) ≤ F_ alpha p.
Section S2.
Variable n : nat.
Hypothesis Hn : 2 ≤ n.
Remark R3 :
F_ (E0_succ alpha) (S n)= F_ alpha (iterate (F_ alpha) (S n) (S n)).
Remark R3' : F_ (E0_succ alpha) n = iterate (F_ alpha) (S n) n.
Remark R4 : F_ (E0_succ alpha) n < iterate (F_ alpha) (S n) (S n).
Lemma L2 : exp2 (F_ (E0_succ alpha) n) ≤ (F_ (E0_succ alpha) (S n)).
End S2.
Lemma L3 : P (E0_succ alpha).
End Successor.
Section Limit.
Variable lambda : E0.
Hypothesis Hlambda : E0limit lambda.
Hypothesis IHlambda :
∀ alpha, E0fin 3 o≤ alpha → alpha o< lambda → P alpha.
Remark R5: ∀ beta, 3 o≤ beta → beta o< lambda →
∀ n, 2 ≤ n →
∀ p, n < p →
exp2 (F_ beta n) ≤ F_ beta p.
Section S3.
Variable n: nat.
Hypothesis Hn : 2 ≤ n.
Lemma L04 : ∀ beta:T1,
T1limit beta →
∀ n, leq lt (\F (S n)) (Canon.canon beta (S n)).
Lemma L04' : ∀ beta, E0limit beta →
∀ n, (S n) o≤
(Canon.Canon beta (S n)).
Lemma L4 : exp2 (F_ lambda n) ≤ F_ lambda (S n).
End S3.
End Limit.
Lemma L alpha : 3 o≤ alpha → P alpha.
End S1.
Theorem F_alpha_Sn alpha : 3 o≤ alpha →
∀ n, 2 ≤ n → exp2 (F_ alpha n) ≤ F_ alpha (S n).
What happens if alpha is less than 3, or n less than 2 ?