Documentation

Mathlib.Analysis.Calculus.ParametricIntervalIntegral

Derivatives of interval integrals depending on parameters #

In this file we restate theorems about derivatives of integrals depending on parameters for interval integrals.

theorem intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip {๐•œ : Type u_1} [IsROrC ๐•œ] {ฮผ : MeasureTheory.Measure โ„} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace โ„ E] [NormedSpace ๐•œ E] [CompleteSpace E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace ๐•œ H] {a : โ„} {b : โ„} {ฮต : โ„} {bound : โ„ โ†’ โ„} {F : H โ†’ โ„ โ†’ E} {F' : โ„ โ†’ H โ†’L[๐•œ] E} {xโ‚€ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : H) in nhds xโ‚€, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (hF_int : IntervalIntegrable (F xโ‚€) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (h_lip : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ ฮ™ a b โ†’ LipschitzOnWith (Real.nnabs (bound t)) (fun (x : H) => F x t) (Metric.ball xโ‚€ ฮต)) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ ฮ™ a b โ†’ HasFDerivAt (fun (x : H) => F x t) (F' t) xโ‚€) :
IntervalIntegrable F' ฮผ a b โˆง HasFDerivAt (fun (x : H) => โˆซ (t : โ„) in a..b, F x t โˆ‚ฮผ) (โˆซ (t : โ„) in a..b, F' t โˆ‚ฮผ) xโ‚€

Differentiation under integral of x โ†ฆ โˆซ t in a..b, F x t at a given point xโ‚€, assuming F xโ‚€ is integrable, x โ†ฆ F x a is locally Lipschitz on a ball around xโ‚€ for ae a (with a ball radius independent of a) with integrable Lipschitz bound, and F x is ae-measurable for x in a possibly smaller neighborhood of xโ‚€.

theorem intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le {๐•œ : Type u_1} [IsROrC ๐•œ] {ฮผ : MeasureTheory.Measure โ„} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace โ„ E] [NormedSpace ๐•œ E] [CompleteSpace E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace ๐•œ H] {a : โ„} {b : โ„} {ฮต : โ„} {bound : โ„ โ†’ โ„} {F : H โ†’ โ„ โ†’ E} {F' : H โ†’ โ„ โ†’ H โ†’L[๐•œ] E} {xโ‚€ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : H) in nhds xโ‚€, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (hF_int : IntervalIntegrable (F xโ‚€) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' xโ‚€) (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (h_bound : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ ฮ™ a b โ†’ โˆ€ x โˆˆ Metric.ball xโ‚€ ฮต, โ€–F' x tโ€– โ‰ค bound t) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ ฮ™ a b โ†’ โˆ€ x โˆˆ Metric.ball xโ‚€ ฮต, HasFDerivAt (fun (x : H) => F x t) (F' x t) x) :
HasFDerivAt (fun (x : H) => โˆซ (t : โ„) in a..b, F x t โˆ‚ฮผ) (โˆซ (t : โ„) in a..b, F' xโ‚€ t โˆ‚ฮผ) xโ‚€

Differentiation under integral of x โ†ฆ โˆซ F x a at a given point xโ‚€, assuming F xโ‚€ is integrable, x โ†ฆ F x a is differentiable on a ball around xโ‚€ for ae a with derivative norm uniformly bounded by an integrable function (the ball radius is independent of a), and F x is ae-measurable for x in a possibly smaller neighborhood of xโ‚€.

theorem intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip {๐•œ : Type u_1} [IsROrC ๐•œ] {ฮผ : MeasureTheory.Measure โ„} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace โ„ E] [NormedSpace ๐•œ E] [CompleteSpace E] {a : โ„} {b : โ„} {ฮต : โ„} {bound : โ„ โ†’ โ„} {F : ๐•œ โ†’ โ„ โ†’ E} {F' : โ„ โ†’ E} {xโ‚€ : ๐•œ} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : ๐•œ) in nhds xโ‚€, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (hF_int : IntervalIntegrable (F xโ‚€) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (h_lipsch : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ ฮ™ a b โ†’ LipschitzOnWith (Real.nnabs (bound t)) (fun (x : ๐•œ) => F x t) (Metric.ball xโ‚€ ฮต)) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โˆ€แต (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โ‚€

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 ball around xโ‚€ for ae a (with ball radius independent of a) with integrable Lipschitz bound, and F x is ae-measurable for x in a possibly smaller neighborhood of xโ‚€.

theorem intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le {๐•œ : Type u_1} [IsROrC ๐•œ] {ฮผ : MeasureTheory.Measure โ„} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace โ„ E] [NormedSpace ๐•œ E] [CompleteSpace E] {a : โ„} {b : โ„} {ฮต : โ„} {bound : โ„ โ†’ โ„} {F : ๐•œ โ†’ โ„ โ†’ E} {F' : ๐•œ โ†’ โ„ โ†’ E} {xโ‚€ : ๐•œ} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : ๐•œ) in nhds xโ‚€, MeasureTheory.AEStronglyMeasurable (F x) (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (hF_int : IntervalIntegrable (F xโ‚€) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' xโ‚€) (MeasureTheory.Measure.restrict ฮผ (ฮ™ a b))) (h_bound : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ ฮ™ a b โ†’ โˆ€ x โˆˆ Metric.ball xโ‚€ ฮต, โ€–F' x tโ€– โ‰ค bound t) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โˆ€แต (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โ‚€

Derivative under integral of x โ†ฆ โˆซ F x a at a given point xโ‚€ : ๐•œ, ๐•œ = โ„ or ๐•œ = โ„‚, 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โ‚€.