Theorems · Theorem · real analysis

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 : α → ℝ} {s : Set H}
  {F' : α → H →L[𝕜] E},
  s ∈ nhds x₀ →
    (∀ᶠ (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) s) →
            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₀

Differentiation under integral of x ↦ ∫ F x a at a given point x₀, assuming F x₀ is integrable, x ↦ F x a is locally Lipschitz in a neighborhood of x₀ for ae a (with a neighborhood independent of a) with integrable Lipschitz bound, 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 262 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceRCLikeNormedAddCommGroupNormedSpaceNormedSpaceNormedAddCommGroupNormedSpace