Rat.finite_rat_abs_sub_lt_one_div_den_sq
theorem Rat.finite_rat_abs_sub_lt_one_div_den_sq : ∀ (ξ : ℚ), {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite
This theorem states that for any given rational number, denoted as ξ, there exists only a finite set of rational numbers (q) such that the absolute difference between ξ and q is less than one divided by the square of the denominator of q. In other words, the number of "good" rational approximations (those within a certain precision based on the size of their denominator) for any given rational number is finite.
More concisely: For any rational number ξ, there exist only finitely many rational numbers q with denominator larger than some constant such that |ξ - q| < 1 / |q|^2.
|
Real.exists_rat_abs_sub_lt_and_lt_of_irrational
theorem Real.exists_rat_abs_sub_lt_and_lt_of_irrational :
∀ {ξ : ℝ}, Irrational ξ → ∀ (q : ℚ), ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
This theorem states that for any irrational real number `ξ` and any rational number `q` which is an approximation to `ξ`, there exists a better rational approximation `q'` such that the absolute difference between `ξ` and `q'` is less than `1` divided by the square of the denominator of `q'` and is also less than the absolute difference between `ξ` and `q`. In other words, given any rational approximation to an irrational number, it's always possible to find a better rational approximation.
More concisely: For any irrational real number `ξ` and rational approximation `q`, there exists a better rational approximation `q'` such that the absolute difference between `ξ` and `q'` is strictly less than the absolute difference between `ξ` and `q` divided by the square of the denominator of `q'`.
|
Real.exists_int_int_abs_mul_sub_le
theorem Real.exists_int_int_abs_mul_sub_le :
∀ (ξ : ℝ) {n : ℕ}, 0 < n → ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
Dirichlet's Approximation Theorem states that for any given real number `ξ` and a positive natural number `n`, it's possible to find integers `j` and `k` such that `k` falls within the range of 1 to `n` (both inclusive), and the absolute value of `k * ξ - j` is less than or equal to `1/(n+1)`. This theorem is useful in number theory for providing approximations of real numbers by rational numbers.
More concisely: For any real number `ξ` and positive natural number `n`, there exist integers `j` and `k` with `1 ≤ k ≤ n` such that the absolute value of `k * ξ - j` is less than or equal to `1 / (n + 1)`.
|
Real.exists_continued_fraction_convergent_eq_rat
theorem Real.exists_continued_fraction_convergent_eq_rat :
∀ {ξ : ℝ} {q : ℚ}, |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2) → ∃ n, (GeneralizedContinuedFraction.of ξ).convergents n = ↑q
This theorem is a statement of Legendre's Theorem on rational approximation. The theorem states that for any real number `ξ` and any rational number `q`, if the absolute difference between `ξ` and `q` is less than `1 / (2 * q.den^2)`, then `q` is a convergent of the continued fraction expansion of `ξ`. This particular version of the theorem uses the `generalized_continued_fraction.convergents` function to compute the convergents of the continued fraction expansion.
More concisely: If the absolute difference between real number `ξ` and rational number `q` is less than `1 / (2 * q.den^2)`, then `q` is a convergent in the continued fraction expansion of `ξ`.
|
Real.exists_rat_eq_convergent
theorem Real.exists_rat_eq_convergent : ∀ {ξ : ℝ} {q : ℚ}, |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2) → ∃ n, q = ξ.convergent n
This is a statement of Legendre's Theorem on rational approximation in the context of real numbers. The theorem states that given any real number `ξ` and any rational number `q`, if the absolute difference between `ξ` and `q` is less than `1 / (2 * q.den ^ 2)`, then `q` must be a convergent of the continued fraction expansion of `ξ`. In other words, there exists an integer `n` such that `q` is the `n`th convergent of `ξ`. The function `ξ.convergent n` in Lean 4 represents the `n`th convergent of the continued fraction expansion of `ξ`.
More concisely: Given any real number `ξ` and rational number `q`, if `|ξ - q| < 1 / (2 * q.den ^ 2)`, then `q` is the `n`th convergent of the continued fraction expansion of `ξ` for some `n`.
|
Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq
theorem Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq :
∀ {ξ q : ℚ}, |ξ - q| < 1 / ↑q.den ^ 2 → q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1 := by
sorry
The theorem `Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq` states that for any two rational numbers `ξ` and `q`, if the absolute value of their difference is less than one divided by the square of the denominator of `q`, then the denominator of `q` is less than or equal to the denominator of `ξ`, and the numerator of `q` is bounded by `ξ` times the denominator of `q`, rounded up minus one and rounded down plus one. This theorem outlines the constraints on the numerator and denominator of a rational number that is a good approximation to another rational number.
More concisely: Given rational numbers ξ and q, if |ξ - q| < 1 / (denominator q)^2, then denominator q is less than or equal to denominator ξ and |numerator q - ξ * denominator q| ≤ 1.
|
Real.convergent_zero
theorem Real.convergent_zero : ∀ (ξ : ℝ), ξ.convergent 0 = ↑⌊ξ⌋
The theorem `Real.convergent_zero` states that for any real number `ξ`, the zeroth term of its sequence of convergents is equal to the greatest integer less than or equal to `ξ`, denoted by `⌊ξ⌋`. In other words, the floor function of a real number provides the first term in the number's sequence of convergents.
More concisely: The theorem `Real.convergent_zero` asserts that the zeroth convergent of a real number `ξ` equals its floor `⌊ξ⌋`.
|
Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational
theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational :
∀ (ξ : ℝ), {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite ↔ Irrational ξ
The theorem states that for any real number `ξ`, the set of rational numbers such that the absolute difference between `ξ` and the rational number is less than one divided by the square of the denominator of the rational number, is infinite if and only if `ξ` is an irrational number. In other words, the theorem establishes a condition for a real number to be irrational: A real number `ξ` is irrational if and only if there are infinitely many rational numbers that approximate `ξ` with an error less than the reciprocal of the square of their denominators.
More concisely: A real number `ξ` is irrational if and only if there exist infinitely many rational numbers `q` such that `|ξ - q| < 1 / (2 ^ 2 * |q|)`.
|
Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational
theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational :
∀ {ξ : ℝ}, Irrational ξ → {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
This theorem states that if `ξ` is an irrational real number, then there exist infinitely many rational numbers `q` such that the absolute difference between `ξ` and `q` is less than the reciprocal of the square of the denominator of `q`. In simpler terms, no matter how irrational a number `ξ` is, we can always find an infinite number of rational numbers that are extremely close to it—where "closeness" is defined relative to the size of the rational number's denominator.
More concisely: For every irrational real number `ξ`, there exists an infinite sequence of rational numbers `{q_n}` such that `|ξ - q_n| < 1 / (denominator(q_n))^2` for all `n`.
|
Real.convergent_succ
theorem Real.convergent_succ : ∀ (ξ : ℝ) (n : ℕ), ξ.convergent (n + 1) = ↑⌊ξ⌋ + ((Int.fract ξ)⁻¹.convergent n)⁻¹ := by
sorry
The theorem `Real.convergent_succ` describes a property of the (n+1)th convergent of a real number ξ. It states that for any real number ξ and any natural number n, the (n+1)th convergent of ξ is equal to the greatest integer less than or equal to ξ (denoted as ⌊ξ⌋) plus the reciprocal of the nth convergent of the reciprocal of the fractional part of ξ. In other words, it provides a relationship between the progressions of convergents for a real number and its fractional part.
More concisely: For any real number ξ and natural number n, the (n+1)th convergent of ξ is equal to the floor of ξ plus the reciprocal of the nth convergent of ξ's reciprocal fractional part.
|
Real.convergent_of_zero
theorem Real.convergent_of_zero : ∀ (n : ℕ), Real.convergent 0 n = 0
This theorem states that all convergents of 0 are zero. In other words, for every natural number 'n', the value of the nth convergent for 0 in the real numbers is 0.
More concisely: For all natural numbers n, the n-th convergent of 0 in the real numbers is equal to 0.
|
Real.exists_rat_abs_sub_le_and_den_le
theorem Real.exists_rat_abs_sub_le_and_den_le :
∀ (ξ : ℝ) {n : ℕ}, 0 < n → ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n
The theorem, known as *Dirichlet's approximation theorem*, states that for any given real number `ξ` and a positive natural number `n`, there exists a rational number `q` satisfying two conditions: the denominator of `q`(i.e., `q.den`) is less than or equal to `n`, and the absolute difference between `ξ` and `q` is less than or equal to the reciprocal of the product of `n+1` and the denominator of `q`. This theorem is a cornerstone in the field of Diophantine approximation. It is referenced in another theorem `AddCircle.exists_norm_nsmul_le`.
More concisely: For any real number `ξ` and natural number `n`, there exists a rational number `q` with denominator `q.den ≤ n` such that the absolute difference between `ξ` and `q` is less than `1/(n+1) * q.den`.
|
Real.exists_rat_eq_convergent'
theorem Real.exists_rat_eq_convergent' :
∀ {ξ : ℝ} {u : ℤ} {v : ℕ}, Real.ContfracLegendre.Ass ξ u ↑v → ∃ n, ↑u / ↑v = ξ.convergent n
This is the technical version of *Legendre's Theorem*. The theorem states that for any real number ξ and integers u and v, if the condition `Real.ContfracLegendre.Ass ξ u v` holds true, then there exists an integer n such that the rational number u/v is the nth convergent of ξ. Here, the condition `Real.ContfracLegendre.Ass ξ u v` requires that u and v are coprime, that if v equals 1 then `-1/2 < ξ - u`, and that the absolute value of `ξ - u/v` is less than the reciprocal of `v*(2*v - 1)`.
More concisely: Given real number ξ and coprime integers u and v, if $-1/2 < ξ - u$ when v = 1 and $|\xi - u/v| < 1/(v(v-1))$, then u/v is the nth convergent of ξ in its continued fraction expansion.
|
Real.continued_fraction_convergent_eq_convergent
theorem Real.continued_fraction_convergent_eq_convergent :
∀ (ξ : ℝ) (n : ℕ), (GeneralizedContinuedFraction.of ξ).convergents n = ↑(ξ.convergent n)
This theorem states that for any real number `ξ` and any natural number `n`, the `n`th convergent of the generalized continued fraction representation of `ξ` is equal to the `n`th convergent of `ξ` itself. This equivalence means that the iterative approximation process using continued fractions can accurately represent `ξ` to the `n`th degree of precision.
More concisely: For any real number `ξ` and natural number `n`, the `n`-th convergent of `ξ` in its generalized continued fraction representation equals the `n`-th convergent of `ξ` itself.
|
Real.convergent_of_int
theorem Real.convergent_of_int : ∀ {ξ : ℤ} (n : ℕ), (↑ξ).convergent n = ↑ξ
This theorem states that if `ξ` is an integer, then for any natural number `n`, the `n`-th convergent of `ξ` is equal to `ξ`. In other words, if we consider any integer as a real number and calculate its convergents, each of the convergents will always equal the original integer, irrespective of the index of the convergent.
More concisely: For any integer `ξ`, the `n`-th convergent of `ξ` as a rational number is equal to `ξ` for all natural numbers `n`.
|
Real.exists_nat_abs_mul_sub_round_le
theorem Real.exists_nat_abs_mul_sub_round_le :
∀ (ξ : ℝ) {n : ℕ}, 0 < n → ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
The theorem is a statement of Dirichlet's Approximation Theorem. It states that for any real number ξ and any positive natural number n, there exists a natural number k, where 0 < k ≤ n, such that the absolute difference between kξ and the nearest integer to kξ is less or equal to 1 divided by (n + 1). Here, `round` is a function that rounds a number to the nearest integer.
More concisely: For any real number ξ and positive natural number n, there exists a natural number k with 0 < k <= n such that |kξ - round(kξ)| <= 1 / (n + 1).
|