LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Calculus.ParametricIntervalIntegral

`intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip` theorem intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {a b ε : ℝ} {bound : ℝ → ℝ} {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜}, 0 < ε → (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) → IntervalIntegrable (F x₀) μ a b → MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Ι a b)) → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)) → IntervalIntegrable bound μ a b → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasDerivAt (fun x => F x t) (F' t) x₀) → IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀ This theorem states that the function `x ↦ ∫ F x a` has a derivative at a given point `x₀` in either the real or complex number system, under the following conditions: - The function `F x₀` is interval integrable. - The function `x ↦ F x a` is Lipschitz continuous in a neighborhood around `x₀` for almost every `a`, with the size of the neighborhood being independent of `a`, and the Lipschitz bound is also integrable. - The function `F x` is almost everywhere measurable for `x` in a potentially smaller neighborhood around `x₀`. - The function `F'` is almost everywhere strongly measurable and interval integrable. - The function `F x` has a derivative `F'` at `x₀` for almost every `t` in the interval. In this case, the derivative of the integral function at `x₀` is the integral of `F'` over the interval. More concisely: Given a function `F` that is interval integrable, Lipschitz continuous with an integrable Lipschitz constant, almost everywhere measurable, and has a almost everywhere defined derivative `F'` that is interval integrable, then the function `x ↦ ∫ F x a` has a derivative at `x₀` equal to `∫ F' x dx`.
`intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip` theorem intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {H : Type u_3} [inst_4 : NormedAddCommGroup H] [inst_5 : NormedSpace 𝕜 H] {a b ε : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H}, 0 < ε → (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) → IntervalIntegrable (F x₀) μ a b → MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Ι a b)) → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)) → IntervalIntegrable bound μ a b → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀) → IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀ The theorem `intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip` states that differentiation under the integral of a function $x \mapsto \int_{a}^{b} F(x, t) dt$ at a given point $x_0$ exists, given certain conditions. These conditions are: - the function $F(x_0, \cdot)$ is interval integrable, - the function $x \mapsto F(x, a)$ is locally Lipschitz continuous on a ball around $x_0$ for almost every $a$, with the radius of this ball being independent of $a$, and the Lipschitz constant is integrable, - the function $F(x, \cdot)$ is almost everywhere strongly measurable for $x$ in a possibly smaller neighborhood of $x_0$, - the derivative of the function $x \mapsto F(x, t)$ at $x_0$ exists for almost every $t$ in the interval $a$ to $b$. The theorem then concludes that the function $F'(x,\cdot)$ is interval integrable and the derivative of the function $x \mapsto \int_{a}^{b} F(x, t) dt$ at $x_0$ exists, and is equal to $\int_{a}^{b} F'(x, t) dt$. More concisely: If $F(x,t)$ is a function that is locally Lipschitz continuous and integrable in the first variable at $x_0$ for almost every $a$, strongly measurable in the second variable for $x$ near $x_0$, and has a derivative in the second variable that is integrable, then the function $x \mapsto \int\_a^b F(x,t) dt$ is differentiable at $x_0$ and its derivative is $\int\_a^b F'(x,t) dt$.
`intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le` theorem intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {H : Type u_3} [inst_4 : NormedAddCommGroup H] [inst_5 : NormedSpace 𝕜 H] {a b ε : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[𝕜] E} {x₀ : H}, 0 < ε → (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) → IntervalIntegrable (F x₀) μ a b → MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)) → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, ‖F' x t‖ ≤ bound t) → IntervalIntegrable bound μ a b → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x) → HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀ The theorem `intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le` states the following in natural language: Given an ordered field `𝕜`, a measure `μ` on the real numbers, normed addition commutative groups `E` and `H`, a real number interval `a..b`, a non-negative real number `ε`, a bounding function `bound`, and functions `F : H → ℝ → E` and `F' : H → ℝ → H →L[𝕜] E`, as well as a point `x₀` in `H`. Assuming the following conditions are met: 1. The function `F x₀` is interval integrable with respect to `μ` on `a..b`. 2. The function `F x` is almost everywhere strongly measurable, for almost every `x` in a neighborhood of `x₀`. 3. The function `F' x₀` is also almost everywhere strongly measurable. 4. The norm of derivative `F' x t` is uniformly bounded by an integrable function `bound` 5. For almost every `t` in `a..b` and for every `x` in a ball around `x₀` with radius `ε`, the function `F x t` has `F' x t` as its derivative at `x`. Then, the function `x ↦ ∫ F x t ∂μ` for `t` in `a..b`, has its derivative at `x₀` equal to `∫ F' x₀ t ∂μ` for `t` in `a..b`. This theorem essentially allows us to differentiate under the integral sign, under certain conditions. More concisely: If `F` is a function satisfying the given conditions, then the function `x ↦ ∫(F x t) dμ for t in a..b` has a derivative at `x₀` equal to `∫(F' x₀ t) dμ for t in a..b`.
`intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le` theorem intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {a b ε : ℝ} {bound : ℝ → ℝ} {F F' : 𝕜 → ℝ → E} {x₀ : 𝕜}, 0 < ε → (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) → IntervalIntegrable (F x₀) μ a b → MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)) → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, ‖F' x t‖ ≤ bound t) → IntervalIntegrable bound μ a b → (∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ Metric.ball x₀ ε, HasDerivAt (fun x => F x t) (F' x t) x) → IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀ This theorem states that under certain conditions, the derivative of the integral function `x ↦ ∫ F x a` at a given point `x₀ : 𝕜` (where `𝕜` is either `ℝ` or `ℂ`) exists. The conditions are as follows: 1. `F x₀` is integrable over the range `[a, b]` with respect to measure `μ`. 2. The function `x ↦ F x a` is differentiable on an interval around `x₀` for almost every `a`, where the radius of the interval is independent of `a`. The derivative is uniformly bounded by an integrable function. 3. `F x` is almost everywhere strongly measurable for `x` in a possibly smaller neighborhood of `x₀`. 4. The function `F' x₀`, which is assumed to be the derivative of `F x a` with respect to `x`, is also almost everywhere strongly measurable over the interval `[a, b]`. 5. For almost every `t` in `[a, b]`, for every `x` in a ball of radius `ε` centered at `x₀`, the norm of `F' x t` is less or equal to a given bound function. Under these conditions, the theorem concludes two things: 1. `F' x₀` is interval-integrable over `[a, b]`. 2. The function `x ↦ ∫ F x a` has derivative at `x₀`, and this derivative is equal to the integral of `F' x₀` over `[a, b]`. More concisely: Under certain conditions on the integrable function `F` and its derivative, the integral function `x ↦ ∫ F x a` has a derivative at `x₀`, which is equal to the integral of `F' x₀` over `[a, b]`.