intervalIntegral.integral_comp_smul_deriv''
theorem intervalIntegral.integral_comp_smul_deriv'' :
∀ {G : Type u_6} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → G},
ContinuousOn f (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
ContinuousOn f' (Set.uIcc a b) →
ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
This theorem is the change of variables for continuous integrands. Given two real numbers `a` and `b`, functions `f`, `f'`, and `g`, where `f'` is the right-derivative of `f`, the theorem states that if `f` is continuous on the closed interval from `a` to `b`, `f'` exists on the open interval from `a` to `b` (taken as the interval from the minimum of `a` and `b` to the maximum of `a` and `b`), `f'` is also continuous on the closed interval from `a` to `b`, and `g` is continuous on the image of the interval under `f`, then the integral from `a` to `b` of `f'` times the composite function `g ∘ f` equals the integral from `f(a)` to `f(b)` of `g`. That is, the theorem allows us to perform a change of variables under certain conditions, simplifying the integral of a function transform by `f` to the integral of `g` over the new range.
More concisely: If `f` is a continuous function on a closed interval [a, b], `f'` exists and is continuous on the open interval (a, b), and `g` is continuous on the image of [a, b] under `f`, then the integral of `g ∘ f` from `a` to `b` equals the integral of `f'` times `g` over the image of [a, b] under `f`.
|
intervalIntegral.fderiv_integral
theorem intervalIntegral.fderiv_integral :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
ContinuousAt f a →
ContinuousAt f b →
fderiv ℝ (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) (a, b) =
(ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)
The theorem named "Fundamental theorem of calculus-1" states that for a function `f` from the real numbers to a normed additive commutative group `E`, if `f` is interval integrable on the interval `a..b`, `f` is strongly measurable at `a` and `b` with respect to the Lebesgue measure, and `f` is continuous at `a` and `b`, then the Fréchet derivative of the function mapping each pair `(u, v)` to the integral of `f` from `u` to `v` at the point `(a, b)` is equal to the second component of the pair `(u, v)` scaled by the value of `f` at `b`, minus the first component of the pair scaled by the value of `f` at `a`. This theorem can be viewed as a precise mathematical expression of the first part of the fundamental theorem of calculus, which relates the derivative of an integral of a function to the original function.
More concisely: The Fundamental theorem of calculus-1 states that the derivative of the function mapping an interval to the integral of a continuous, strongly measurable, and interval integrable function equals the scaled difference between the integral's upper and lower bounds.
|
intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le
theorem intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le :
∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
a ≤ b →
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
(∀ x ∈ Set.Ioo a b, g' x ≤ φ x) → g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
This theorem, called the "hard part of the Fundamental Theorem of Calculus (FTC-2) for integrable derivatives with real-valued functions", states the following:
Given functions `g`, `g'`, and `φ` from real numbers to real numbers, and real numbers `a` and `b` such that `a` is less than or equal to `b`, if the following conditions hold:
1. `g` is continuous on the closed interval from `a` to `b` (denoted as `[a, b]` or `Set.Icc a b` in Lean),
2. `g'` is the derivative of `g` at every point in the open interval `(a, b)` (denoted as `Set.Ioo a b` in Lean) and is less than or equal to `φ` at every point in the same open interval,
3. `φ` is integrable (in the sense of Lebesgue integration) on the closed interval `[a, b]`
then the difference of the values of `g` at `b` and `a` (i.e., `g b - g a`) is less than or equal to the integral of `φ` over the closed interval `[a, b]`.
This theorem is an auxiliary lemma used in the proof of the statement `integral_eq_sub_of_hasDeriv_right_of_le`. It extends FTC-2 to the case where the derivative `g'` is not necessarily integrable, but is dominated by an integrable function `φ`.
More concisely: If a real-valued function `g` is continuous on a closed interval `[a, b]`, has a derivative `g'` that is less than or equal to an integrable function `φ` on the open interval `(a, b)`, then `g(b) - g(a) ≤ ∫[a, b] φ(x) dx`.
|
Continuous.deriv_integral
theorem Continuous.deriv_integral :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ℝ → E),
Continuous f → ∀ (a b : ℝ), deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b
The theorem is a statement of the first part of the Fundamental Theorem of Calculus for a real-valued function continuous over its domain. It states that if we have a real-valued function `f` which is continuous, then the derivative of the function `u ↦ ∫ x in a..u, f x` at a point `b` is equal to the value of the function `f` at `b`. In other words, the rate of change of the area under the curve of `f` from `a` to `b` is just the value of `f` at `b`. This is essentially the link between the integral (area under the curve) of a function and its derivative.
More concisely: The derivative of the function `u ↦ ∫ x in a..u, f x with respect to `u` at a point `b` equals `f`(`b`).
|
intervalIntegral.FTCFilter.finiteAt_inner
theorem intervalIntegral.FTCFilter.finiteAt_inner :
∀ {a : ℝ} (l : Filter ℝ) {l' : Filter ℝ} [h : intervalIntegral.FTCFilter a l l'] {μ : MeasureTheory.Measure ℝ}
[inst : MeasureTheory.IsLocallyFiniteMeasure μ], μ.FiniteAtFilter l'
This theorem states that for any real number `a` and any pair of filters `l` and `l'` on the real numbers, such that `l'` is the Future Time Control (FTC) filter of `l` at `a`, and given a locally finite measure `μ`, the measure `μ` is finite at the filter `l'`. In other words, there exists some set `s` in the filter `l'` such that the measure of `s` is less than infinity. This theorem is a result from the area of real analysis, specifically the Fundamental Theorem of Calculus (FTC) in the context of measure theory.
More concisely: Given a real number `a`, a filter `l` on the real numbers, and assuming `l'` is the FTC filter of `l` at `a`, for any locally finite measure `μ`, there exists a set `s` in `l'` with finite measure `μ(s)`.
|
intervalIntegral.integral_eq_sub_of_hasDerivAt
theorem intervalIntegral.integral_eq_sub_of_hasDerivAt :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f f' : ℝ → E}
{a b : ℝ},
(∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
This is a formulation of the Fundamental Theorem of Calculus, Part 2. The theorem states that if a function `f : ℝ → E` has a derivative at every point in the closed interval `[a, b]` and this derivative function `f'` is interval integrable on `[a, b]`, then the integral of `f'` on the interval from `a` to `b` is equal to the difference `f(b) - f(a)`. Here, `E` is a complete normed space over the real numbers (`ℝ`). This theorem connects the concept of differentiability and integrability, showing that the integral of the derivative recovers the original function (up to a constant).
More concisely: If a real-valued function `f` on a closed interval `[a, b]` is differentiable with integrable derivative, then the integral of `f'` over `[a, b]` equals `f(b) - f(a)`.
|
intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left
theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
{f : ℝ → E} {c : E} {la la' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ}
[inst_3 : intervalIntegral.FTCFilter a la la'],
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f la' MeasureTheory.volume →
Filter.Tendsto f (la' ⊓ MeasureTheory.volume.ae) (nhds c) →
Filter.Tendsto u lt la →
Filter.Tendsto v lt la →
(fun t => ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)
The Fundamental Theorem of Calculus-1 states that, if a function `f` is measurable and integrable on an interval from `a` to `b`, `(la, la')` forms an `intervalIntegral.FTCFilter` pair around `a`, and `f` has a finite limit `c` almost surely at `la'`, then the difference of the integrals from `v` and `u` to `b`, plus the quantity `(v - u)` scaled by `c`, is little o of `(v - u)` as `u` and `v` tend to `la`. This is the case if `f` is strongly measurable with respect to `la'` and volume measure, `f` tends to `c` at the intersection of `la'` and volume measure's almost everywhere, and both `u` and `v` tend to `la` with `lt` filter. This statement is about the strict differentiability at `la` filter in both endpoints. It could have been formulated using `HasStrictDerivAtFilter` if such a definition existed.
More concisely: If a function `f` is measurable and integrable on an interval `[a, b]`, `f` has a finite limit `c` almost everywhere at `a`, and `f` is strongly measurable and tends to `c` at `a` with respect to volume measure, then the integral from `a` to `b` of `f` is approximately equal to `c` times the length of the interval, up to an error that is little o of the interval length as the interval shrinks to `a`.
|
intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae
theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
{f : ℝ → E} {ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {ua ub va vb : ι → ℝ}
[inst_3 : intervalIntegral.FTCFilter a la la'] [inst_4 : intervalIntegral.FTCFilter b lb lb'],
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f la' MeasureTheory.volume →
StronglyMeasurableAtFilter f lb' MeasureTheory.volume →
Filter.Tendsto f (la' ⊓ MeasureTheory.volume.ae) (nhds ca) →
Filter.Tendsto f (lb' ⊓ MeasureTheory.volume.ae) (nhds cb) →
Filter.Tendsto ua lt la →
Filter.Tendsto va lt la →
Filter.Tendsto ub lt lb →
Filter.Tendsto vb lt lb →
(fun t =>
((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) -
((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt]
fun t => ‖va t - ua t‖ + ‖vb t - ub t‖
This is the "Fundamental Theorem of Calculus-1", stating the strict differentiability at a filter in both endpoints. The theorem states that if `f` is a measurable function which is interval integrable on `a..b`, `(la, la')` is a filter pair around `a`, `(lb, lb')` is a filter pair around `b`, and `f` has finite limits `ca` and `cb` almost surely at `la'` and `lb'` respectively, then the difference of integral of `f` in `va..vb` and integral of `f` in `ua..ub` is equal to the difference of the scaled limit values `cb` and `ca` plus a small-o term accounting for the change in `ua`, `va`, `ub` and `vb` as `ua` and `va` tend to `la` while `ub` and `vb` tend to `lb`. The theorem emphasizes on the conditions under which the change in the integral of a function over an interval is approximately linear with respect to the length of the interval.
More concisely: If a measurable, interval integrable function `f` has finite limits at the endpoints of an interval `[a, b]`, then the difference of the integrals of `f` over subintervals with endpoints approaching `a` and `b`, respectively, is equal to the difference of the limit values plus an error term that approaches zero as the lengths of the subintervals approach zero.
|
intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae
theorem intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{ca cb : E} {la lb : Filter ℝ} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) la]
[inst_4 : intervalIntegral.FTCFilter b (nhdsWithin b t) lb],
StronglyMeasurableAtFilter f la MeasureTheory.volume →
StronglyMeasurableAtFilter f lb MeasureTheory.volume →
Filter.Tendsto f (la ⊓ MeasureTheory.volume.ae) (nhds ca) →
Filter.Tendsto f (lb ⊓ MeasureTheory.volume.ae) (nhds cb) →
HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x)
((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca)
(s ×ˢ t) (a, b)
This theorem states that for a measurable function `f` which is interval integrable over `a..b`, the function `(u, v) ↦ ∫ x in u..v, f x` has a derivative `(u, v) ↦ v • cb - u • ca` within a product of sets `s × t` at the point `(a, b)`, where `s` belongs to the set `{Iic a, {a}, Ici a, univ}` and `t` belongs to the set `{Iic b, {b}, Ici b, univ}`. This is provided that `f` tends to `ca` and `cb` almost surely at the filters `la` and `lb`, respectively. The specific filters `la` and `lb` are chosen based on the values of `s` and `t` according to a given table. For example, if `s` is `Iic a` (the set of all numbers less than or equal to `a`), then `la` is `𝓝[≤] a` (the neighborhood filter of `a` for nonstrictly decreasing sequences), and so on for other possible values of `s` and `t`.
More concisely: Under certain measurability and integrability conditions, the function defined by `(u, v) ↦ ∫ x in u..v, f x` has a derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` for `s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}`, where `f` converges almost surely to `ca` at the filter `la` and `cb` at the filter `lb`.
|
intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right
theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
Filter.Tendsto f (nhds b ⊓ MeasureTheory.volume.ae) (nhds c) →
HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
The theorem, "Fundamental theorem of calculus-1, strict differentiability at the right endpoint", states that given a function `f : ℝ → E` that is interval integrable over `a..b`, and if `f(x)` has a limit `c` almost everywhere at `b`, then the function `u ↦ ∫ x in a..u, f x` has a derivative `c` at `b` in the sense of strict differentiability. In other words, if the function `f` is integrable within the interval `a..b` and converges strongly to `c` at `b`, the indefinite integral of `f` from `a` to `u` has a strict derivative of `c` at `b`.
More concisely: If a real-valued function `f` is integrable over the interval `[a, b]` and has a limit `c` at `b`, then the function `F(x) = ∫[a, x], f(t) dt` is strictly differentiable at `x = b` with derivative `c`.
|
intervalIntegral.integral_hasDerivWithinAt_left
theorem intervalIntegral.integral_hasDerivWithinAt_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
ContinuousWithinAt f t a → HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) s a
The Fundamental Theorem of Calculus is stated as follows: If `f` is a function from real numbers to a normed and complete additive commutative group `E`, and `f` is interval integrable (integrable on both intervals `(a, b]` and `(b, a]`) with respect to the Lebesgue measure between real numbers `a` and `b`, then for `s` and `t` as subsets of real numbers (where `s` and `t` are sets within the neighbourhood of `a`), the function `u ↦ ∫ x in u..b, f x` has a derivative within `s` at `a` (either from the left or the right), with the derivative being `-f a` at `a`. This holds under the conditions that `f x` is strongly measurable at a filter `t` within the neighbourhood of `a` with respect to the restricted Lebesgue measure and `f x` is continuous at `a` within `t`.
More concisely: If a real-valued function `f` is interval integrable and continuous at `a` with strongly measurable derivatives `-f(a)` at `a` for both the left and right limits, then the function `x ↦ ∫(a, x) f(t) dt` has these values as derivatives.
|
intervalIntegral.integral_hasFDerivAt_of_tendsto_ae
theorem intervalIntegral.integral_hasFDerivAt_of_tendsto_ae :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{ca cb : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
Filter.Tendsto f (nhds a ⊓ MeasureTheory.volume.ae) (nhds ca) →
Filter.Tendsto f (nhds b ⊓ MeasureTheory.volume.ae) (nhds cb) →
HasFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x)
((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca)
(a, b)
The **Fundamental Theorem of Calculus-1** states that if a function `f : ℝ → E` is interval integrable on `a..b`, and if `f x` has finite limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then the function `(u, v) ↦ ∫ x in u..v, f x` has a derivative at `(a, b)` given by `(u, v) ↦ v • cb - u • ca`. Here, `E` is a normed commutative additive group, `ca` and `cb` are the limits of `f` at `a` and `b`, `a` and `b` are real numbers, and `f` is strongly measurable at filters `nhds a` and `nhds b` with respect to the Lebesgue measure. The derivative is expressed as the difference of two continuous linear maps, the second map multiplied by `cb` and the first map multiplied by `ca`.
More concisely: The Fundamental Theorem of Calculus-1 states that under certain conditions on a function `f` and the limits of `f` at the endpoints `a` and `b`, the function defined by integrating `f` over an interval `[u, v]` has a derivative equal to `(v - u) * cb - (u - a) * ca`, where `ca` and `cb` are the limits of `f` at `a` and `b`, respectively.
|
intervalIntegral.integral_hasStrictDerivAt_right
theorem intervalIntegral.integral_hasStrictDerivAt_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
ContinuousAt f b → HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
The **Fundamental Theorem of Calculus-1**, in the context of strict differentiability at the right endpoint, asserts that if a function `f : ℝ → E` (where `E` is a normed and complete additive commutative group) is interval integrable on `a..b` and `f` is continuous at `b`, then the function `u ↦ ∫ x in a..u, f x` has a strict derivative at `b` which is `f b`. This theorem is a cornerstone of calculus, linking the concept of an integral to the derivative of the function. It provides the rigorous foundation for the process of finding antiderivatives by integrating a function.
More concisely: If a function `f : ℝ → E` is continuous at `b` and interval integrable on `a..b` (where `E` is a normed and complete additive commutative group), then the definite integral `∫ x in a..b, f x` has a strict derivative at `b` equal to `f b`.
|
intervalIntegral.integral_comp_mul_deriv
theorem intervalIntegral.integral_comp_mul_deriv :
∀ {a b : ℝ} {f f' g : ℝ → ℝ},
(∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
ContinuousOn f' (Set.uIcc a b) →
Continuous g → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x
This theorem, often referred to as the "change of variables" theorem, states the following: Given real numbers `a` and `b`, functions `f`, `f'`, and `g` from real numbers to real numbers, if `f` has a continuous derivative `f'` on the interval including `a` and `b`, and if `f'` is continuous on the same interval, and `g` is continuous, then the integral from `a` to `b` of the function composed of `g` and `f` times `f'` is equal to the integral from `f(a)` to `f(b)` of `g`. In mathematical terms, this theorem is saying:
\[ \int_a^b (g \circ f)(x) \cdot f'(x) \, dx = \int_{f(a)}^{f(b)} g(u) \, du \]
This theorem essentially allows for the substitution of the variable of integration in an integral.
More concisely: The Change of Variables theorem asserts that if `f` is a function with a continuous derivative on an interval, and `g` is a continuous function, then the integral of `g` composed with `f` times `f'` from `a` to `b` equals the integral of `g` from `f(a)` to `f(b)`.
|
intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left
theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
Filter.Tendsto f (nhds a ⊓ MeasureTheory.volume.ae) (nhds c) →
HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
This theorem is a version of the Fundamental Theorem of Calculus (part 1), with strict differentiability at the left endpoint.
In particular, if a function `f : ℝ → E` is interval integrable on an interval `a..b`, and the function `f` at `x` approaches a finite limit `c` almost surely as `x` approaches `a`, then the function `u ↦ ∫ x in u..b, f x` has a derivative of `-c` at `a`, in the sense of strict differentiability. This means that as `u` tends to `a`, the change in the integral of `f` from `u` to `b` approximates `-c` times the change in `u`, plus a term that goes to zero faster than the change in `u`. In addition, `f` needs to be strongly measurable at the filter on `a`, which means that it is almost everywhere strongly measurable with respect to the restriction of the measure to some set in the filter.
More concisely: If a strongly measurable, interval integrable function `f : ℝ → E` on the interval `a..b` has a left-endpoint limit `c` at `a`, then the function `u ↦ ∫ x in u..b, f x` is strictly differentiable at `a` with derivative `-c`.
|
intervalIntegral.integral_eq_sub_of_hasDeriv_right
theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f f' : ℝ → E}
{a b : ℝ},
ContinuousOn f (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
Theorem `intervalIntegral.integral_eq_sub_of_hasDeriv_right` is the second part of the Fundamental Theorem of Calculus. It states that if a function `f` mapping real numbers to a normed and complete space `E` is continuous on the closed interval `[a, b]` and has a right derivative `f'` at every point within the open interval `(a, b)`, and if this derivative `f'` is interval integrable on `[a, b]`, then the integral of `f'` over the interval from `a` to `b` is equal to the difference `f(b) - f(a)`. This theorem essentially links the concept of derivatives and definite integrals.
More concisely: If a continuous function `f` with a right-continuous derivative on a closed interval `[a, b]`, and its derivative is integrable on `[a, b]`, then `∫[a, b] f'(x) dx = f(b) - f(a)`.
|
intervalIntegral.integral_comp_smul_deriv'
theorem intervalIntegral.integral_comp_smul_deriv' :
∀ {G : Type u_6} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → G},
(∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
ContinuousOn f' (Set.uIcc a b) →
ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
This theorem, known as the Change of Variables theorem, states that if you have a function `f` with a continuous derivative `f'` on the interval `[a, b]` and another function `g` that is continuous on the image of `f` over the interval `[a, b]`, then you can perform a variable substitution `u = f x`. This transforms the integral of `f' x * (g ∘ f) x` with respect to `x` over the interval `[a, b]` into the integral of `g u` with respect to `u` over the interval `[f a, f b]`. Compared to the `intervalIntegral.integral_comp_smul_deriv` theorem, this version only requires that the function `g` be continuous on the image of `f` over the interval `[a, b]`.
More concisely: If `f` is a differentiable function with continuous derivative on an interval `[a, b]` and `g` is a continuous function on the image of `f` over `[a, b]`, then the integral of `g(f(x)) * f'(x)` with respect to `x` over `[a, b]` equals the integral of `g(u)` with respect to `u` over `[f(a), f(b)]`.
|
intervalIntegral.integral_comp_smul_deriv
theorem intervalIntegral.integral_comp_smul_deriv :
∀ {G : Type u_6} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → G},
(∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
ContinuousOn f' (Set.uIcc a b) →
Continuous g → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
This theorem, named `intervalIntegral.integral_comp_smul_deriv`, is a version of the change of variables formula in calculus, specifically for definite integrals. It states that if a function `f` has a continuous derivative `f'` on the closed interval from `a` to `b`, and if another function `g` is continuous, then we can change the variable of integration using `f`. More formally, the integral from `a` to `b` of `f'(x)` times `(g ∘ f)(x)` (where `∘` denotes composition of functions) is equal to the integral from `f(a)` to `f(b)` of `g(x)`. The conditions of the theorem ensure that the required integrals exist and the change of variables is valid.
More concisely: If `f:` [a, b] → ℝ is continuously differentiable and `g:` ℝ → ℝ is continuous, then ∫[a, b] `f'`(x) (*g) (x) dx = ∫(f(a) to f(b)) `g`(x) dx.
|
intervalIntegral.integral_hasStrictFDerivAt
theorem intervalIntegral.integral_hasStrictFDerivAt :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
ContinuousAt f a →
ContinuousAt f b →
HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x)
((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a))
(a, b)
The theorem, named as "Fundamental theorem of calculus-1", states that if a real-valued function `f` is interval integrable over an interval `a` to `b` and `f` is continuous at both `a` and `b`, then the function `(u, v) ↦ ∫ x in u..v, f x`, which maps a pair of real numbers `(u, v)` to the integral of `f` over the interval `u` to `v`, has a strict derivative at the point `(a, b)`. The derivative at `(a, b)` is given by `(u, v) ↦ v • cb - u • ca`, where `cb` and `ca` are the values of `f` at `b` and `a` respectively. This derivative is computed in terms of continuous linear maps, specifically the second and first component functions with respect to scalar multiplication by `f(b)` and `f(a)` respectively.
More concisely: If a real-valued function that is continuous and interval integrable over an interval with integrable opposite endpoints has a continuous antiderivative, then the function mapping an interval to its definite integral is differentiable at that interval with derivative given by the product of the length of the interval and the difference of the function values at the endpoints.
|
intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f f' : ℝ → E}
{a b : ℝ},
a ≤ b →
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
The "Fundamental theorem of calculus-2" states: Suppose `f` is a function from real numbers to type `E` (where `E` has a normed addition group structure, normed space structure over real numbers, and is a complete space). Now, if `f` is continuous on the closed interval `[a, b]` (where `a` is less than or equal to `b`) and has a right derivative `f'` at every point `x` in the open interval `(a, b)`, and if `f'` is interval integrable on the interval `[a, b]` with respect to the Lebesgue measure, then the integral of `f'` from `a` to `b` equals `f(b) - f(a)`. This implies that the area under the curve of the derivative function `f'` between `a` and `b` equals the difference in function values of `f` at `b` and `a`.
More concisely: If a real-valued function `f` on the interval `[a, b]` is continuous, has a right derivative at every point in `(a, b)`, and its derivative is Lebesgue integrable on `[a, b]`, then the definite integral of `f'` equals `f(b) - f(a)`.
|
intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left
theorem intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
Filter.Tendsto f (nhdsWithin a t ⊓ MeasureTheory.volume.ae) (nhds c) →
HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) s a
The theorem, named "intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left", is a statement of the Fundamental Theorem of Calculus. Specifically, it states that if a function `f : ℝ → E` is interval integrable on an interval from `a` to `b` and `f(x)` tends to a finite limit `c` almost surely as `x` approaches `a` from the right or the left, then the function `u ↦ ∫ x in u..b, f x` has a derivative at `a` within a certain subset, where the derivative is `-c`. This holds for any real numbers `a` and `b`, where `E` is a normed group over reals that is also a complete space. The subsets used for the neighborhood of `a` and the limit of `f(x)` as `x` approaches `a` also satisfy some conditions related to the filter generated by intervals around `a`.
More concisely: If a function `f : ℝ → E` is interval integrable on `[a, b]` and `f(x)` tends to a finite limit `c` as `x` approaches `a` from the right or left, then the function `x ↦ ∫ x in a..b, f x` has a derivative at `a` within the subset of `a` where the limit of `f` exists, and that derivative is equal to `-c`.
|
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge'
theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c : E}
{l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [inst_2 : CompleteSpace E]
[inst_3 : l'.IsMeasurablyGenerated] [inst_4 : Filter.TendstoIxxClass Set.Ioc l l'],
StronglyMeasurableAtFilter f l' μ →
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
μ.FiniteAtFilter l' →
Filter.Tendsto u lt l →
Filter.Tendsto v lt l →
lt.EventuallyLE v u →
(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + (↑↑μ (Set.Ioc (v t) (u t))).toReal • c) =o[lt] fun t =>
(↑↑μ (Set.Ioc (v t) (u t))).toReal
This theorem is a local version of the Fundamental Theorem of Calculus-1 for any measure. It states that for any ι-type filters `l` and `l'` related by the `TendstoIxxClass Ioc` relation, if a real-valued function `f` has a finite limit `c` at the filter intersection of `l` and `μ.ae`, where `μ` is a measure finite at `l`, then the integral of `f` from `u` to `v` with respect to `μ` is equivalent to `-μ (Ioc v u) • c + o(μ(Ioc v u))` as both `u` and `v` tend to `l` such that `v ≤ u`. We thus have an asymptotic relationship between the integral of `f` and the measure of the interval `(v,u)`. The conditions include strong measurability of `f` at the filter `l'` with respect to `μ`, convergence of `f` to `c` at the intersection of `l'` and `μ.ae`, finiteness of `μ` at `l'`, and the convergence of `u` and `v` to `l` under the filter `lt`, with `v` eventually being less than or equal to `u` under `lt`.
More concisely: For measures `μ` and filters `l` and `l'` related by `TendstoIxxClass Ioc`, if `f` is a real-valued function strongly measurable at `l'` with respect to `μ`, convergent to `c` at the intersection of `l'` and `μ.ae`, and `μ` is finite at `l'`, then the integral of `f` from `u` to `v` with respect to `μ` is asymptotically equivalent to `-μ (Ioc v u) • c + o(μ(Ioc v u))` as `u` and `v` tend to `l` with `v ≤ u`.
|
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae'
theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c : E}
{l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [inst_2 : l'.IsMeasurablyGenerated]
[inst_3 : Filter.TendstoIxxClass Set.Ioc l l'],
StronglyMeasurableAtFilter f l' μ →
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
μ.FiniteAtFilter l' →
Filter.Tendsto u lt l →
Filter.Tendsto v lt l →
(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
∫ (x : ℝ) in u t..v t, 1 ∂μ
This is the local version of the Fundamental Theorem of Calculus-1, applicable to any measure. Given two filters `l` and `l'` associated by the class `TendstoIxxClass Ioc`, and a function `f` that has a finite limit `c` at the meet of `l'` and `μ.ae` (where `μ` is a measure finite at `l'`), the theorem states that the difference between the integral of `f` and the integral of the constant function `c` over the interval `u..v` is little-o of the integral of the constant function `1` over the same interval as `u` and `v` both tend to `l`. Additional assumptions include that `f` is strongly measurable at the filter `l'` with respect to measure `μ`, the function `f` tends to `c` at the meet of `l'` and `μ.ae`, the measure `μ` is finite at filter `l'`, and both `u` and `v` tend to filter `l` as `t` tends to infinity. This theorem is often used in applications that involve switching the order of limit and integral operations.
More concisely: Given filters `l` and `l'` related by `TendstoIxxClass Ioc`, a finite limit `c` of measurable function `f` at `l'` with respect to measure `μ`, and `μ` finite at `l'`, if `f` tends to `c` at `l'` and `μ.ae`, then `∫(f - c) ds is little-o of ∫(1) ds` as `s` tends to `l`.
|
intervalIntegral.deriv_integral_of_tendsto_ae_right
theorem intervalIntegral.deriv_integral_of_tendsto_ae_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
Filter.Tendsto f (nhds b ⊓ MeasureTheory.volume.ae) (nhds c) →
deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = c
This theorem is a version of the Fundamental Theorem of Calculus. It states that if `f : ℝ → E` is a function that is interval integrable on an interval `a..b` and the limit of `f` is a finite value `c` almost surely at `b`, then the derivative of the function `u ↦ ∫ x in a..u, f x` at point `b` equals `c`. Here, `E` is a normed add commutative group with a normed space structure over the real numbers ℝ and is also a complete space. The limit of `f` at `b` is taken with respect to the neighborhood filter at `b` intersected with the almost everywhere filter of the Lebesgue measure.
More concisely: If `f : ℝ → E` is an interval integrable function on `a..b` with `E` being a complete normed add commutative group, and `f` has a finite limit `c` almost surely at `b`, then `(d/dx) (x ↦ ∫ t in a..x, f t) = c` at `x = b`.
|
intervalIntegral.integrableOn_deriv_of_nonneg
theorem intervalIntegral.integrableOn_deriv_of_nonneg :
∀ {g' g : ℝ → ℝ} {a b : ℝ},
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioo a b, 0 ≤ g' x) → MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume
The theorem `intervalIntegral.integrableOn_deriv_of_nonneg` states that if a real function `g` is continuous on a closed interval `[a, b]` and has a derivative `g'` at each point in the open interval `(a, b)`, and if this derivative `g'` is nonnegative on `(a, b)`, then `g'` is integrable on the half-open interval `(a, b]` with respect to the Lebesgue measure. Essentially, if the derivative of a function is nonnegative in an interval, then the derivative is integrable over that interval.
More concisely: If a real-valued function `g` is continuous on a closed interval `[a, b]`, has a nonnegative derivative `g'` on the open interval `(a, b)`, then `g'` is integrable on the half-open interval `(a, b]` with respect to Lebesgue measure.
|
intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae
theorem intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{ca cb : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
Filter.Tendsto f (nhds a ⊓ MeasureTheory.volume.ae) (nhds ca) →
Filter.Tendsto f (nhds b ⊓ MeasureTheory.volume.ae) (nhds cb) →
HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x)
((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca)
(a, b)
This is the first part of the Fundamental Theorem of Calculus, concerning strict differentiability at both endpoints. The theorem states that if we have a function `f` mapping real numbers to a normed additive commutative group `E`, and if `f` is interval integrable on an interval from `a` to `b`, and if `f` has finite limits `ca` and `cb` almost everywhere as it approaches `a` and `b` respectively, then the function which maps a pair `(u, v)` to the integral of `f` from `u` to `v`, has a derivative at `(a, b)` which is given by `(u, v) ↦ v * cb - u * ca`. This derivative is strictly differentiable, meaning it exists and is unique. The conditions of strong measurability at the filters around `a` and `b`, and the tendency of `f` to approach `ca` and `cb` almost everywhere as it approaches `a` and `b` respectively, are needed to ensure the existence and uniqueness of this derivative.
More concisely: The first part of the Fundamental Theorem of Calculus asserts that the function mapping a pair of real numbers `(u, v)` to the integral of a strict differentiable function `f` from `u` to `v`, with finite limits `ca` and `cb` at `a` and `b`, has a strictly differentiable derivative equal to `(u, v) ↦ v * cb - u * ca`.
|
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'
theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c : E}
{l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [inst_2 : CompleteSpace E]
[inst_3 : l'.IsMeasurablyGenerated] [inst_4 : Filter.TendstoIxxClass Set.Ioc l l'],
StronglyMeasurableAtFilter f l' μ →
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
μ.FiniteAtFilter l' →
Filter.Tendsto u lt l →
Filter.Tendsto v lt l →
lt.EventuallyLE u v →
(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - (↑↑μ (Set.Ioc (u t) (v t))).toReal • c) =o[lt] fun t =>
(↑↑μ (Set.Ioc (u t) (v t))).toReal
This is a local version of the **Fundamental Theorem of Calculus-1** for any measure. It states that given a normed group `E` and filters `l` and `l'` related by `TendstoIxxClass Ioc`, if a function `f` has a finite limit `c` at the intersection of `l` and the almost everywhere filter with respect to a measure `μ` that is finite at `l`, then the integral of `f` over the interval `[u,v]` with respect to `μ` is equal to the measure of the interval `(u, v]` times `c` plus a term that is little o of the measure of the interval `(u, v]` as both `u` and `v` tend to `l` in such a way that `u` is less than or equal to `v`. This theorem is specifically useful when `l` is one of the neighborhood filters at `a`: `𝓝[≥] a`, `𝓝[≤] a`, `𝓝 a`. The primed version also works for cases like `l = l' = Filter.atTop`.
More concisely: Given a normed group `E`, a measure `μ` on `E`, and a function `f` with finite limits at the intersection of filters `l` and `l'` related by `TendstoIxxClass Ioc`, if `f` is integrable with respect to `μ` on every interval `[u, v]` with `u` and `v` in `l`, then the integral of `f` over `[u, v]` is equal to the measure of `(u, v]` times the limit `c` of `f` plus an infinitesimal of order less than the measure of `(u, v]`.
|
intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right
theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
{f : ℝ → E} {c : E} {lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ}
[inst_3 : intervalIntegral.FTCFilter b lb lb'],
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f lb' MeasureTheory.volume →
Filter.Tendsto f (lb' ⊓ MeasureTheory.volume.ae) (nhds c) →
Filter.Tendsto u lt lb →
Filter.Tendsto v lt lb →
(fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)
This is a version of the first part of the Fundamental Theorem of Calculus, considering strict differentiability at filter for both endpoints of an interval. The theorem is as follows:
Given a function `f` which is a measurable and interval integrable on `a..b`, a pair `(lb, lb')` which forms an `intervalIntegral.FTCFilter` around `b`, and a finite limit `c` for `f` which it almost surely approaches at `lb'`. Then, as `u` and `v` tend to `lb`, the difference between the integrals of `f` from `a` to `v` and `a` to `u`, subtracted from the scalar multiplication of `(v - u)` and `c`, is little-o of `‖v - u‖`. In other words,
\[ ((\int_{a}^{v} f(x) dx) - \int_{a}^{u} f(x) dx) - (v - u) \cdot c = o(\|v - u\|) \]
as `u` and `v` tend to `lb`.
This formulation could've been expressed using `HasStrictDerivAtFilter` if such a definition was available.
More concisely: Given a measurable and interval integrable function `f` on `[a, b]`, a limit `c` of `f` at `b`, and an `intervalIntegral.FTCFilter` pair `(lb, lb')` around `b`, as `u` and `v` approach `lb`, the difference between the Riemann integrals of `f` from `a` to `u` and `a` to `v`, minus the product of `(v - u)` and `c`, is o(||v - u||). That is,
\[ (\int\_a^v f(x) dx - \int\_a^u f(x) dx) - (v - u) \cdot c = o(|v - u|) \]
|
intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right
theorem intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
Filter.Tendsto f (nhds b ⊓ MeasureTheory.volume.ae) (nhds c) →
HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
The theorem, known as the Fundamental Theorem of Calculus-1, states that if a function `f : ℝ → E` is interval-integrable on a given interval `a..b` and the limit of `f(x)` as `x` approaches `b` exists and is equal to a finite value `c` (almost surely), then the function `u ↦ ∫ x in a..u, f x` has a derivative at `b` which is equal to `c`. Here, `ℝ` is the set of real numbers, `E` is a normed add commutative group which is also a normed space over `ℝ`, and `f` is a strongly measurable function at a neighborhood filter of `b` with respect to the Lebesgue measure. The limit of `f` at the intersection of the neighborhood filter of `b` and the set of all Lebesgue measurable sets, is `c`.
More concisely: If a real-valued function `f` is interval-integrable on `[a, b]` with a finite limit `c` as `x` approaches `b`, then the function `F(x) = ∫[a, x], f(t) dt` has a derivative at `x = b` equal to `c`.
|
intervalIntegral.integral_hasFDerivAt
theorem intervalIntegral.integral_hasFDerivAt :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
ContinuousAt f a →
ContinuousAt f b →
HasFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x)
((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a))
(a, b)
The **Fundamental Theorem of Calculus - Part 1** states that if a function `f : ℝ → E` (where `E` is a normed add commutative group with a normed space structure over real numbers and is also a complete space) is interval integrable on `a..b` and `f` is continuous at `a` and `b`, then the function `(u, v) ↦ ∫ x in u..v, f x` (which gives the integral of `f` from `u` to `v`) has a derivative at the point `(a, b)`. This derivative is given by `(u, v) ↦ v • cb - u • ca` (which is a linear map subtracting the product of `u` and the value of `f` at `a` from the product of `v` and the value of `f` at `b`). This theorem is a fundamental result in calculus linking the concept of a derivative with the concept of an integral.
More concisely: If a continuous, real-valued function `f` on an interval `[a, b]` is integrable, then the function that maps an interval `[u, v]` to the integral of `f` from `u` to `v` is differentiable and its derivative is given by the constant function `c = b*f(b) - a*f(a)`.
|
intervalIntegral.integral_unitInterval_deriv_eq_sub
theorem intervalIntegral.integral_unitInterval_deriv_eq_sub :
∀ {𝕜 : Type u_2} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
[inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower ℝ 𝕜 E] {f f' : 𝕜 → E} {z₀ z₁ : 𝕜},
ContinuousOn (fun t => f' (z₀ + t • z₁)) (Set.Icc 0 1) →
(∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)) →
z₁ • ∫ (t : ℝ) in 0 ..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀
This theorem is a variant of the Fundamental Theorem of Calculus, particularly considering the integration over the unit interval. It states that for any type `𝕜` and `E` where `E` is a complete normed group with a normed space structure over real numbers and `𝕜`, and `𝕜` behaves like real numbers and has a normed space structure over `E`. Given two functions `f` and `f'` from `𝕜` to `E`, and two points `z₀` and `z₁` in `𝕜`, if the function `f'` applied to `(z₀ + t • z₁)` is continuous on the closed interval from 0 to 1, and for every `t` in the closed interval from 0 to 1, `f` has derivative `f'` applied to `(z₀ + t • z₁)` at the point `(z₀ + t • z₁)`, then the result of `z₁` scaled by the integral from 0 to 1 of `f'` applied to `(z₀ + t • z₁)` equals the difference of `f` applied to `(z₀ + z₁)` and `f` applied to `z₀`.
More concisely: If `f: 𝕜 -> E` is differentiable on the closed interval [0, 1] with `f'(z₀ + t * z₁)` continuous, then `∫(0, 1) f'(z₀ + t * z₁) dt = f(z₀ + z₁) - f(z₀)`.
|
intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae
theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ}
{ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {ua va ub vb : ι → ℝ}
[inst_2 : intervalIntegral.FTCFilter a la la'] [inst_3 : intervalIntegral.FTCFilter b lb lb']
[inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ],
IntervalIntegrable f μ a b →
StronglyMeasurableAtFilter f la' μ →
StronglyMeasurableAtFilter f lb' μ →
Filter.Tendsto f (la' ⊓ μ.ae) (nhds ca) →
Filter.Tendsto f (lb' ⊓ μ.ae) (nhds cb) →
Filter.Tendsto ua lt la →
Filter.Tendsto va lt la →
Filter.Tendsto ub lt lb →
Filter.Tendsto vb lt lb →
(fun t =>
∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
(∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
fun t => ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖
This is the first part of the Fundamental Theorem of Calculus (FTC-1), for a strictly differentiable function with respect to locally finite measure. Suppose we have a measurable function `f` that is integrable over an interval from `a` to `b`. We also have pairs of FTCFilters `(la, la')` around `a` and `(lb, lb')` around `b`. Assume that `f` has finite limits `ca` and `cb` at filters `la'` and `lb'` intersected with the almost everywhere filter of the measure `μ`, respectively. Then, the difference between the integrals of `f` over the intervals `va..vb` and `ua..ub`, minus the difference between the integrals of `cb` over `ub..vb` and `ca` over `ua..va`, is little-o of the sum of the norms of the integrals of 1 over `ua..va` and `ub..vb`, as `ua`, `va` approach the filter `la` and `ub`, `vb` approach the filter `lb`. This theorem captures the relationship between integration and differentiation, pivotal in calculus.
More concisely: Under the given conditions, the integral of a strictly differentiable function `f` between `a` and `b` equals the difference of the integrals of `f` over subintervals around `a` and `b`, plus the product of the function's limit at `b` and the width of the subinterval around `b`, plus an error term that is little-o of the sum of the integrals of 1 over those subintervals as the lengths approach zero.
|
intervalIntegral.integral_hasDerivAt_left
theorem intervalIntegral.integral_hasDerivAt_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
ContinuousAt f a → HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
The Fundamental Theorem of Calculus-1 states that if a function `f : ℝ → E` is interval integrable on `a..b` (that is, it is integrable on both intervals `(a, b]` and `(b, a]`) and is continuous at `a`, then the function defined by `u ↦ ∫ x in u..b, f x` has a derivative at `a` which is `-f a`. Here, `E` is a normed additively commutative group which is also a normed space over the real numbers and is complete. The function `f` is strongly measurable at a neighborhood filter of `a` with respect to the Lebesgue measure.
More concisely: If a continuous, interval integrable function `f : ℝ → E` on `[a, b]` satisfies the condition that `f` is integrable on both `[a, b]` and `[b, a]`, then the function `u ↦ ∫ x in u..b, f x` has a derivative at `a` equal to `-f a`.
|
intervalIntegral.derivWithin_integral_of_tendsto_ae_right
theorem intervalIntegral.derivWithin_integral_of_tendsto_ae_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
Filter.Tendsto f (nhdsWithin b t ⊓ MeasureTheory.volume.ae) (nhds c) →
autoParam (UniqueDiffWithinAt ℝ s b) _auto✝ → derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = c
The Fundamental Theorem of Calculus (FTC) states that if a function `f` from real numbers to a normed additively commutative group `E` is interval integrable on an interval from `a` to `b`, and if `f(x)` tends to a finite limit `c` almost everywhere as `x` approaches `b` from the right or left, then the right (or left) derivative of the function `u ↦ ∫ x in a..u, f x` at `b` equals `c`. This theorem requires that the function `f` is strongly measurable at filter `nhdsWithin b t` with respect to the volume measure, and that `f` tends to `c` within the intersection of the set `nhdsWithin b t` and the set of almost everywhere points with respect to the volume measure. The theorem also assumes that every tangent vector to `ℝ` at `b` within `s` is unique.
More concisely: If a real-valued function `f` is interval integrable on an interval `[a, b]` and has a right (or left) limit `c` at `b`, then the function `u ↦ ∫ x in a..u, f x` has a right (or left) derivative at `b` equal to `c`. (Assumes measurability and uniqueness of tangent vectors.)
|
intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right
theorem intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
Filter.Tendsto f (nhdsWithin b t ⊓ MeasureTheory.volume.ae) (nhds c) →
HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) c s b
The Fundamental Theorem of Calculus is stated as follows: given a function `f : ℝ → E` which is interval integrable on `a..b`, and the limit of `f x` as `x` approaches `b` from either the right or the left is finite and equals some `c` (almost surely), then the function `u ↦ ∫ x in a..u, f x` has a right (or left) derivative at `b` which is `c`. The theorem is specific in the sense that it requires the function `f` to be strongly measurable at a chosen filter and to also have a limit that tends to `c` at that filter, almost everywhere with respect to the Lebesgue measure.
More concisely: If a strongly measurable function `f : ℝ → E` on the real numbers `ℝ` with values in a Banach space `E` is interval integrable on `a..b` and has right-left limiting value `c` at `b`, then the function `u ↦ ∫ x in a..u, f x` has a right (or left) derivative at `b` equal to `c`.
|
intervalIntegral.derivWithin_integral_left
theorem intervalIntegral.derivWithin_integral_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
ContinuousWithinAt f t a →
autoParam (UniqueDiffWithinAt ℝ s a) _auto✝ → derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -f a
This theorem is a version of the Fundamental Theorem of Calculus. For a given function `f : ℝ → E`, that is interval integrable on an interval `a..b`, if `f x` is continuous on the right or on the left at `a`, then the right (or left) derivative of the function `u ↦ ∫ x in u..b, f x` at `a` is equal to `-f a`. The theorem requires that the function `f` is strongly measurable at a filter from `nhdsWithin a t` with respect to the Lebesgue measure, and continuous within the set `t` at `a`. The theorem makes use of an assumption (provided via `autoParam`) that the set `s` has a unique differential at `a` in ℝ.
More concisely: If a function `f : ℝ → E` is interval integrable on an interval `[a, b]` and `f` is continuous on the right (or left) at `a`, then the derivative of the function `u ↦ ∫ x in u..b, f x` at `a` is equal to `-f a`. (Assumes `f` is strongly measurable at a filter from `nhdsWithin a t` with respect to the Lebesgue measure, continuous within the set `t` at `a`, and `s` has a unique differential at `a` in ℝ.)
|
intervalIntegral.integral_hasFDerivWithinAt
theorem intervalIntegral.integral_hasFDerivWithinAt :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{la lb : Filter ℝ} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f la MeasureTheory.volume →
StronglyMeasurableAtFilter f lb MeasureTheory.volume →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) la]
[inst_4 : intervalIntegral.FTCFilter b (nhdsWithin b t) lb],
Filter.Tendsto f la (nhds (f a)) →
Filter.Tendsto f lb (nhds (f b)) →
HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x)
((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a))
(s ×ˢ t) (a, b)
The theorem `intervalIntegral.integral_hasFDerivWithinAt` states that for a function `f` which is measurable and interval integrable over an interval from `a` to `b`, the function `(u, v) ↦ ∫ x in u..v, f x` has a derivative `(u, v) ↦ v • f b - u • f a` within the cartesian product of sets `s` and `t` at the point `(a, b)`. Here, `s` and `t` are elements of the set `{Iic a, {a}, Ici a, univ}` and `{Iic b, {b}, Ici b, univ}` respectively. The function `f` tends to `f a` and `f b` at filters `la` and `lb` respectively, as specified by a table in the theorem's documentation. This condition usually means that the function `f` is continuous at a given point or within a given set. The theorem is a statement about the derivative of an interval integral of a function, which is a version of the Fundamental Theorem of Calculus.
More concisely: The theorem `intervalIntegral.integral_hasFDerivWithinAt` asserts that the function defining the interval integral of a measurable and interval integrable function over an interval has a derivative equal to the product of the interval endpoints and the function values at the endpoints.
|
intervalIntegral.deriv_integral_right
theorem intervalIntegral.deriv_integral_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
ContinuousAt f b → deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b
This theorem, known as the fundamental theorem of calculus, states that if a function `f` mapping real numbers to a normed additively commutative group `E` is interval integrable on an interval from `a` to `b` with respect to the Lebesgue measure, and `f` is strongly measurable and continuous at `b`, then the derivative of the function `u ↦ ∫ x in a..u, f x` at `b` equals `f(b)`. In other words, the rate of change of the integral of `f` from `a` to `u` at `u = b` is exactly `f(b)`. This theorem is crucial in connecting differentiation and integration in calculus.
More concisely: If a continuous, strongly measurable function `f` on a real interval [a, b] is integrable, then the derivative of the function `u ↦ ∫x in a..u, f x` exists and equals `f(u)` at `u = b`.
|
intervalIntegral.integral_deriv_eq_sub
theorem intervalIntegral.integral_deriv_eq_sub :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
(∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) →
IntervalIntegrable (deriv f) MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, deriv f y = f b - f a
This is a statement of the Fundamental Theorem of Calculus-2 in Lean. It states that if a function `f : ℝ → E`, where `E` is a normed space over real numbers, is differentiable at every point `x` within the closed interval `[a, b]`, and if the derivative of `f` is interval integrable over `[a, b]`, then the integral over the range `a..b` of the derivative of `f` equals `f b - f a`. This theorem connects differentiation and integration in a profound way, asserting that the area under the curve of a function's derivative over a certain interval is equal to the difference in the values of the original function at the interval's endpoints.
More concisely: If a real-valued function `f` on a closed interval `[a, b]` is differentiable with integrable derivative, then the integral of `f'` over `[a, b]` equals `f b - f a`.
|
intervalIntegral.integrableOn_deriv_right_of_nonneg
theorem intervalIntegral.integrableOn_deriv_right_of_nonneg :
∀ {g' g : ℝ → ℝ} {a b : ℝ},
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
(∀ x ∈ Set.Ioo a b, 0 ≤ g' x) → MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume
This theorem states that given a real-valued function `g` on a closed interval `[a, b]`, if the function is continuous on that interval and for each point `x` in the open interval `(a, b)`, the function `g` has a right derivative `g'(x)` at `x` and `g'(x)` is nonnegative, then the derivative function `g'` is integrable over the half-open interval `(a, b]` with respect to the Lebesgue measure. This theorem provides a sufficient condition for the integrability of the derivative of a function.
More concisely: If a real-valued function `g` on a closed interval `[a, b]` is continuous and has nonnegative right derivatives `g'(x)` in the open interval `(a, b)`, then `g'` is integrable over the half-open interval `(a, b]` with respect to the Lebesgue measure.
|
intervalIntegral.integral_deriv_eq_sub'
theorem intervalIntegral.integral_deriv_eq_sub' :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f' : ℝ → E}
{a b : ℝ} (f : ℝ → E),
deriv f = f' →
(∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) →
ContinuousOn f' (Set.uIcc a b) → ∫ (y : ℝ) in a..b, f' y = f b - f a
The theorem `intervalIntegral.integral_deriv_eq_sub'` states that for every real-valued function `f` on a normed additive commutative group `E` with a normed space structure over the real numbers, and which is complete, given its derivative `f'`, and any two real numbers `a` and `b`, if the function `f` is differentiable at every point in the closed interval between `a` and `b` (inclusive), and the derivative `f'` is continuous on this interval, then the integral of `f'` from `a` to `b` equals the value of `f` at `b` minus the value of `f` at `a`. This is essentially the fundamental theorem of calculus.
More concisely: If a real-valued function on a complete normed additive commutative group with a normed space structure is differentiable with a continuous derivative on a closed interval, then the integral of its derivative equals the function's value at the right endpoint minus its value at the left endpoint.
|
intervalIntegral.integral_comp_mul_deriv''
theorem intervalIntegral.integral_comp_mul_deriv'' :
∀ {a b : ℝ} {f f' g : ℝ → ℝ},
ContinuousOn f (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
ContinuousOn f' (Set.uIcc a b) →
ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
This theorem is about the change of variables for continuous integrands. It states that, given real numbers `a` and `b`, functions `f`, `f'`, and `g` where `f` is continuous on the closed interval `[a, b]`, `f` has a continuous right-derivative `f'` within the open interval `(a, b)` and `f'` is also continuous on `[a, b]`, and `g` is continuous on the image of `f` within `[a, b]`, then the integral from `a` to `b` of `(g ∘ f) x * f' x` with respect to `x` equals the integral from `f a` to `f b` of `g u` with respect to `u`. This essentially allows us to substitute `u = f x` in the integral.
More concisely: If `f: [a, b] -> ℝ` is continuous with a continuous right-derivative `f'` on `(a, b)`, `g: ℝ -> ℝ` is continuous on the image of `f` on `[a, b]`, then ∫(g ∘ f) dx = ∫g(f(x)) df.
|
intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right
theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ}
{c : E} {lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ}
[inst_2 : intervalIntegral.FTCFilter b lb lb'] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
IntervalIntegrable f μ a b →
StronglyMeasurableAtFilter f lb' μ →
Filter.Tendsto f (lb' ⊓ μ.ae) (nhds c) →
Filter.Tendsto u lt lb →
Filter.Tendsto v lt lb →
(fun t =>
∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt]
fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
This is a version of the Fundamental Theorem of Calculus (FTC-1), focusing on the strict derivative at the right endpoint for a locally finite measure.
In the context of this theorem, we consider a measurable function `f` that is interval integrable over an interval `a..b`. We have a pair of FTC filters `lb` and `lb'` around a point `b`, and assume that `f` has a finite limit `c` at the infimum of `lb'` and the set of points where `μ` is almost everywhere defined.
The theorem states that as `u` and `v` tend to `lb`, the difference between the integral of `f` over `a..v` and the integral of `f` over `a..u` equals to the integral of the constant function `c` over `u..v`, up to a small error term. The error term is a little o of the integral of the constant function `1` over `u..v`. That is, the error term becomes negligible as `u` and `v` get closer and closer to `lb`.
This result is a formal expression of the property that the net "change" in an integral over an interval as the interval shifts is closely approximated by the value of the function at the shifting endpoint, a key concept in the Fundamental Theorem of Calculus.
More concisely: Given a measurable, interval integrable function `f` with a finite limit `c` at the right endpoint `b`, and locally finite measure `μ`, as `u` and `v` approach `b`, the difference between the integrals of `f` over `[a, u]` and `[a, v]` equals `c * (v - u) + o(v - u)`, where `o(v - u)` is a little-o error term.
|
intervalIntegral.intervalIntegrable_deriv_of_nonneg
theorem intervalIntegral.intervalIntegrable_deriv_of_nonneg :
∀ {g' g : ℝ → ℝ} {a b : ℝ},
ContinuousOn g (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ g' x) → IntervalIntegrable g' MeasureTheory.volume a b
This theorem states that if a real-valued function `g` is continuous on the closed interval `[a, b]`, has a derivative `g'` at each point in the open interval `(min(a, b), max(a, b))`, and this derivative is nonnegative within the same open interval, then `g'` is interval integrable with respect to the Lebesgue measure on the interval `[a, b]`. In other words, when the derivative of a function is nonnegative throughout an interval, it is automatically integrable over that interval.
More concisely: If a real-valued function `g` is continuous on a closed interval `[a, b]`, has a nonnegative derivative `g'` that is integrable on the open interval `(a, b)`, then `g'` is integrable with respect to the Lebesgue measure on `[a, b]`.
|
intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le
theorem intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le :
∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
a ≤ b →
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
(∀ x ∈ Set.Ioo a b, φ x ≤ g' x) → ∫ (y : ℝ) in a..b, φ y ≤ g b - g a
This theorem, `intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le`, is an auxiliary lemma used in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`. It states that for any three real-valued functions `g'`, `g`, and `φ`, and any two real numbers `a` and `b` where `a` is less than or equal to `b`, if the function `g` is continuous on the closed interval from `a` to `b` (`Set.Icc a b`), `g` has a derivative `g'` at every point `x` in the open interval from `a` to `b` (`Set.Ioo a b`) within the open right-infinite interval greater than `x` (`Set.Ioi x`), `φ` is integrable on the closed interval from `a` to `b` under the Lebesgue measure (`MeasureTheory.volume`), and `φ` is less than or equal to `g'` for all `x` in the open interval from `a` to `b`, then the integral of `φ` from `a` to `b` is less than or equal to the difference of `g` at `b` and `g` at `a`.
More concisely: If a real-valued function `g` is continuous on a closed interval `[a, b]`, has a derivative `g'` at every point in the open interval `(a, b)`, `φ` is integrable on `[a, b]`, and `φ ≤ g'` on `(a, b)`, then `∫[a, b] φ d x ≤ g(b) - g(a)`.
|
intervalIntegral.integral_sub_linear_isLittleO_of_tendsto_ae
theorem intervalIntegral.integral_sub_linear_isLittleO_of_tendsto_ae :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
{f : ℝ → E} {c : E} {l l' : Filter ℝ} {lt : Filter ι} {a : ℝ} [inst_3 : intervalIntegral.FTCFilter a l l'],
StronglyMeasurableAtFilter f l' MeasureTheory.volume →
Filter.Tendsto f (l' ⊓ MeasureTheory.volume.ae) (nhds c) →
∀ {u v : ι → ℝ},
Filter.Tendsto u lt l →
Filter.Tendsto v lt l → (fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)
This is a local version of the **Fundamental Theorem of Calculus-1**. The theorem states that if a function `f` has a finite limit `c` almost everywhere at a filter `l'`, where `(l, l')` is a filter pair around a real number `a` defined by `intervalIntegral.FTCFilter`, then the interval integral of `f` over the interval from `u` to `v` is equal to `(v - u) * c + o(v - u)`, as both `u` and `v` tend to `l`. This result holds when `f` is strongly measurable with respect to the volume measure restricted to `l'`, and `f` tends to `c` almost everywhere at `l'` with respect to the neighborhood filter of `c`. Here `u` and `v` are functions of a variable from an arbitrary type `ι`, and both functions `u` and `v` tend to `l` with respect to a filter `lt`. The `o` notation represents the little-o notation in asymptotic analysis.
More concisely: If a function `f` is strongly measurable with respect to the volume measure and has a limit `c` almost everywhere at a filter `l'` around a real number `a`, then `∫(v - u) * f d(v - u) = (v - u) * ∫f dv + o((v - u)^2)` as `u` and `v` tend to `l` with respect to a filter `lt`, where `u` and `v` are functions of a variable from an arbitrary type `ι` and `∫` denotes the Riemann integral.
|
intervalIntegral.fderivWithin_integral_of_tendsto_ae
theorem intervalIntegral.fderivWithin_integral_of_tendsto_ae :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{ca cb : E} {la lb : Filter ℝ} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f la MeasureTheory.volume →
StronglyMeasurableAtFilter f lb MeasureTheory.volume →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) la]
[inst_4 : intervalIntegral.FTCFilter b (nhdsWithin b t) lb],
Filter.Tendsto f (la ⊓ MeasureTheory.volume.ae) (nhds ca) →
Filter.Tendsto f (lb ⊓ MeasureTheory.volume.ae) (nhds cb) →
autoParam (UniqueDiffWithinAt ℝ s a) _auto✝ →
autoParam (UniqueDiffWithinAt ℝ t b) _auto✝¹ →
fderivWithin ℝ (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) (s ×ˢ t) (a, b) =
(ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
This theorem states that if you have a measurable function `f` which is interval integrable on an unordered interval `a..b`, and you choose sets `s` and `t` from the sets `{Iic a, Ici a, univ}` and `{Iic b, Ici b, univ}` respectively. If `f` tends to constants `ca` and `cb` almost surely at filters `la` and `lb` (as specified in the given table), then the derivative of the function defined by the integral of `f` from `p.1` to `p.2` with respect to the product set `s ×ˢ t` at the point `(a, b)` is equal to the linear combination of `cb` and `ca` with coefficients given by the second and first coordinates of the point `(u, v)`, i.e., `(u, v) ↦ u • cb - v • ca`.
The table specifies the relationship between the sets `s` and `t` and the filters `la` and `lb` as follows:
- When `s` is `Iic a`, `la` is `𝓝[≤] a`. When `t` is `Iic b`, `lb` is `𝓝[≤] b`.
- When `s` is `Ici a`, `la` is `𝓝[>] a`. When `t` is `Ici b`, `lb` is `𝓝[>] b`.
- When `s` is `{a}`, `la` is `⊥`. When `t` is `{b}`, `lb` is `⊥`.
- When `s` is `univ`, `la` is `𝓝 a`. When `t` is `univ`, `lb` is `𝓝 b`.
More concisely: If `f` is a measurable, interval integrable function on an unordered interval `a..b`, tending to constants `ca` and `cb` almost surely at filters `la` and `lb` respectively, then the derivative of the function defined as the integral of `f` on `a..b` with respect to the product measure on sets `{Iic a, Ici a, univ}` and `{Iic b, Ici b, univ}` equals `cb - ca` multiplied by the second and first coordinates of the interval endpoints.
|
intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left
theorem intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
Filter.Tendsto f (nhds a ⊓ MeasureTheory.volume.ae) (nhds c) →
HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
The **Fundamental Theorem of Calculus-1** states that if a real-valued function `f` is interval integrable on a given interval `a..b`, and `f(x)` has a finite limit `c` almost surely as `x` approaches `a`, then the function `u ↦ ∫ x in u..b, f x` has a derivative at `a` which is `-c`. Here, 'almost surely' means that the set of exceptions has measure zero, 'interval integrable' means that `f` is integrable on both intervals `(a, b]` and `(b, a]` (one of which is always empty), 'finite limit' means the function `f` approaches a finite value `c` as `x` approaches `a` and 'has a derivative' means the function has a rate of change at a certain point.
More concisely: If a real-valued function `f` is interval integrable on `[a, b]` and has a right-hand limit `c` at `a`, then `∫ x in a..b, f x` has a derivative equal to `-c` at `a`.
|
intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real
theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real :
∀ {g' g : ℝ → ℝ} {a b : ℝ},
a ≤ b →
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
MeasureTheory.IntegrableOn g' (Set.Icc a b) MeasureTheory.volume → ∫ (y : ℝ) in a..b, g' y = g b - g a
The theorem `intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real` states that for all real-valued functions `g'` and `g` and for all real numbers `a` and `b` such that `a` is less than or equal to `b`, if the function `g` is continuous on the closed interval from `a` to `b` and for every `x` in the open interval from `a` to `b`, `g` has a derivative `g'(x)` at the point `x` within the right-infinite interval starting from `x`, and if `g'` is integrable on the closed interval from `a` to `b` with respect to the Lebesgue measure, then the definite integral of `g'` from `a` to `b` equals to the difference of `g(b)` and `g(a)`.
More concisely: If a real-valued function `g` is continuous on a closed interval [`a`, `b`], differentiable on the open interval [`a`, `b`], and its derivative `g'` is integrable on [`a`, `b`], then `∫(g' dx) = g(b) - g(a)`.
|
intervalIntegral.deriv_integral_left
theorem intervalIntegral.deriv_integral_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
ContinuousAt f a → deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -f a
This is the Fundamental Theorem of Calculus. It states that if a function `f : ℝ → E` is interval integrable on an interval `a..b` and `f` is continuous at `a`, then the derivative of the function `u ↦ ∫ x in u..b, f x` at the point `a` equals `-f a`. Here `E` is a normed additive commutative group which is also a normed space over the real numbers, and is complete. The function `f` is assumed to be strongly measurable at a filter around `a` with respect to Lebesgue measure. The function `u ↦ ∫ x in u..b, f x` is the function that maps `u` to the integral of `f` over the interval from `u` to `b`. The theorem is a central result in analysis that links the concept of differentiation and integration.
More concisely: If a continuous and strongly measurable function `f : ℝ → E` on an interval `[a, b]` is interval integrable, then the derivative of the function `u ↦ ∫ x in u..b, f x` at `a` equals `-f a`.
|
intervalIntegral.derivWithin_integral_right
theorem intervalIntegral.derivWithin_integral_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
ContinuousWithinAt f t b →
autoParam (UniqueDiffWithinAt ℝ s b) _auto✝ → derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = f b
This theorem is known as the fundamental theorem of calculus. It states that if a function `f : ℝ → E` is interval integrable over an unordered interval `a..b`, and the function `f(x)` is continuous on the right or left at `b`, then the right (or left) derivative of the function `u ↦ ∫ x in a..u, f x` at `b` equals `f(b)`. Here, `ℝ → E` is a function from the real numbers to a NormedAddCommGroup `E`, and `a` and `b` are real numbers. The theorem also requires the conditions that `f` is strongly measurable at a filter `nhdsWithin b t` with respect to the Lebesgue measure, and that `f` is continuous within the set `t` at `b`. The uniqueness of the derivative within the set `s` at `b` is assumed automatically.
More concisely: If a function `f : ℝ → E` is interval integrable over `a..b`, continuously differentiable at `b`, and satisfies the Lebesgue integrability and continuity conditions at `b`, then `(d/dy)(∫ x in a..y, f x) = f(y)` at `y = b`.
|
intervalIntegral.integral_hasStrictDerivAt_left
theorem intervalIntegral.integral_hasStrictDerivAt_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
ContinuousAt f a → HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
The theorem, termed as the "Fundamental theorem of calculus-1", asserts the strict differentiability at the left endpoint of a function. Specifically, if a function `f` mapping real numbers to a normed add commutative group `E` is interval integrable on an interval `a..b` and is continuous at the point `a`, then the function `u ↦ ∫ x in u..b, f x` has a derivative at `a` equal to `-f a` in the sense of strict differentiability. This is a key theorem in calculus that links the concept of an integral with that of derivative.
More concisely: If a real-valued, continuous function `f` on an interval `[a, b]` is integrable on `[a, b]`, then the function `F(x) = ∫ t from a to x, f(t) dt` is differentiable at `x = a` with derivative `-f(a)`.
|
intervalIntegral.fderiv_integral_of_tendsto_ae
theorem intervalIntegral.fderiv_integral_of_tendsto_ae :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{ca cb : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
Filter.Tendsto f (nhds a ⊓ MeasureTheory.volume.ae) (nhds ca) →
Filter.Tendsto f (nhds b ⊓ MeasureTheory.volume.ae) (nhds cb) →
fderiv ℝ (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) (a, b) =
(ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
The **Fundamental Theorem of Calculus-1** states that if a function `f` mapping real numbers to a normed additively commutative group `E` is interval integrable on an interval from `a` to `b`, and if `f` has finite limits `ca` and `cb` almost surely when `x` approaches `a` and `b` respectively, then the derivative of the map `(u, v) ↦ ∫ x in u..v, f x` at the point `(a, b)` is equal to the map `(u, v) ↦ v*cb - u*ca`. This is expressed by using the continuous linear map `ContinuousLinearMap.snd ℝ ℝ ℝ` multiplied by `cb` and subtracting the continuous linear map `ContinuousLinearMap.fst ℝ ℝ ℝ` multiplied by `ca`. The various conditions on `f` express requirements like strong measurability at `a` and `b` and that `f` must tend to its respective limits `ca` and `cb` at `a` and `b` in a specific way, namely almost everywhere with respect to the volume measure.
More concisely: If a real-valued function `f` is interval integrable on `[a, b]` with finite limits `ca` and `cb` at `a` and `b` respectively, then the definite integral `∫[a, b] f dx` is equal to `cb * (b - a) - ca`.
|
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae
theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E}
{l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ}
[inst_2 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_3 : intervalIntegral.FTCFilter a l l'],
StronglyMeasurableAtFilter f l' μ →
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
Filter.Tendsto u lt l →
Filter.Tendsto v lt l →
(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
∫ (x : ℝ) in u t..v t, 1 ∂μ
This is the local version of the Fundamental Theorem of Calculus-1 for any measure. Given filters `l` and `l'` that are related by `[intervalIntegral.FTCFilter a l l']` and a locally finite measure `μ`, if there is a function `f` that has a finite limit `c` at the intersection of `l'` and `μ.ae`, then the difference between the integral of `f` and a constant `c` over the interval from `u` to `v` is little-o of the integral of 1 over the same interval, as both `u` and `v` tend to `l`. This holds when `f` is strongly measurable at filter `l'` with respect to measure `μ`, and `f`, `u`, and `v` all tend to `l` in the sense of filter `lt`.
In other words, the deviation of the integral of `f` from the integral of its limit `c` becomes negligible compared to the size of the interval as this interval shrinks and approaches `l`. This theorem is a generalization of the standard result from calculus about the behavior of integrals of a function near a point where the function has a limit.
More concisely: Given filters `l` and `l'`, locally finite measure `μ`, and strongly measurable function `f` with limit `c` at `l'` with respect to `μ`, if `f` integrates to `c` over any interval in `l'`, then the difference between `∫[u,v] f dμ` and `c` is o(∫[u,v] 1 dμ) as `u` and `v` tend to `l` in the filter `lt`.
|
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge
theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E}
{l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [inst_2 : CompleteSpace E]
[inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_4 : intervalIntegral.FTCFilter a l l'],
StronglyMeasurableAtFilter f l' μ →
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
Filter.Tendsto u lt l →
Filter.Tendsto v lt l →
lt.EventuallyLE v u →
(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + (↑↑μ (Set.Ioc (v t) (u t))).toReal • c) =o[lt] fun t =>
(↑↑μ (Set.Ioc (v t) (u t))).toReal
This is the local version of the Fundamental Theorem of Calculus for any measure. Given two filters `l` and `l'` related by `[intervalIntegral.FTCFilter a l l']` and a locally finite measure `μ`, if a function `f` has a finite limit `c` at `l' ⊓ μ.ae`, then the integral of `f` over the interval `[u, v]` with respect to `μ` is equal to `-μ (Set.Ioc v u) • c + o(μ(Set.Ioc v u))` as both `u` and `v` tend to `l`. This theorem requires that `f` is strongly measurable at filter `l'` with respect to `μ`, the function `f` tends to `c` at the filter `l' ⊓ μ.ae`, and both `u` and `v` tend to `l` eventually with `v ≤ u`. Additionally, this theorem also applies when `l = l' = Filter.atTop`.
More concisely: Given filters `l` and `l'`, locally finite measure `μ`, and strongly measurable function `f` with respect to `μ`, if `f` has a finite limit `c` at `l' ⊓ μ.ae` and `u` and `v` tend to `l` with `v ≤ u` such that `[intervalIntegral.FTCFilter a l l']`, then `∫[u, v] f dμ = -μ (Set.Ioc v u) • c + o(μ(Set.Ioc v u))`.
|
intervalIntegral.integral_comp_mul_deriv'
theorem intervalIntegral.integral_comp_mul_deriv' :
∀ {a b : ℝ} {f f' g : ℝ → ℝ},
(∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
ContinuousOn f' (Set.uIcc a b) →
ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x
The theorem named `intervalIntegral.integral_comp_mul_deriv'` states the following: Given two real-valued functions `f` and `g` and the real numbers `a` and `b`, if `f` has a continuous derivative `f'` on the closed interval `[a, b]`, `f'` is continuous on `[a, b]`, and `g` is continuous on the image of `[a, b]` under `f`, i.e., `f '' [a, b]`, then the integral of the function `(g ∘ f) x * f' x` from `a` to `b` is equal to the integral of the function `g` from `f(a)` to `f(b)`. This theorem is a variant of the change of variables formula for definite integrals, in which we substitute `u = f x`. Compared to `intervalIntegral.integral_comp_mul_deriv`, this theorem only requires that `g` is continuous on the image of `[a, b]` under `f`.
More concisely: If functions `f` with a continuous derivative `f'` and continuous function `g` are defined on a closed interval `[a, b]` such that `g` is continuous on `f[a, b]`, then the definite integral of `g(f(x)) * f'(x)` from `x = a` to `x = b` equals the definite integral of `g(u)` from `u = f(a)` to `u = f(b)`.
|
intervalIntegral.deriv_integral_of_tendsto_ae_left
theorem intervalIntegral.deriv_integral_of_tendsto_ae_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
Filter.Tendsto f (nhds a ⊓ MeasureTheory.volume.ae) (nhds c) →
deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -c
The theorem, known as the Fundamental Theorem of Calculus, states that if a real-valued function `f` is interval integrable on an interval from `a` to `b` and `f` has a finite limit `c` almost surely at `a`, then the derivative of the function given by `u ↦ ∫ x in u..b, f x` at `a` equals `-c`. Here, interval integrable means that `f` is integrable on both intervals `(a, b]` and `(b, a]`. The condition that `f` has a finite limit `c` almost surely at `a` is formalized by the fact that `f` is strongly measurable at a filter `nhds a` with respect to a measure `MeasureTheory.volume` and `f` tends to `c` at the neighborhood filter at `a` intersected with the set of measurable values. This theorem is a key result in real analysis and provides a link between integral calculus and differential calculus.
More concisely: If a real-valued function `f` is interval integrable on an interval `[a, b]` and has a finite limit `c` at `a`, then `(d/dx)(∫x in a..b, f x) = -c`.
|
intervalIntegral.differentiableOn_integral_of_continuous
theorem intervalIntegral.differentiableOn_integral_of_continuous :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a : ℝ} {s : Set ℝ},
(∀ x ∈ s, IntervalIntegrable f MeasureTheory.volume a x) →
Continuous f → DifferentiableOn ℝ (fun u => ∫ (x : ℝ) in a..u, f x) s
This theorem states that the integral of a continuous function is differentiable on a real set `s`. Specifically, for any normed additive commutative group `E` that is also a complete space, and any real-valued function `f`, if `f` is interval integrable with respect to Lebesgue measure between a real number `a` and any point in the set `s`, and `f` is continuous, then the function that maps a real number `u` to the integral of `f` from `a` to `u` is differentiable at any point in the set `s`. This implies that you can differentiate under the integral sign in this case.
More concisely: If a continuous, interval integrable function defines an ordinary real-valued function of a real variable through integration, then this function is differentiable.
|
intervalIntegral.integral_comp_smul_deriv'''
theorem intervalIntegral.integral_comp_smul_deriv''' :
∀ {G : Type u_6} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → G},
ContinuousOn f (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
ContinuousOn g (f '' Set.Ioo (min a b) (max a b)) →
MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume →
MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.uIcc a b) MeasureTheory.volume →
∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
This theorem is a general form of the change of variables in integrals. It states that if we have a function `f` that is continuous on the closed interval `[a, b]` and has a right derivative `f'` within the open interval `(a, b)`, and another function `g` that is continuous on the image of `f` within `(a, b)` and integrable on the image of `f` within `[a, b]`, and if the expression `f'(x) * (g ◦ f)(x)` is integrable on `[a, b]`, then we can substitute `u = f(x)` in the integral and end up with the result that the integral from `a` to `b` of `f'(x) * (g ◦ f)(x)` with respect to `x` is equal to the integral from `f(a)` to `f(b)` of `g(u)` with respect to `u`. This theorem is a powerful tool in calculus that allows us to simplify the computation of integrals by changing variables.
More concisely: If `f` is a continuous function on `[a, b]` with a right derivative in `(a, b)`, `g` is continuous on the image of `f` in `(a, b)` and integrable on this image, and `f'(x) * (g ◦ f)(x)` is integrable on `[a, b]`, then the integral of `f'(x) * (g ◦ f)(x)` from `a` to `b` equals the integral of `g(u)` from `f(a)` to `f(b)`.
|
intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left
theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ}
{c : E} {la la' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ}
[inst_2 : intervalIntegral.FTCFilter a la la'] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
IntervalIntegrable f μ a b →
StronglyMeasurableAtFilter f la' μ →
Filter.Tendsto f (la' ⊓ μ.ae) (nhds c) →
Filter.Tendsto u lt la →
Filter.Tendsto v lt la →
(fun t =>
∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt]
fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
This is a statement of a version of the Fundamental Theorem of Calculus with respect to a locally finite measure. Given a real-valued function `f` which is interval integrable on `a..b` and a pair of `intervalIntegral.FTCFilter`s `la` and `la'` around `a`, assume that `f` has a finite limit `c` at the intersection of `la'` and `μ.ae`.
The theorem states that for filters of real numbers `u` and `v` tending towards `la`, the difference of the integral of `f` from `v` to `b` and the integral of `f` from `u` to `b`, plus the integral of `c` from `u` to `v`, equals `o(∫ x in u..v, 1 ∂μ)`. In other words, the difference goes to zero faster than the integral of `u` to `v` as `u` and `v` tend to `la`. This theorem is a crucial part of establishing the relationship between integrals and derivatives in measure theory.
More concisely: Given a locally finite measure `μ`, a real-valued function `f` that is interval integrable on `[a, b]`, and filters `u` and `v` converging to `a`, the integral of `f` from `v` to `b` minus the integral of `f` from `u` to `b`, plus the product of `c` (the limit of `f` at `a` with respect to `μ`) and the measure of `u` to `v`, approaches zero faster than the measure of `u` to `v`, where `c` and `μ.ae` exist.
|
intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le
theorem intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f f' : ℝ → E}
{a b : ℝ},
a ≤ b →
ContinuousOn f (Set.Icc a b) →
(∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
The Fundamental Theorem of Calculus, Part 2, states that if a function `f : ℝ → E` is continuous over the closed interval `[a, b]` (where `a ≤ b`) and has a derivative at `f' x` for all `x` within the open interval `(a, b)`, and if the derivative `f'` is interval integrable over `[a, b]`, then the integral of `f'` from `a` to `b` equals `f b - f a`. This theorem essentially connects the concept of derivatives and integrals, stating that the integral of a derivative over an interval is equal to the change in the original function over that interval.
More concisely: If a continuous function `f : ℝ → E` on the interval `[a, b]` with `a ≤ b` has a integrable derivative `f'`, then `∫[a, b] f' dx = f b - f a`.
|
intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico
theorem intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico :
∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
a ≤ b →
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ico a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
(∀ x ∈ Set.Ico a b, g' x ≤ φ x) → g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
The theorem named `intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico` is a part of the Fundamental Theorem of Calculus (FTC-2) for real-valued functions with integrable derivatives. It states that for any functions `g`, `g'` and `φ` mapping real numbers to real numbers, and any real numbers `a` and `b` where `a` is less than or equal to `b`, if `g` is continuous on the closed interval from `a` to `b`, and the derivative of `g` at any point `x` in the half-open interval from `a` to `b` exists and is less than or equal to the function `φ` at `x`, and if `φ` is integrable on the closed interval from `a` to `b`, then the difference `g(b) - g(a)` is less than or equal to the integral of `φ` from `a` to `b`. The remarkable part of this theorem is that it holds even if `g'` is not known to be integrable.
More concisely: If a real-valued function `g` is continuous on a closed interval `[a, b]`, and the derivative of `g` is pointwise less than or equal to an integrable function `φ` on `[a, b]`, then `g(b) - g(a)` is less than or equal to the integral of `φ` from `a` to `b`.
|
intervalIntegral.derivWithin_integral_of_tendsto_ae_left
theorem intervalIntegral.derivWithin_integral_of_tendsto_ae_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{c : E} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
Filter.Tendsto f (nhdsWithin a t ⊓ MeasureTheory.volume.ae) (nhds c) →
autoParam (UniqueDiffWithinAt ℝ s a) _auto✝ → derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -c
The theorem `intervalIntegral.derivWithin_integral_of_tendsto_ae_left` is a version of the Fundamental Theorem of Calculus. It states that if a function `f : ℝ → E`, where `E` is a normed additively commutative group with a complete normed vector space structure over real numbers, is interval integrable on an interval from `a` to `b` and `f(x)` converges almost surely to a limit `c` as `x` approaches `a` from either direction, then the left or right derivative of the function `u ↦ ∫ x in u..b, f x` at `a` is `-c`. This theorem considers general measurable functions `f` and requires conditions on the filters `s` and `t` around `a`, where `s` is the set in which differentiation takes place and `t` is the set within which the function `f` is strongly measurable.
More concisely: If a function `f : ℝ → E` is interval integrable on an interval `[a, b]` and `f(x)` converges almost surely to a limit `c` as `x` approaches `a`, then the left derivative of `x ↦ ∫ x in a..b, f x` at `a` is `-c`.
|
intervalIntegral.integral_comp_mul_deriv'''
theorem intervalIntegral.integral_comp_mul_deriv''' :
∀ {a b : ℝ} {f f' g : ℝ → ℝ},
ContinuousOn f (Set.uIcc a b) →
(∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
ContinuousOn g (f '' Set.Ioo (min a b) (max a b)) →
MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume →
MeasureTheory.IntegrableOn (fun x => (g ∘ f) x * f' x) (Set.uIcc a b) MeasureTheory.volume →
∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
This theorem is a version of the change of variables rule for scalar functions in integration. It states that if we have a function `f` that is continuous on the closed interval `[a, b]` and has a continuous right-derivative `f'` in the open interval `(a, b)`, and another function `g` that is continuous on the image of `(a, b)` under `f` and integrable on the image of `[a, b]` under `f`, then, if the function `(g ∘ f) x * f' x` is integrable on `[a, b]`, we can change variables in the integral from `x` to `u = f x`. This gives the equality `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`, meaning that the integral of the product of `g` composed with `f` and the derivative of `f`, with respect to `x` from `a` to `b`, is equal to the integral of `g` with respect to `u` (where `u = f x`) from `f a` to `f b`.
More concisely: If a function `f` is continuous on a closed interval `[a, b]` with a continuous right-derivative in the open interval `(a, b)`, and the composite function `g ∘ f` and the product `(g ∘ f) x * f' x` are integrable on `[a, b]`, then `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
|
Continuous.integral_hasStrictDerivAt
theorem Continuous.integral_hasStrictDerivAt :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E},
Continuous f → ∀ (a b : ℝ), HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
The **Fundamental Theorem of Calculus - Part 1** states that if a function `f` is continuous over the real numbers, then the function `u ↦ ∫ x in a..u, f x` (which represents the integral of `f` from a fixed point `a` to a variable point `u`) has a strict derivative at any point `b` that equals the value of `f` at `b`.
In more formal terms, for any function `f : ℝ → E` where `E` stands for a normed add commutative group which is also a normed space over real numbers and a complete space, if `f` is continuous, then for any real numbers `a` and `b`, the function defined as `(fun u => ∫ (x : ℝ) in a..u, f x)` has a strict derivative at `b` and it is equal to `f b`. This is the essence of the first part of the Fundamental Theorem of Calculus.
More concisely: If a function `f : ℝ → E` is continuous, then the function `u mapsto ∫ x in a..u, f x` has a strict derivative equal to `f` at each point `u` in ℝ, where `E` is a complete normed add commutative group and normed space over real numbers.
|
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le
theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E}
{l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [inst_2 : CompleteSpace E]
[inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_4 : intervalIntegral.FTCFilter a l l'],
StronglyMeasurableAtFilter f l' μ →
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
Filter.Tendsto u lt l →
Filter.Tendsto v lt l →
lt.EventuallyLE u v →
(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - (↑↑μ (Set.Ioc (u t) (v t))).toReal • c) =o[lt] fun t =>
(↑↑μ (Set.Ioc (u t) (v t))).toReal
This is a local version of the Fundamental Theorem of Calculus-1 applicable to any measure. Given functions `f : ℝ → E`, `u : ι → ℝ`, `v : ι → ℝ` and constants `a : ℝ`, `c : E`, it states the following: If filters `l` and `l'` are related according to the condition `[intervalIntegral.FTCFilter a l l']` and `μ` is a locally finite measure, and if `f` has a finite limit `c` at the intersection of `l'` and the almost everywhere filter of `μ`, then the difference between the integral of `f` with respect to `μ` over the interval from `u` to `v` and the product of `μ` measured over the interval `(u, v]` and `c` is little-o of `μ` measured over the interval `(u, v]` as both `u` and `v` tend to `l` in filter `lt`.
In other words, as `u` and `v` approach `l`, the difference between the integral of `f` from `u` to `v` and `c` times the measure of the interval `(u, v]` becomes negligible compared to the measure of the interval `(u, v]`. This theorem is a generalization of the fundamental theorem of calculus for Lebesgue integrals and works under more general conditions than the classic version.
More concisely: Given a locally finite measure `μ`, function `f : ℝ → E`, and constants `a : ℝ`, `c : E`, if filters `l` and `l'` satisfy `[intervalIntegral.FTCFilter a l l']`, `f` has a finite limit `c` at the intersection of `l'` and almost everywhere with respect to `μ`, and the interval `(u, v]` approaches `l` in filter `lt`, then `∫[u,v] f dμ ≈ c * μ[(u,v)]` as `u` and `v` tend to `l`.
|
intervalIntegral.integral_hasDerivAt_right
theorem intervalIntegral.integral_hasDerivAt_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
ContinuousAt f b → HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
The Fundamental Theorem of Calculus-1 states that if a function `f : ℝ → E` is interval integrable on `a..b` and the function `f` is continuous at `b`, then the function `u ↦ ∫ x in a..u, f x` has a derivative `f b` at `b`. Here, `ℝ` represents the real number line, `E` is a normed additive commutative group that is also a normed space over the real numbers and is complete. The interval integrability of `f` considers the measure of the intervals `(a, b]` and `(b, a]`. The function is said to be strongly measurable at a filter (in this case the neighborhood of `b`) with respect to a measure. A function is said to be continuous at a point if the function's output value tends to the value at that point as the input tends to that point. The derivative of a function at a point is determined by how the function changes as we change the input values around that point.
More concisely: If a continuous, real-valued function `f` defined on a closed interval `[a, b]` is integrable on `[a, b]`, then the function `F(x) = ∫[a, x], f(t) dt` is differentiable at `x = b` with derivative `F'(b) = f(b)`.
|
intervalIntegral.integral_hasDerivWithinAt_right
theorem intervalIntegral.integral_hasDerivWithinAt_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {f : ℝ → E}
{a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
∀ {s t : Set ℝ} [inst_3 : intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
ContinuousWithinAt f t b → HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) s b
The theorem states the Fundamental Theorem of Calculus with respect to measures and filters. Essentially, it says that if a function `f` from the real numbers to some normed additive commutative group `E` is interval integrable with respect to the standard Lebesgue measure `volume` over an interval from `a` to `b`, then if `f(x)` is also continuous at `b` within a certain subset `t` of the real numbers, and `f` is strongly measurable at a filter of `b` within `t` with respect to `volume`, then the function `u ↦ ∫ x in a..u, f x` has a derivative at `b` within the set `s` and this derivative is `f(b)`. The condition `intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)` ensures that the technical conditions needed for the theorem are satisfied. The spaces involved are assumed to have the required algebraic and topological structure, including a norm on `E` and completeness of `E`.
More concisely: If a continuous and strongly measurable function `f` is interval integrable over an interval `[a, b]` with respect to the Lebesgue measure, then the function `x ↦ ∫ t in a..x, f t` has a derivative equal to `f(b)` at `x = b`.
|