Theorems · Theorem · real analysis

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

Derivative under integral of x ↦ ∫ F x a at a given point x₀ : 𝕜, 𝕜 = ℝ or 𝕜 = ℂ, assuming F x₀ is integrable, x ↦ F x a is locally Lipschitz on 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

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceRCLikeNormedAddCommGroupNormedSpaceNormedSpace