Real.smoothTransition.one_of_one_le
theorem Real.smoothTransition.one_of_one_le : ∀ {x : ℝ}, 1 ≤ x → x.smoothTransition = 1
This theorem states that for any real number 'x', if 'x' is greater than or equal to 1, the value of the infinitely smooth transition function at 'x' is 1. The smooth transition function referred to here is defined such that its value is 0 for all 'x' less than or equal to 0, 1 for 'x' greater than or equal to 1, and between 0 and 1 for 'x' in the open interval (0, 1).
More concisely: For any real number x, the smooth transition function equals 1 if x ≥ 1.
|
expNegInvGlue.tendsto_polynomial_inv_mul_zero
theorem expNegInvGlue.tendsto_polynomial_inv_mul_zero :
∀ (p : Polynomial ℝ), Filter.Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (nhds 0) (nhds 0) := by
sorry
This theorem states that for any real polynomial `p`, the function that maps `x` to the product of the evaluation of `p` at `x⁻¹` and `expNegInvGlue x`, tends to zero at zero. This is to say, as `x` approaches zero, this function value also approaches zero. It can be mathematically represented as: for any real polynomial `P`, the limit as `x` approaches zero of (`P(x⁻¹) * exp(-1/x)`) is zero. The function `exp(-1/x)` is an exponential function that is inverse of `x`, which is zero for `x` less or equal to zero and exponential of `-1/x` for `x` greater than zero.
More concisely: The limit of the product of a real polynomial evaluated at its reciprocal and the inverse exponential function as x approaches 0 is 0.
|
Real.smoothTransition.projIcc
theorem Real.smoothTransition.projIcc : ∀ {x : ℝ}, (↑(Set.projIcc 0 1 ⋯ x)).smoothTransition = x.smoothTransition := by
sorry
The theorem `Real.smoothTransition.projIcc` states that for any real number `x`, applying the `Real.smoothTransition` function to the projection of `x` onto the interval [0, 1] yields the same result as directly applying `Real.smoothTransition` to `x`. This is due to the property of the `Real.smoothTransition` function that it is constant on the intervals $(-∞, 0]$ and $[1, ∞)$. Thus, projecting `x` onto [0, 1] does not change the output of the `Real.smoothTransition` function.
More concisely: For all real numbers x, applying `Real.smoothTransition` to the projection of x onto the interval [0, 1] is equivalent to directly applying `Real.smoothTransition` to x, due to the constant behavior of `Real.smoothTransition` outside the interval [0, 1].
|
expNegInvGlue.nonneg
theorem expNegInvGlue.nonneg : ∀ (x : ℝ), 0 ≤ expNegInvGlue x
The theorem `expNegInvGlue.nonneg` states that the function `expNegInvGlue` is nonnegative for all real numbers. In other words, for every real number `x`, the value of `expNegInvGlue` at `x` is always greater than or equal to zero. This affirms that the function `expNegInvGlue`, which equals `exp(-1/x)` for `x > 0` and `0` for `x ≤ 0`, will never yield a negative result.
More concisely: The theorem `expNegInvGlue.nonneg` asserts that the function `expNegInvGlue` is non-negative for all real numbers, i.e., `expNegInvGlue x ≥ 0` for every `x` in ℝ.
|
expNegInvGlue.contDiff
theorem expNegInvGlue.contDiff : ∀ {n : ℕ∞}, ContDiff ℝ n expNegInvGlue
The theorem `expNegInvGlue.contDiff` states that the function `expNegInvGlue` is smooth. Here, smoothness is defined in terms of being continuously differentiable for all natural numbers `n`, including infinity (`ℕ∞`). This means that the function `expNegInvGlue`, which is defined as `x ↦ exp(-1/x)` for `x > 0` and `0` for `x ≤ 0`, has derivatives of all orders and these derivatives are continuous functions.
More concisely: The function `expNegInvGlue` is continuously differentiable for all natural numbers `n` and at infinity. In other words, it is a smooth function.
|
expNegInvGlue.pos_of_pos
theorem expNegInvGlue.pos_of_pos : ∀ {x : ℝ}, 0 < x → 0 < expNegInvGlue x
The theorem `expNegInvGlue.pos_of_pos` states that the function `expNegInvGlue`, which is defined as $e^{-1/x}$ for $x>0$ and $0$ for $x \leq 0$, is positive on the interval $(0, +\infty)$. In other words, for any real number $x$ that is greater than zero, the value of `expNegInvGlue` at $x$ is also greater than zero.
More concisely: For all $x > 0$, the function `expNegInvGlue` returns a positive real number.
|
Real.smoothTransition.pos_denom
theorem Real.smoothTransition.pos_denom : ∀ (x : ℝ), 0 < expNegInvGlue x + expNegInvGlue (1 - x)
The theorem `Real.smoothTransition.pos_denom` states that for all real numbers `x`, the sum of the function `expNegInvGlue` evaluated at `x` and `1 - x` is always greater than zero. The function `expNegInvGlue` gives the value of exponentiating `-1/x` for `x > 0`, and zero for `x ≤ 0`. This theorem is essentially asserting that the sum of the values of this function at any point and its reflection about `x = 0.5` is always positive, which contributes to the smoothness of the function transition at the junction.
More concisely: For all real numbers x, the sum of expNegInvGlue x and expNegInvGlue (1 - x) is positive.
|
expNegInvGlue.zero_of_nonpos
theorem expNegInvGlue.zero_of_nonpos : ∀ {x : ℝ}, x ≤ 0 → expNegInvGlue x = 0
The theorem `expNegInvGlue.zero_of_nonpos` states that the function `expNegInvGlue` evaluates to zero for all real numbers `x` that are less than or equal to zero. In other words, the function `expNegInvGlue` vanishes on the interval from negative infinity to zero, inclusive.
More concisely: For all real numbers `x ≤ 0`, the function `expNegInvGlue(x) = 0`.
|