---

Step * 4 1 2 of Lemma regularize-k-regular


1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ¬↑regular-upto(k;n;f)
5. m : ℕ+
6. ¬↑regular-upto(k;m;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
14. b : ℕ+
15. seq-min-upper(k;j;f) = b ∈ ℕ+
16. ∀i:ℕ+j + 1. (((i * (f b)) - b * (f i)) ≤ ((2 * k) * (b - i)))
17. b ≤ j
18. a : ℤ
19. ((f b) + (2 * k)) = a ∈ ℤ
⊢ ((r((k * ((m * a) ÷ b * k)) - 2 * k)/r((2 * k) * m)) ≤ (r(a)/r((2 * k) * b)))
∧ ((r(a)/r((2 * k) * b)) ≤ (r((k * ((m * a) ÷ b * k)) + (2 * k))/r((2 * k) * m)))
BY
{ ((InstLemma `rational-approx-property` [⌜(r(a))/(2 * k) * b⌝;⌜m⌝]⋅ THENA Auto)
   THEN RepUR ``rational-approx`` -1
   THEN Subst' (r(a))/(2 * k) * b m ~ (m * a) ÷ k * b -1) }

1
.....equality..... 
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ¬↑regular-upto(k;n;f)
5. m : ℕ+
6. ¬↑regular-upto(k;m;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
14. b : ℕ+
15. seq-min-upper(k;j;f) = b ∈ ℕ+
16. ∀i:ℕ+j + 1. (((i * (f b)) - b * (f i)) ≤ ((2 * k) * (b - i)))
17. b ≤ j
18. a : ℤ
19. ((f b) + (2 * k)) = a ∈ ℤ
20. |(r(a))/(2 * k) * b - (r((r(a))/(2 * k) * b m))/2 * m| ≤ (r1/r(m))
⊢ (r(a))/(2 * k) * b m ~ (m * a) ÷ k * b

2
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. ¬↑regular-upto(k;n;f)
5. m : ℕ+
6. ¬↑regular-upto(k;m;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
14. b : ℕ+
15. seq-min-upper(k;j;f) = b ∈ ℕ+
16. ∀i:ℕ+j + 1. (((i * (f b)) - b * (f i)) ≤ ((2 * k) * (b - i)))
17. b ≤ j
18. a : ℤ
19. ((f b) + (2 * k)) = a ∈ ℤ
20. |(r(a))/(2 * k) * b - (r((m * a) ÷ k * b))/2 * m| ≤ (r1/r(m))
⊢ ((r((k * ((m * a) ÷ b * k)) - 2 * k)/r((2 * k) * m)) ≤ (r(a)/r((2 * k) * b)))
∧ ((r(a)/r((2 * k) * b)) ≤ (r((k * ((m * a) ÷ b * k)) + (2 * k))/r((2 * k) * m)))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  \mneg{}\muparrow{}regular-upto(k;n;f)
5.  m  :  \mBbbN{}\msupplus{}
6.  \mneg{}\muparrow{}regular-upto(k;m;f)
7.  v  :  \mBbbN{}
8.  \mneg{}\muparrow{}regular-upto(k;v;f)
9.  \mforall{}[i:\mBbbN{}].  \mneg{}\mneg{}\muparrow{}regular-upto(k;i;f)  supposing  i  <  v
10.  \mneg{}(v  =  1)
11.  \mneg{}(v  =  0)
12.  j  :  \mBbbN{}\msupplus{}
13.  (v  -  1)  =  j
14.  b  :  \mBbbN{}\msupplus{}
15.  seq-min-upper(k;j;f)  =  b
16.  \mforall{}i:\mBbbN{}\msupplus{}j  +  1.  (((i  *  (f  b))  -  b  *  (f  i))  \mleq{}  ((2  *  k)  *  (b  -  i)))
17.  b  \mleq{}  j
18.  a  :  \mBbbZ{}
19.  ((f  b)  +  (2  *  k))  =  a
\mvdash{}  ((r((k  *  ((m  *  a)  \mdiv{}  b  *  k))  -  2  *  k)/r((2  *  k)  *  m))  \mleq{}  (r(a)/r((2  *  k)  *  b)))
\mwedge{}  ((r(a)/r((2  *  k)  *  b))  \mleq{}  (r((k  *  ((m  *  a)  \mdiv{}  b  *  k))  +  (2  *  k))/r((2  *  k)  *  m)))


By

---

Latex:
((InstLemma  `rational-approx-property`  [\mkleeneopen{}(r(a))/(2  *  k)  *  b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``rational-approx``  -1
  THEN  Subst'  (r(a))/(2  *  k)  *  b  m  \msim{}  (m  *  a)  \mdiv{}  k  *  b  -1)

---

Home Index