hasDerivAt_integral_of_dominated_loc_of_lip
theorem hasDerivAt_integral_of_dominated_loc_of_lip :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
{E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E]
{bound : α → ℝ} {ε : ℝ} {F : 𝕜 → α → E} {x₀ : 𝕜} {F' : α → E},
0 < ε →
(∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
MeasureTheory.Integrable (F x₀) μ →
MeasureTheory.AEStronglyMeasurable F' μ →
(∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (Metric.ball x₀ ε)) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' a) x₀) →
MeasureTheory.Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
This theorem states that we can compute the derivative under the integral of a function `F(x, a)` at a given point `x₀`, where `𝕜` stands for either real numbers `ℝ` or complex numbers `ℂ`. The integral is computed with respect to a measure `μ` over a measurable space `α`. The assumptions for this theorem are:
1. The function `F` at `x₀` is integrable.
2. The function `F` is almost everywhere strongly measurable in a neighborhood of `x₀`.
3. The function `F(x, a)` is locally Lipschitz continuous on a ball around `x₀` for almost every `a` (with the radius of the ball independent of `a`), and the Lipschitz bound is integrable.
4. The derivative `F'` of `F` with respect to `x` is almost everywhere strongly measurable and integrable against `μ`.
Then, the theorem states that the function `F'` is integrable and the function `x ↦ ∫ F x a ∂μ` has a derivative at `x₀` which equals `∫ F' a ∂μ`, essentially allowing us to "swap" the order of integration and differentiation.
More concisely: Under the given assumptions, the derivative of the function `x ↦ ∫(F x) dμ(a)` exists at `x₀` and equals `∫(F' x) dμ(a)`.
|
hasDerivAt_integral_of_dominated_loc_of_deriv_le
theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
{E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E]
{bound : α → ℝ} {ε : ℝ} {F : 𝕜 → α → E} {x₀ : 𝕜},
0 < ε →
(∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
MeasureTheory.Integrable (F x₀) μ →
∀ {F' : 𝕜 → α → E},
MeasureTheory.AEStronglyMeasurable (F' x₀) μ →
(∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F' x a‖ ≤ bound a) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x) →
MeasureTheory.Integrable (F' x₀) μ ∧
HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
This theorem is about the differentiability under the integral of a function `F` mapping two variables `x` and `a` at a given point `x₀`. Under certain conditions, it asserts that the function `x ↦ ∫ F x a` has a derivative at `x₀`.
Here are the conditions for the theorem to hold:
- `x₀` is surrounded by an interval of positive radius `ε`.
- The function `F x` is almost everywhere strongly measurable with respect to measure `μ` for all `x` in the neighborhood of `x₀`.
- The function `F x₀` is integrable.
- There exists another function `F'` such that `F' x₀` is also almost everywhere strongly measurable with respect to measure `μ`, and the norm of `F' x a` is bounded by a function `bound a` for all `x` in the ball around `x₀` with radius `ε` and almost every `a` with respect to measure `μ`.
- This bounding function `bound` is integrable.
- The function `x ↦ F x a` has a derivative `F' x a` at every `x` in the ball around `x₀` with radius `ε` for almost every `a` with respect to measure `μ`.
If these conditions are met, then the function `F' x₀` is integrable and the function `x ↦ ∫ F x a` has a derivative at `x₀` equal to `∫ F' x₀ a`.
More concisely: Under the given conditions on the measurable function `F` and the measure `μ`, the function `x ↦ ∫ F x dμ` is differentiable at `x₀` with derivative `∫ F' x₀ dμ`, where `F'` is the derivative of `F` with respect to the first variable.
|
hasFDerivAt_integral_of_dominated_loc_of_lip'
theorem hasFDerivAt_integral_of_dominated_loc_of_lip' :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
{E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E]
{H : Type u_4} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ}
{ε : ℝ} {F' : α → H →L[𝕜] E},
0 < ε →
(∀ x ∈ Metric.ball x₀ ε, MeasureTheory.AEStronglyMeasurable (F x) μ) →
MeasureTheory.Integrable (F x₀) μ →
MeasureTheory.AEStronglyMeasurable F' μ →
(∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) →
MeasureTheory.Integrable F' μ ∧
HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
This theorem, `hasFDerivAt_integral_of_dominated_loc_of_lip'`, states that given a function `F: H → α → E`, a measure `μ` over `α`, and a point `x₀` in `H`, if the following conditions hold:
- `F x₀` is integrable with respect to `μ`,
- for every `x` in the ball of radius `ε` around `x₀`, `F x` is almost everywhere strongly measurable with respect to `μ`,
- there exists a function `F'` that is almost everywhere strongly measurable with respect to `μ` and, for almost every `a` in the measure space `α`, is the derivative of the function `x ↦ F x a` at `x₀`,
- there exists an integrable function `bound` such that for almost every `a` in the measure space `α`, the norm of the difference `F x a - F x₀ a` is at most `bound a * ‖x - x₀‖` for every `x` in the ball of radius `ε` around `x₀`,
then `F'` is integrable with respect to `μ` and the function `x ↦ ∫ F x a ∂μ` has `∫ F' a ∂μ` as its derivative at `x₀`. This theorem essentially states that under certain conditions, differentiation can be interchanged with integration.
More concisely: Under the given conditions, the derivative of the function `x ↦ ∫(F x ∂μ)` exists and is equal to `∫(F' ∂μ)` at `x₀`.
|
hasFDerivAt_integral_of_dominated_loc_of_lip
theorem hasFDerivAt_integral_of_dominated_loc_of_lip :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
{E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E]
{H : Type u_4} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ}
{ε : ℝ} {F' : α → H →L[𝕜] E},
0 < ε →
(∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
MeasureTheory.Integrable (F x₀) μ →
MeasureTheory.AEStronglyMeasurable F' μ →
(∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (Metric.ball x₀ ε)) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) →
MeasureTheory.Integrable F' μ ∧
HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
This theorem establishes conditions for differentiating under the integral of a function `F` at a given point `x₀`. It assumes that `F x₀` is integrable, the function `x ↦ F x a` is locally Lipschitz continuous on a ball around `x₀` for almost everywhere `a` (with a ball radius independent of `a`), and that the Lipschitz bound is integrable. It also assumes that `F x` is almost everywhere measurable for `x` in a potentially smaller neighborhood of `x₀`. If these conditions are met, then the theorem states that the function `F'` is integrable and the derivative of the function `x ↦ ∫ F x a` at `x₀` is the integral of `F'`.
More concisely: If `F` is a function satisfying certain integrability, measurability, and Lipschitz continuity conditions at `x₀`, then `F'` is integrable and the derivative of the function `x ↦ ∫₡ F x da` at `x₀` is equal to `∫₡ F'(x₀) da`.
|
hasFDerivAt_integral_of_dominated_of_fderiv_le
theorem hasFDerivAt_integral_of_dominated_of_fderiv_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
{E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E]
{H : Type u_4} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ}
{ε : ℝ} {F' : H → α → H →L[𝕜] E},
0 < ε →
(∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
MeasureTheory.Integrable (F x₀) μ →
MeasureTheory.AEStronglyMeasurable (F' x₀) μ →
(∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F' x a‖ ≤ bound a) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun x => F x a) (F' x a) x) →
HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
This theorem states that for a function `F` mapping from a normed additive commutative group `H` to a function from a measurable space `α` to a normed additive commutative group `E`, the derivative under the integral of `F` at a given point `x₀` can be established under certain conditions. These conditions include:
1. `F x₀` is integrable with respect to a measure `μ`.
2. `F` is differentiable on a ball around `x₀` (with a radius independent of `α`), almost everywhere with respect to `α`, and the derivative's norm is uniformly bounded by an integrable function.
3. `F x` is almost everywhere-measurable for values of `x` in a potentially smaller neighborhood of `x₀`.
The derivative is given by `∫ (a : α), F' x₀ a ∂μ`, where `F' x₀ a` is the derivative of `F x a` at `x₀`. This essentially states that under the above conditions, the derivative of the integral of `F` can be computed as the integral of the derivative of `F`, evaluated at `x₀`.
More concisely: Under the given conditions on a function `F` mapping from a normed additive commutative group to a measurable space to a normed additive commutative group, the derivative of the integral of `F` at a point `x₀` is equal to the integral of the derivative of `F` evaluated at `x₀`.
|