Theorems · Theorem · real analysis

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₀ : 𝕜} {s : Set 𝕜},
  s ∈ nhds x₀ →
    (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
      MeasureTheory.Integrable (F x₀) μ →
        ∀ {F' : 𝕜 → α → E},
          MeasureTheory.AEStronglyMeasurable (F' x₀) μ →
            (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a) →
              MeasureTheory.Integrable bound μ →
                (∀ᵐ (a : α) ∂μ, ∀ x ∈ s, 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₀

Derivative under integral of x ↦ ∫ F x a at a given point x₀ : ℝ, assuming F x₀ is integrable, x ↦ F x a is differentiable on an interval around x₀ for ae a (with interval radius independent of a) with derivative uniformly bounded by an integrable function, and F x is ae-measurable for x in a possibly smaller neighborhood of x₀.

Defined in

Mathlib.Analysis.Calculus.ParametricIntegral

Cited by

4 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceRCLikeNormedAddCommGroupNormedSpaceNormedSpace