Real.cos_pi_div_six
theorem Real.cos_pi_div_six : (Real.pi / 6).cos = √3 / 2
The theorem `Real.cos_pi_div_six` states that the cosine of `π / 6` is equal to the square root of 3 divided by 2. This is a well-known result in trigonometry. Here, `Real.cos` refers to the cosine function over real numbers, `Real.pi` denotes the mathematical constant π (approximately 3.14159), and `Real.sqrt` indicates the square root function over real numbers. Therefore, in conventional mathematical notation, this theorem can be written as: cos(π / 6) = √3 / 2.
More concisely: The cosine of π/6 equals the square root of 3/2.
|
Real.cos_pi_over_two_pow
theorem Real.cos_pi_over_two_pow : ∀ (n : ℕ), (Real.pi / 2 ^ (n + 1)).cos = Real.sqrtTwoAddSeries 0 n / 2
This theorem states that for any natural number `n`, the cosine of `π` divided by `2` to the power of `n + 1` (which is represented in Lean 4 as `Real.cos (Real.pi / 2 ^ (n + 1))`) is equal to the `n`th term of the series `sqrtTwoAddSeries` starting with 0 divided by 2 (`Real.sqrtTwoAddSeries 0 n / 2`). The series `sqrtTwoAddSeries` is defined as `sqrt(2 + sqrt(2 + ... ))` with `n` square roots.
More concisely: For any natural number `n`, `Real.cos (Real.pi / 2 ^ (n + 1))` equals `Real.sqrtTwoAddSeries 0 n / 2`.
|
Real.sin_pi_div_three
theorem Real.sin_pi_div_three : (Real.pi / 3).sin = √3 / 2
This theorem states that the sine of pi divided by three equals the square root of three divided by two. In mathematical terms, this can be written as sin(π/3) = √3/2.
More concisely: The sine of pi over 3 is equal to the square root of three halved. (sin(π/3) = √3/2)
|
Real.continuousOn_sin
theorem Real.continuousOn_sin : ∀ {s : Set ℝ}, ContinuousOn Real.sin s
This theorem states that the real sine function (`Real.sin`) is continuous on any subset `s` of real numbers. In mathematical terms, this means that for all `s` which is a set of real numbers, `Real.sin` is continuous at every point in `s`. Continuity, in the topological sense, implies that the function's value changes smoothly without any jumps or breaks over `s`.
More concisely: For any subset `s` of real numbers, the real sine function `Real.sin` is continuous on `s`.
|
NNReal.pi_ne_zero
theorem NNReal.pi_ne_zero : NNReal.pi ≠ 0
The theorem `NNReal.pi_ne_zero` asserts that π, when considered as a nonnegative real number (`NNReal.pi`), is not equal to zero. In other words, it states that the value of π is nonzero in the domain of nonnegative real numbers.
More concisely: The theorem `NNReal.pi_ne_zero` asserts that π (as a nonnegative real number) is distinct from zero.
|
Real.cos_pos_of_mem_Ioo
theorem Real.cos_pos_of_mem_Ioo : ∀ {x : ℝ}, x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → 0 < x.cos
The theorem `Real.cos_pos_of_mem_Ioo` states that for any real number `x`, if `x` belongs to the open interval from negative half pi to positive half pi (i.e., `x` is strictly greater than `-π/2` and strictly less than `π/2`), then the cosine of `x` is strictly greater than zero. This corresponds to the well-known fact from trigonometry that the cosine function is positive in the first and fourth quadrants of the unit circle, which correspond to the described interval in radians.
More concisely: If `x` is in the open interval `(-π/2, π/2)`, then `cos x > 0`.
|
Real.sin_periodic
theorem Real.sin_periodic : Function.Periodic Real.sin (2 * Real.pi)
The theorem `Real.sin_periodic` states that the real sine function is periodic with a period of `2 * Real.pi`. In other words, for any real number `x`, the value of `Real.sin(x + 2 * Real.pi)` is the same as the value of `Real.sin(x)`. This is in line with the well-known mathematical fact that the sine function repeats its values every `2π` radians.
More concisely: The real sine function is periodic with a period of 2π, i.e., Real.sin(x + 2π) = Real.sin(x) for all real x.
|
Real.continuous_cos
theorem Real.continuous_cos : Continuous Real.cos
This theorem states that the cosine function on real numbers is continuous. In mathematical terms, it means that for every real number `x` and any positive number `ε`, there exists a positive number `δ` such that for all real numbers `y`, if the absolute difference between `x` and `y` is less than `δ`, then the absolute difference between `cos(x)` and `cos(y)` is less than `ε`. This captures the intuitive notion that small changes in the input of the cosine function lead to small changes in the output.
More concisely: The cosine function is a continuous function on the real numbers.
|
Real.injOn_sin
theorem Real.injOn_sin : Set.InjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
The theorem `Real.injOn_sin` states that the real sine function `Real.sin` is injective, which means it does not produce the same output for two different inputs, when it is restricted to the interval `Set.Icc (-(Real.pi / 2)) (Real.pi / 2)`. In other words, for any two different numbers in the interval from negative half-pi to half-pi, their sine values are also different.
More concisely: The sine function restricted to the interval `(-π/2, π/2)` is injective.
|
Complex.cos_antiperiodic
theorem Complex.cos_antiperiodic : Function.Antiperiodic Complex.cos ↑Real.pi
The theorem `Complex.cos_antiperiodic` states that the complex cosine function (`Complex.cos`) is antiperiodic with a period equal to pi (`Real.pi`). This means that for every complex number `z`, the value of `Complex.cos` at `z` plus pi is the negative of the value of `Complex.cos` at `z` i.e., `Complex.cos (z + π) = - Complex.cos z`. It essentially states the well-known property of the cosine function being antiperiodic with respect to the period π in the complex plane.
More concisely: The complex cosine function `Complex.cos` is antiperiodic with period `Real.pi`, i.e., `Complex.cos (z + Real.pi) = - Complex.cos z` for all complex numbers `z`.
|
Real.cos_antiperiodic
theorem Real.cos_antiperiodic : Function.Antiperiodic Real.cos Real.pi
The theorem `Real.cos_antiperiodic` states that the real cosine function, denoted by `Real.cos`, is antiperiodic with an antiperiod of pi (`Real.pi`). In other words, for any real number `x`, the cosine of `x + pi` is equal to the negative of the cosine of `x`, or formally, $\cos(x + \pi) = -\cos(x)$ for all real `x`. This fact is a well-known property of the cosine function in trigonometry.
More concisely: The cosine function is antiperiodic with a period of pi, i.e., $\cos(x+\pi) = -\cos(x)$ for all real numbers $x$.
|
Complex.exp_antiperiodic
theorem Complex.exp_antiperiodic : Function.Antiperiodic Complex.exp (↑Real.pi * Complex.I)
This theorem states that the complex exponential function is "antiperiodic" with an antiperiod of "pi times the imaginary unit". In other words, for any complex number z, the value of the complex exponential function at (z + pi * i) is the negative of its value at z. This property is similar to periodicity, but involves a sign change in addition to the function repeating its values.
More concisely: The complex exponential function is a complex-valued function with a negative conjugate symmetry, specifically, exp(z) = -exp(z + πi) for all complex numbers z.
|
Real.sin_nonneg_of_mem_Icc
theorem Real.sin_nonneg_of_mem_Icc : ∀ {x : ℝ}, x ∈ Set.Icc 0 Real.pi → 0 ≤ x.sin
This theorem states that for any real number 'x', if 'x' lies in the interval from 0 to π (both inclusive), then the sine of 'x' is non-negative. In mathematical terms, this is saying that for all real numbers 'x', if '0 ≤ x ≤ π', then '0 ≤ sin(x)'. This result is a consequence of the properties of the sine function on the interval [0, π] in trigonometry.
More concisely: For all real numbers x, if 0 ≤ x ≤ π, then 0 ≤ sin(x).
|
Real.cos_nonneg_of_mem_Icc
theorem Real.cos_nonneg_of_mem_Icc : ∀ {x : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → 0 ≤ x.cos
The theorem `Real.cos_nonneg_of_mem_Icc` asserts that for any real number `x`, if `x` lies in the closed interval from negative pi over 2 to pi over 2 (inclusive), then the cosine of `x` is nonnegative. In mathematical terms, this means that for all $x \in [-\pi/2, \pi/2]$, we have $\cos(x) \geq 0$. This is a property of the cosine function in the real number system.
More concisely: For all $x \in [-\pi/2, \pi/2]$, we have $\cos(x) \geq 0$.
|
Complex.abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le
theorem Complex.abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le :
∀ {a b : ℝ},
a ≤ 0 →
∀ {z : ℂ},
|z.im| ≤ b → b ≤ Real.pi / 2 → Complex.abs (↑a * (z.exp + (-z).exp)).exp ≤ (a * b.cos * |z.re|.exp).exp
This is a support lemma for the Phragmen-Lindelöf principle in the context of complex numbers. The lemma states that for any real numbers `a` and `b`, with `a` less than or equal to zero, and any complex number `z` such that the absolute value of the imaginary part of `z` is less than or equal to `b` and `b` is less than or equal to the half of the number pi, the absolute value of the exponential of `a` times the sum of the exponentiation of `z` and its negation, is less than or equal to the exponential of `a` times the cosine of `b` times the exponentiation of the absolute value of the real part of `z`. In mathematical terms, if `|Im(z)| ≤ b`, `b ≤ π / 2`, and `a ≤ 0`, then the inequality $|\exp^{a(e^{z}+e^{-z})}| ≤ \exp^{a \cos(b) \exp^{|Re(z)|}}$ holds true.
More concisely: For complex numbers $z$ with imaginary partIm(z) absolutely smaller than or equal to $b$ and real partRe(z) such that $b$ is less than or equal to $\pi / 2$ and $a$ is non-positive, we have $|\exp(az)(\exp(z) + \exp(-z))| \leq \exp(a\cos(b))\exp(|Re(z)|)$.
|
Complex.continuous_cos
theorem Complex.continuous_cos : Continuous Complex.cos
This theorem states that the cosine function for complex numbers is continuous. In other words, for every point in the complex plane, small changes in the input result in arbitrarily small changes in the output of the complex cosine function. This function is defined via the exponential function (exp), where for a given complex number `z`, `Complex.cos z` is computed as `(Complex.exp (z * Complex.I) + Complex.exp (-z * Complex.I)) / 2`.
More concisely: The complex cosine function, defined as the real part of the complex number ((exp (z * I) + exp (-z * I)) / 2) for complex number z, is a continuous function.
|
Complex.cos_sub_pi_div_two
theorem Complex.cos_sub_pi_div_two : ∀ (x : ℂ), (x - ↑Real.pi / 2).cos = x.sin
The theorem `Complex.cos_sub_pi_div_two` states that for any complex number `x`, the cosine of (`x - π/2`) is equal to the sine of `x`. Here, `π` represents the mathematical constant Pi, `-` denotes subtraction, and `↑Real.pi / 2` is the Lean 4 way of expressing "pi divided by 2". The functions `Complex.cos` and `Complex.sin` are the complex versions of the cosine and sine functions, with both functions defined via the exponential function (`exp`). The theorem essentially establishes a shift property between the complex sine and cosine functions.
More concisely: The theorem asserts that for any complex number x, the cosine of (x - π/2) equals the sine of x.
|
Complex.sin_periodic
theorem Complex.sin_periodic : Function.Periodic Complex.sin (2 * ↑Real.pi)
This theorem states that the complex sine function is periodic with a period of `2 * π`. In other words, for any complex number `z`, the value of `sin(z + 2π)` is equal to `sin(z)`. Here, `π` is defined as `3.14159265...`, which is twice a zero of the cosine function in the interval `[1,2]`. The periodic nature of the complex sine function is a fundamental property in complex analysis and trigonometry.
More concisely: The complex sine function is periodic with a period of 2π, i.e., sin(z + 2π) = sin(z) for all complex numbers z.
|
Real.continuousOn_cos
theorem Real.continuousOn_cos : ∀ {s : Set ℝ}, ContinuousOn Real.cos s
This theorem states that for any set of real numbers `s`, the cosine function is continuous on `s`. In other words, for each point in the set `s`, the real cosine function does not make any jumps or breaks, meaning that as the input values approach any particular point in `s`, the output of the cosine function also approaches the value of the cosine function at that point. This characteristic of the cosine function holds true for any subset of real numbers, not just the entire set of real numbers.
More concisely: The cosine function is continuous on any set of real numbers.
|
Real.two_pi_pos
theorem Real.two_pi_pos : 0 < 2 * Real.pi
This theorem states that the product of 2 and π (pi), where π is defined as twice a zero of cosine in the interval [1,2], is a positive real number. In mathematical notation, this is expressed as 0 < 2 * π.
More concisely: The theorem asserts that the product of 2 and the real number π, defined as twice a zero of cosine in the interval [1, 2], is a positive real number. In mathematical notation, 2 * π > 0.
|
Complex.cos_periodic
theorem Complex.cos_periodic : Function.Periodic Complex.cos (2 * ↑Real.pi)
The theorem `Complex.cos_periodic` states that the complex cosine function, `Complex.cos`, is periodic with a period of `2 * Real.pi`. In other words, for all complex numbers `z`, the value of `Complex.cos` at `z + 2π` (where `π` is the constant `Real.pi` representing the mathematical constant pi) is equal to the value of `Complex.cos` at `z`. This is a reflection of the well-known property in trigonometry that the cosine function repeats its values every `2π` radians.
More concisely: The complex cosine function, `Complex.cos`, is periodic with a period of `2 * Real.pi`. In other words, `Complex.cos (z + 2π) = Complex.cos z` for all complex numbers `z`.
|
Real.sin_antiperiodic
theorem Real.sin_antiperiodic : Function.Antiperiodic Real.sin Real.pi
The theorem `Real.sin_antiperiodic` states that the sine function is antiperiodic with the antiperiod being π. An antiperiodic function is defined such that for any given input, the value of the function at the input plus the antiperiod is the negation of the value of the function at the input. In this case, for any real number `x`, `sin(x + π) = -sin(x)`.
More concisely: For all real numbers x, sin(x + π) = -sin(x).
|
Real.sin_pi
theorem Real.sin_pi : Real.pi.sin = 0
The theorem `Real.sin_pi` asserts that the sine of π (Pi), as defined in the real numbers, is equal to zero. This is a commonly known fact in trigonometry, which states that sin(π) = 0. Here, π is defined as twice a zero of cosine in the interval [1,2]. The sine function is defined as the real part of the complex sine.
More concisely: The theorem `Real.sin_pi` asserts that the real part of the complex sine of π (Pi), defined as twice a zero of cosine in the interval [1,2], equals zero.
|
Real.sin_pi_div_two
theorem Real.sin_pi_div_two : (Real.pi / 2).sin = 1
This theorem states that the sine of pi divided by 2, in real numbers, is equal to 1. In other words, it is expressing the well-known trigonometric fact that $\sin(\pi/2) = 1$ where $\pi$ is the mathematical constant Pi. The sine function here is defined as the real part of the complex sine.
More concisely: The real part of the complex sine of π/2 is equal to 1.
|
Real.injOn_cos
theorem Real.injOn_cos : Set.InjOn Real.cos (Set.Icc 0 Real.pi)
This theorem states that the real cosine function is injective, i.e., it doesn't map distinct arguments to the same result, when restricted to the interval ranging from 0 to π (both endpoints inclusive). In other words, for any two distinct real numbers x₁ and x₂ in the range from 0 to π, cos(x₁) is not equal to cos(x₂).
More concisely: The cosine function is injective on the interval [0, π].
|
Real.sin_pi_over_two_pow_succ
theorem Real.sin_pi_over_two_pow_succ :
∀ (n : ℕ), (Real.pi / 2 ^ (n + 2)).sin = (2 - Real.sqrtTwoAddSeries 0 n).sqrt / 2
This theorem states that for every natural number `n`, the sine of pi divided by 2 raised to the power of `n + 2` equals to the square root of the difference between 2 and the `n`-th term of the `sqrtTwoAddSeries` starting from 0, all divided by 2. In mathematical notation, for all natural numbers `n`, we have $\sin \left(\frac{\pi}{2^{n+2}}\right) = \frac{\sqrt{2 - \text{sqrtTwoAddSeries}(0,n)}}{2}$. This series, `sqrtTwoAddSeries`, represents an iterative calculation of square roots in the form of $\sqrt{2 + \sqrt{2 + \ldots}}$ with `n` square roots, starting with an initial value of 0.
More concisely: For every natural number `n`, the sine of pi divided by 2 raised to the power of `n + 2` equals to half of the difference between 2 and the sum of the first `n` terms of the square root of 2 iterative series, `sqrtTwoAddSeries`, starting from 0.
|
Real.sq_cos_pi_div_six
theorem Real.sq_cos_pi_div_six : (Real.pi / 6).cos ^ 2 = 3 / 4
This theorem states that the square of the cosine of pi divided by 6 (or π/6 as written in Lean 4) equals 3/4. That is, when π/6 is used as the angle in the cosine function, and the result further squared, the value obtained is precisely 3/4. This theorem can sometimes be more convenient than directly using the result for the cosine of π/6 itself.
More concisely: The square of the cosine of π/6 equals 3/4.
|
Real.sin_nonneg_of_nonneg_of_le_pi
theorem Real.sin_nonneg_of_nonneg_of_le_pi : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → 0 ≤ x.sin
This theorem states that for all real numbers `x`, if `x` is nonnegative and less than or equal to the value of pi (`π`), then the sine of `x` is nonnegative. In other words, the sine function returns a nonnegative real number when its input is a real number between 0 and `π` inclusive.
More concisely: For all real numbers `x` with `0 ≤ x ≤ π`, the sine of `x` is nonnegative (i.e., `sin x ≥ 0`).
|
Real.pi_pos
theorem Real.pi_pos : 0 < Real.pi
This theorem states that the real number π (pi), which is defined as twice a zero of the cosine function in the interval [1,2], is greater than zero. In other words, the value of π is positive.
More concisely: The theorem asserts that 0 < π, where π is defined as the positive root of the polynomial x => x^2 + x - 1 in the interval (1, 2).
|
Real.pi_div_two_pos
theorem Real.pi_div_two_pos : 0 < Real.pi / 2
The theorem `Real.pi_div_two_pos` asserts that the number Pi divided by 2 is greater than zero. In other words, it establishes the positivity of half of Pi, a basic and important property of this mathematical constant in the field of real numbers.
More concisely: The theorem `Real.pi_div_two_pos` asserts that 0 < Pi / 2 in the real numbers.
|
Real.sin_mem_Icc
theorem Real.sin_mem_Icc : ∀ (x : ℝ), x.sin ∈ Set.Icc (-1) 1
This theorem states that for all real numbers `x`, the sine of `x` (denoted as `Real.sin x` in Lean 4) lies in the closed interval from -1 to 1. In other words, the real value of the sine function for any real number is always between -1 and 1, inclusive. This is a mathematical property of the sine function, which is known to fluctuate between -1 and 1, inclusive.
More concisely: For all real numbers x, |Real.sin x| ≤ 1.
|
Complex.continuous_sin
theorem Complex.continuous_sin : Continuous Complex.sin
This theorem states that the complex sine function is continuous. In other words, for any point in the complex plane, the sine function varies smoothly without any jumps, breaks, or holes around that point. In mathematical terms, the complex sine function, defined as `sin(z) = (e^(-zi) - e^(zi)) * i / 2`, has the property of continuity.
More concisely: The complex sine function, defined as `sin(z) := (e^(-zi) - e^(zi)) * I / 2`, is a continuous function on the complex plane.
|
Complex.tan_periodic
theorem Complex.tan_periodic : Function.Periodic Complex.tan ↑Real.pi
The theorem `Complex.tan_periodic` states that the complex tangent function, defined as the ratio of the sine to the cosine of a complex number, is periodic with a period of π (pi, the ratio of a circle's circumference to its diameter). This means that for any complex number `z`, `tan(z + π) = tan(z)`.
More concisely: The complex tangent function is periodic with a period of pi, i.e., tan(z + pi) = tan(z) for all complex numbers z.
|
Real.sin_neg_of_neg_of_neg_pi_lt
theorem Real.sin_neg_of_neg_of_neg_pi_lt : ∀ {x : ℝ}, x < 0 → -Real.pi < x → x.sin < 0
This theorem states that for any real number `x`, if `x` is less than 0 and greater than negative pi (`-π`), then the sine of `x` is also less than 0. It, in essence, establishes that the sine of a real number within the interval `(-π,0)` is negative.
More concisely: For any real number `x` with `x < 0` and `x > -π`, we have `sin(x) < 0`.
|
Complex.cos_pi_div_two
theorem Complex.cos_pi_div_two : (↑Real.pi / 2).cos = 0
This theorem states that the cosine of pi divided by two, when evaluated in the field of complex numbers, equals zero. Here, pi is a real number defined as twice a zero of the cosine function in the interval [1,2]. The complex cosine function is defined using the exponential function. In mathematical terms, this theorem corresponds to the well-known result cos(π/2) = 0.
More concisely: The cosine of pi over 2, evaluated in the complex numbers, equals zero, where pi is the real number defined as twice a zero of the cosine function in the interval [1,2].
|
Real.two_le_pi
theorem Real.two_le_pi : 2 ≤ Real.pi
The theorem `Real.two_le_pi` states that the number 2 is less than or equal to π, the mathematical constant representing the ratio of a circle's circumference to its diameter, in real numbers. It formalizes the numerical fact that π, approximately 3.14159265, is indeed greater than 2.
More concisely: The theorem `Real.two_le_pi` asserts that 2 ≤ π in the real number system.
|
Real.cos_pi
theorem Real.cos_pi : Real.pi.cos = -1
The theorem `Real.cos_pi` states that the cosine of pi in real numbers is equal to -1. In other words, it asserts that the value of the function `Real.cos` at the point `Real.pi` is -1. This is a standard result in trigonometry, represented here in Lean 4.
More concisely: The theorem `Real.cos_pi` asserts that `Real.cos (Real.pi) = -1` in Lean 4.
|
Complex.exp_periodic
theorem Complex.exp_periodic : Function.Periodic Complex.exp (2 * ↑Real.pi * Complex.I)
The theorem `Complex.exp_periodic` states that the complex exponential function is periodic with a period of `2 * π * i`, where `i` is the imaginary unit. In other words, for any complex number `z`, the value of the complex exponential function at `z + 2πi` is the same as its value at `z`. This is a formal version of the well-known fact from complex analysis that `e^(z + 2πi) = e^z` for all complex `z`.
More concisely: The complex exponential function is periodic with a period of `2 * π * i`. That is, `Complex.exp (z + 2 * π * i) = Complex.exp z` for all complex `z`.
|
Real.sin_pos_of_pos_of_lt_pi
theorem Real.sin_pos_of_pos_of_lt_pi : ∀ {x : ℝ}, 0 < x → x < Real.pi → 0 < x.sin
This theorem states that for all real numbers `x`, if `x` is greater than 0 and less than π (pi), then the sine of `x` is greater than 0. In mathematical terms, it can be written as: for all `x` in ℝ, if `0 < x < π` then `0 < sin(x)`. This is a reflection of the property of the sine function on the interval `(0, π)` in the real number line.
More concisely: For all real numbers `x`, if `0 < x < π`, then `sin(x) > 0`.
|
Real.pi_ne_zero
theorem Real.pi_ne_zero : Real.pi ≠ 0
This theorem states that the number pi, denoted as π in mathematics and defined as twice a zero of the cosine function in the range [1, 2], is not equal to zero. Simply put, it asserts the non-zero nature of the mathematical constant π.
More concisely: The theorem asserts that the mathematical constant π, defined as a zero of cosine in the range [1, 2], is non-zero.
|
Complex.cos_pi
theorem Complex.cos_pi : (↑Real.pi).cos = -1
The theorem `Complex.cos_pi` states that the cosine of pi in the complex number system is equal to -1. Here, pi is defined as twice a zero of the cosine function in the interval [1,2]. This theorem is fundamental in trigonometry and underlies many properties related to the unit circle and the cosine function.
More concisely: The cosine of pi in the complex number system equals -1, where pi is defined as the double root of the cosine function in the interval [1, 2].
|
Real.sin_int_mul_pi
theorem Real.sin_int_mul_pi : ∀ (n : ℤ), (↑n * Real.pi).sin = 0
This theorem states that for all integers 'n', the sine of 'n' times pi is equal to zero. In mathematical terms, it states that for any integer \(n\), \(\sin(n \pi) = 0\). This is a well-known result in trigonometry, reflecting the periodicity and symmetry of the sine function.
More concisely: For all integers n, sin(nπ) = 0.
|
Real.cos_pi_div_two
theorem Real.cos_pi_div_two : (Real.pi / 2).cos = 0
This theorem states that the cosine of pi divided by two, when calculated on the set of real numbers, equals zero. In other words, it formalizes the well-known trigonometric property that $\cos(\pi / 2) = 0$ in the context of real numbers.
More concisely: cos (pi / 2) = 0 on the set of real numbers.
|
Real.exists_cos_eq_zero
theorem Real.exists_cos_eq_zero : 0 ∈ Real.cos '' Set.Icc 1 2
This theorem states that there exists a real number between 1 and 2 (inclusive) such that the cosine of that number is zero. In other words, the cosine function, when applied to some number within the closed interval from 1 to 2, yields zero.
More concisely: There exists a real number x in the interval [1, 2] such that cos(x) = 0.
|
Real.tan_periodic
theorem Real.tan_periodic : Function.Periodic Real.tan Real.pi
The theorem `Real.tan_periodic` states that the real tangent function (`Real.tan`) is periodic, with a period of π (`Real.pi`). In mathematical terms, this means that for all real numbers x, the value of `Real.tan (x + π)` is equal to the value of `Real.tan x`. This property is a well-known characteristic of the tangent function in trigonometry.
More concisely: The tangent function is periodic with a period of pi, that is, tan(x + pi) = tan(x) for all real numbers x.
|
Real.continuous_sin
theorem Real.continuous_sin : Continuous Real.sin
This theorem states that the sine function, as defined on the real numbers, is continuous. In mathematical terms, this means for any real number and any positive epsilon, there exists a positive delta such that the absolute difference between the sine of any two real numbers less than delta apart is less than epsilon. This is a fundamental property of the sine function in calculus and real analysis.
More concisely: The sine function is a continuous real-valued function on the real numbers.
|
Real.cos_pi_div_two_sub
theorem Real.cos_pi_div_two_sub : ∀ (x : ℝ), (Real.pi / 2 - x).cos = x.sin
This theorem states that for all real numbers `x`, the cosine of the quantity `π/2 - x` is equal to the sine of `x`. In other words, it captures the property of the cosine and sine functions that `cos(π/2 - x) = sin(x)` for all `x` in the real numbers, where `π` is the mathematical constant pi and `cos` and `sin` represent the cosine and sine functions respectively.
More concisely: For all real numbers x, cos(π/2 - x) = sin(x).
|
Real.cos_pi_div_three
theorem Real.cos_pi_div_three : (Real.pi / 3).cos = 1 / 2
This theorem states that the cosine of π/3 is equal to 1/2. In other words, if you divide the number π (approximately 3.14159265...) by 3 and then take the cosine of the result, you will get the value 1/2. This is a well-known fact in trigonometry.
More concisely: Cosine of π/3 = 1/2.
|
Real.sin_pi_div_two_sub
theorem Real.sin_pi_div_two_sub : ∀ (x : ℝ), (Real.pi / 2 - x).sin = x.cos
This theorem states that for all real numbers `x`, the sine of (π/2 minus `x`) equals the cosine of `x`. In mathematical notation, this theorem is expressing the identity sin(π/2 - x) = cos(x), which is a fundamental identity in trigonometry. Here, π/2 is half of the number π, which in Lean 4 is defined as twice a zero of the cosine function in the interval [1,2]. The real sine and cosine functions are defined as the real part of the complex sine and complex cosine functions respectively.
More concisely: The sine of (π/2 - x) is equal to the cosine of x for all real numbers x.
|
Complex.sin_pi_div_two
theorem Complex.sin_pi_div_two : (↑Real.pi / 2).sin = 1
This theorem states that the sine of pi divided by two (or π/2) in the complex numbers is equal to one. In mathematical terms, this translates to the following equation: sin(π/2) = 1. Note that the sine function used here is the complex sine function, defined in terms of the complex exponential function, and π is defined as twice the zero of the cosine function in the interval [1,2]. This theorem aligns with the well-known result from trigonometry in the real numbers.
More concisely: In the complex numbers, the sine of π/2 is equal to 1.
|
Complex.sin_pi
theorem Complex.sin_pi : (↑Real.pi).sin = 0
This theorem states that the sine of pi in the complex plane is zero. To be more precise, when the real number pi, represented as `Real.pi` in Lean, is considered as a complex number (by the coercion `↑Real.pi`), the application of the complex sine function to it (`Complex.sin ↑Real.pi`) results in zero. It utilizes the mathematical concept that the sine of pi is zero in both the real number system and the complex number system.
More concisely: The complex sine function evaluates to zero at the real number pi. (`Complex.sin ↑Real.pi = 0`)
|
Complex.sin_antiperiodic
theorem Complex.sin_antiperiodic : Function.Antiperiodic Complex.sin ↑Real.pi
The theorem `Complex.sin_antiperiodic` states that the complex sine function is antiperiodic with an antiperiod equal to the real number π. This means that for every complex number `x`, the value of `Complex.sin` at `x + π` is the negative of its value at `x`, i.e., `Complex.sin (x + π) = -Complex.sin x`.
More concisely: The complex sine function is antiperiodic with a period of π, i.e., `Complex.sin (x + π) = -Complex.sin x` for all complex numbers `x`.
|
Real.sq_sin_pi_div_three
theorem Real.sq_sin_pi_div_three : (Real.pi / 3).sin ^ 2 = 3 / 4
This theorem states that the square of the sine of π divided by 3, i.e., sin²(π/3), is equal to 3/4. This is a common trigonometric identity that might be more convenient to use than the result for cosine in certain situations.
More concisely: sin^2(π/3) = 3/4.
|
Real.sin_pi_div_six
theorem Real.sin_pi_div_six : (Real.pi / 6).sin = 1 / 2
This theorem states that the sine of π/6 is equal to 1/2. In other words, if you take the mathematical constant pi (π), divide it by 6, and then take the sine of that result, you will get the value 1/2.
More concisely: sin(π/6) = 1/2
|
Real.cos_periodic
theorem Real.cos_periodic : Function.Periodic Real.cos (2 * Real.pi)
The theorem `Real.cos_periodic` states that the real cosine function `Real.cos` is periodic with a period of `2 * Real.pi`. In mathematical terms, this means for all real numbers `x`, `Real.cos (x + 2 * Real.pi) = Real.cos x`. This mirrors the well-known property of the cosine function in trigonometry, where the function repeats its values every `2π` intervals.
More concisely: The real cosine function is periodic with a period of 2π, i.e., Real.cos(x + 2π) = Real.cos(x) for all real numbers x.
|
Real.sin_eq_zero_iff
theorem Real.sin_eq_zero_iff : ∀ {x : ℝ}, x.sin = 0 ↔ ∃ n, ↑n * Real.pi = x
This theorem states that for every real number 'x', the sine of 'x' equals to zero if and only if 'x' equals 'n' times pi, where 'n' is an integer. In mathematical terms, `sin(x) = 0` if and only if `x = nπ`, ∀ `n ∈ Z`, where 'Z' is the set of all integers.
More concisely: The sine function equals zero if and only if the argument is an integer multiple of pi.
|