equal
deleted
inserted
replaced
10 Summation |
10 Summation |
11 Integral_Test |
11 Integral_Test |
12 begin |
12 begin |
13 |
13 |
14 text \<open> |
14 text \<open> |
15 The definition of the Harmonic Numbers and the Euler–Mascheroni constant. |
15 The definition of the Harmonic Numbers and the Euler-Mascheroni constant. |
16 Also provides a reasonably accurate approximation of @{term "ln 2 :: real"} |
16 Also provides a reasonably accurate approximation of @{term "ln 2 :: real"} |
17 and the Euler–Mascheroni constant. |
17 and the Euler-Mascheroni constant. |
18 \<close> |
18 \<close> |
19 |
19 |
20 lemma ln_2_less_1: "ln 2 < (1::real)" |
20 lemma ln_2_less_1: "ln 2 < (1::real)" |
21 proof - |
21 proof - |
22 have "2 < 5/(2::real)" by simp |
22 have "2 < 5/(2::real)" by simp |