not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux
theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : CompleteSpace E] {f : ℝ → E} {g : ℝ → F} {k : Set ℝ} (l : Filter ℝ)
[inst_4 : l.NeBot] [inst_5 : Filter.TendstoIxxClass Set.Icc l l],
k ∈ l →
(∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) →
Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop →
deriv f =O[l] g → ¬MeasureTheory.IntegrableOn g k MeasureTheory.volume
This theorem states that if a real-valued function `f` is eventually differentiable along a nontrivial filter `l` that is generated by convex sets, and the norm of `f` tends to infinity along `l`, and `f' = O(g)` along `l` where `f'` is the derivative of `f`, then the function `g` is not integrable on any set `k` belonging to `l`. This is an auxiliary version of the theorem that assumes the space `E` is complete. In more detail, it takes a set `k` that belongs to the filter `l`, and asserts that if for almost all `x` in `l`, `f` is differentiable at `x`, the norm of `f(x)` tends to infinity as `x` approaches the limit according to `l`, and the derivative of `f` is big O of `g` along `l`, then `g` cannot be integrated over the set `k` with respect to the Lebesgue measure.
More concisely: If a real-valued function `f` is eventually differentiable along a convex nontrivial filter `l` where its norm tends to infinity, and `f' = O(g)` along `l`, then `g` is not integrable on any set in `l` with respect to Lebesgue measure.
|
intervalIntegrable_sub_inv_iff
theorem intervalIntegrable_sub_inv_iff :
∀ {a b c : ℝ}, IntervalIntegrable (fun x => (x - c)⁻¹) MeasureTheory.volume a b ↔ a = b ∨ c ∉ Set.uIcc a b := by
sorry
The theorem `intervalIntegrable_sub_inv_iff` states that for any real numbers `a`, `b`, and `c`, the function `(x - c)⁻¹` is interval integrable on the interval from `a` to `b` (inclusive) under the Lebesgue measure if and only if either `a` equals `b` or `c` is not an element of the closed interval from `a` to `b`. Here, interval integrable means that the function is integrable on both of the intervals `(a, b]` and `(b, a]`, and the Lebesgue measure is a way of assigning a volume or size to certain subsets of the real numbers.
More concisely: The function `(x - c)⁻¹` is interval integrable with respect to Lebesgue measure on `[a, b]` if and only if `a ≠ b` or `c ∉ [a, b]`.
|
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a b c : ℝ},
(∀ᶠ (x : ℝ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℝ f x) →
Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c {c}ᶜ) Filter.atTop →
deriv f =O[nhdsWithin c {c}ᶜ] g → a ≠ b → c ∈ Set.uIcc a b → ¬IntervalIntegrable g MeasureTheory.volume a b
The theorem states that if a function `f` is differentiable in a punctured neighborhood of a point `c` (everywhere near `c` except at `c` itself), and the norm of `f(x)` tends to infinity as `x` approaches `c`, and the derivative of `f` is big O of another function `g` in the punctured neighborhood of `c`, then `g` is not interval integrable on any nontrivial interval `a..b` that includes `c`. In other words, if `f` behaves in this way near `c`, we cannot find a good integral of `g` over an interval containing `c`.
More concisely: If a differentiable function `f` has infinite limit at a point `c`, and its derivative is big O of another function `g` in the punctured neighborhood of `c`, then `g` is not Riemann integrable on any nontrivial interval containing `c`.
|
not_IntegrableOn_Ioi_inv
theorem not_IntegrableOn_Ioi_inv :
∀ {a : ℝ}, ¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ioi a) MeasureTheory.volume
The theorem `not_IntegrableOn_Ioi_inv` states that the function defined by $x \mapsto x^{-1}$ is not integrable on any interval of the form $(a, +\infty)$, where $a$ is a real number. Here, integrability is defined in the sense of the Lebesgue measure (denoted as `MeasureTheory.volume`), i.e., the function is almost everywhere strongly measurable and the integral of its absolute value is finite. The interval $(a, +\infty)$ (denoted as `Set.Ioi a` in Lean) is a set of all real numbers greater than $a$.
More concisely: The function $x \mapsto x^{-1}$ is not integrable with respect to the Lebesgue measure on any interval $(a, +\infty)$ for any real number $a$.
|
intervalIntegrable_inv_iff
theorem intervalIntegrable_inv_iff :
∀ {a b : ℝ}, IntervalIntegrable (fun x => x⁻¹) MeasureTheory.volume a b ↔ a = b ∨ 0 ∉ Set.uIcc a b
The theorem `intervalIntegrable_inv_iff` states that the function `f(x) = x⁻¹` is interval-integrable over the interval from `a` to `b` with respect to the Lebesgue measure if and only if either `a` equals `b` or the number `0` is not contained within the closed interval from `a` to `b`, including the boundaries `a` and `b`. This is because the integrability of the reciprocal function is undefined at `0`.
More concisely: The function `x → x^(-1)` is Lebesgue integrable over the interval `[a, b]` if and only if `a ≠ b`.
|
not_intervalIntegrable_of_sub_inv_isBigO_punctured
theorem not_intervalIntegrable_of_sub_inv_isBigO_punctured :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] {f : ℝ → F} {a b c : ℝ},
(fun x => (x - c)⁻¹) =O[nhdsWithin c {c}ᶜ] f →
a ≠ b → c ∈ Set.uIcc a b → ¬IntervalIntegrable f MeasureTheory.volume a b
The theorem `not_intervalIntegrable_of_sub_inv_isBigO_punctured` states that given any normed additively commutative group `F` and a real-valued function `f`, if the function `f` grows at least as fast as the reciprocal of the distance from a real number `c` in the punctured neighborhood of `c`, then `f` is not interval integrable with respect to the Lebesgue measure on any nontrivial interval `a..b` where `c` lies between `a` and `b` inclusive. Here, the punctured neighborhood of `c` is the set of points arbitrarily close to `c` but not including `c` itself. The growth rate of `f` is measured using Big O notation, which is used to describe the upper bound of the function in question.
More concisely: If a real-valued function `f` on a normed additively commutative group grows at least as fast as the reciprocal of the distance to a point `c` in any nontrivial interval containing `c`, then `f` is not interval integrable with respect to Lebesgue measure at that interval.
|
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a b : ℝ} (l : Filter ℝ) [inst_3 : l.NeBot]
[inst_4 : Filter.TendstoIxxClass Set.Icc l l],
Set.uIcc a b ∈ l →
(∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) →
Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop →
deriv f =O[l] g → ¬IntervalIntegrable g MeasureTheory.volume a b
The theorem states that if a real-valued function `f` is eventually differentiable along a nontrivial filter `l`, which is generated by convex sets, and if the norm of `f` tends to infinity along `l`, then if the derivative of `f` is Big O of another function `g` along `l`, it follows that `g` is not interval-integrable on any interval from `a` to `b`. This holds if the closed interval from `a` to `b` is included in the filter `l`. Here, interval-integrability is taken with respect to the Lebesgue measure. In other words, when the function `f` grows rapidly (its norm tends to infinity) and its derivative is bounded by another function `g` (in the Big O sense) in the long run (as determined by the filter `l`), the function `g` cannot be integrated over any interval that is determined by that filter.
More concisely: If a real-valued function `f` is eventually differentiable along a nontrivial, convex filter `l` such that `|f(x)|` tends to infinity, and `f' = O(g)` along `l`, then `g` is not Lebesgue-integrable on any interval included in `l`.
|
not_IntegrableOn_Ici_inv
theorem not_IntegrableOn_Ici_inv :
∀ {a : ℝ}, ¬MeasureTheory.IntegrableOn (fun x => x⁻¹) (Set.Ici a) MeasureTheory.volume
The theorem `not_IntegrableOn_Ici_inv` states that the function defined by `f(x) = x⁻¹`, or equivalently `1/x`, is not integrable on any interval `[a, +∞)`. In other words, for all real numbers `a`, the integral from `a` to positive infinity of `1/x` does not exist according to the Lebesgue measure, as the integral of its pointwise norm over the interval is infinity.
More concisely: The function `1/x` is not integrable with respect to the Lebesgue measure on any interval `[a, +∞)`.
|
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a b c : ℝ},
a ≠ b →
c ∈ Set.uIcc a b →
(∀ᶠ (x : ℝ) in nhdsWithin c (Set.uIcc a b \ {c}), DifferentiableAt ℝ f x) →
Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c (Set.uIcc a b \ {c})) Filter.atTop →
deriv f =O[nhdsWithin c (Set.uIcc a b \ {c})] g → ¬IntervalIntegrable g MeasureTheory.volume a b
If two real numbers `a` and `b` are not equal, and if `c` is in the closed interval between `a` and `b`, and if a function `f` is differentiable in the neighborhood of `c` within the set that is the closed interval from `a` to `b` excluding `c`, and if as `x` approaches `c` within that same set the norm of `f(x)` goes to infinity, and if the derivative of `f` is big O of another function `g` in that same neighborhood, then `g` is not interval integrable on the interval from `a` to `b`.
In other words, this theorem states that under these conditions on `a`, `b`, `c`, `f`, and `g`, we can conclude that `g` is not interval integrable on the interval from `a` to `b`. This conclusion is particularly useful when `f` becomes arbitrarily large near some point and its derivative is asymptotically bounded by `g` near that point.
More concisely: If two real numbers `a` and `b` are not equal, `c` is in the closed interval between `a` and `b`, `f` is differentiable in the neighborhood of `c` excluding `c`, `f(x)` goes to infinity as `x` approaches `c` within the interval `[a, b]`, and the derivative of `f` is big O of `g` in that neighborhood, then `g` is not Riemann integrable on the interval `[a, b]`.
|