mathlib documentation

analysis.calculus.parametric_interval_integral

Derivatives of interval integrals depending on parameters #

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

theorem interval_integral.has_fderiv_at_integral_of_dominated_loc_of_lip {๐•œ : Type u_1} [is_R_or_C ๐•œ] {ฮผ : measure_theory.measure โ„} {E : Type u_2} [normed_group E] [normed_space โ„ E] [normed_space ๐•œ E] [complete_space E] {H : Type u_3} [normed_group H] [normed_space ๐•œ H] {a b ฮต : โ„} {bound : โ„ โ†’ โ„} {F : H โ†’ โ„ โ†’ E} {F' : โ„ โ†’ (H โ†’L[๐•œ] E)} {xโ‚€ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : H) in nhds xโ‚€, measure_theory.ae_strongly_measurable (F x) (ฮผ.restrict (set.interval_oc a b))) (hF_int : interval_integrable (F xโ‚€) ฮผ a b) (hF'_meas : measure_theory.ae_strongly_measurable F' (ฮผ.restrict (set.interval_oc a b))) (h_lip : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ lipschitz_on_with (โ‡‘real.nnabs (bound t)) (ฮป (x : H), F x t) (metric.ball xโ‚€ ฮต)) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ has_fderiv_at (ฮป (x : H), F x t) (F' t) xโ‚€) :
interval_integrable F' ฮผ a b โˆง has_fderiv_at (ฮป (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 interval_integral.has_fderiv_at_integral_of_dominated_of_fderiv_le {๐•œ : Type u_1} [is_R_or_C ๐•œ] {ฮผ : measure_theory.measure โ„} {E : Type u_2} [normed_group E] [normed_space โ„ E] [normed_space ๐•œ E] [complete_space E] {H : Type u_3} [normed_group H] [normed_space ๐•œ H] {a b ฮต : โ„} {bound : โ„ โ†’ โ„} {F : H โ†’ โ„ โ†’ E} {F' : H โ†’ โ„ โ†’ (H โ†’L[๐•œ] E)} {xโ‚€ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : H) in nhds xโ‚€, measure_theory.ae_strongly_measurable (F x) (ฮผ.restrict (set.interval_oc a b))) (hF_int : interval_integrable (F xโ‚€) ฮผ a b) (hF'_meas : measure_theory.ae_strongly_measurable (F' xโ‚€) (ฮผ.restrict (set.interval_oc a b))) (h_bound : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ โˆ€ (x : H), x โˆˆ metric.ball xโ‚€ ฮต โ†’ โˆฅF' x tโˆฅ โ‰ค bound t) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ โˆ€ (x : H), x โˆˆ metric.ball xโ‚€ ฮต โ†’ has_fderiv_at (ฮป (x : H), F x t) (F' x t) x) :
has_fderiv_at (ฮป (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 interval_integral.has_deriv_at_integral_of_dominated_loc_of_lip {๐•œ : Type u_1} [is_R_or_C ๐•œ] {ฮผ : measure_theory.measure โ„} {E : Type u_2} [normed_group E] [normed_space โ„ E] [normed_space ๐•œ E] [complete_space E] {a b ฮต : โ„} {bound : โ„ โ†’ โ„} {F : ๐•œ โ†’ โ„ โ†’ E} {F' : โ„ โ†’ E} {xโ‚€ : ๐•œ} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : ๐•œ) in nhds xโ‚€, measure_theory.ae_strongly_measurable (F x) (ฮผ.restrict (set.interval_oc a b))) (hF_int : interval_integrable (F xโ‚€) ฮผ a b) (hF'_meas : measure_theory.ae_strongly_measurable F' (ฮผ.restrict (set.interval_oc a b))) (h_lipsch : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ lipschitz_on_with (โ‡‘real.nnabs (bound t)) (ฮป (x : ๐•œ), F x t) (metric.ball xโ‚€ ฮต)) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ has_deriv_at (ฮป (x : ๐•œ), F x t) (F' t) xโ‚€) :
interval_integrable F' ฮผ a b โˆง has_deriv_at (ฮป (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 interval_integral.has_deriv_at_integral_of_dominated_loc_of_deriv_le {๐•œ : Type u_1} [is_R_or_C ๐•œ] {ฮผ : measure_theory.measure โ„} {E : Type u_2} [normed_group E] [normed_space โ„ E] [normed_space ๐•œ E] [complete_space E] {a b ฮต : โ„} {bound : โ„ โ†’ โ„} {F F' : ๐•œ โ†’ โ„ โ†’ E} {xโ‚€ : ๐•œ} (ฮต_pos : 0 < ฮต) (hF_meas : โˆ€แถ  (x : ๐•œ) in nhds xโ‚€, measure_theory.ae_strongly_measurable (F x) (ฮผ.restrict (set.interval_oc a b))) (hF_int : interval_integrable (F xโ‚€) ฮผ a b) (hF'_meas : measure_theory.ae_strongly_measurable (F' xโ‚€) (ฮผ.restrict (set.interval_oc a b))) (h_bound : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ โˆ€ (x : ๐•œ), x โˆˆ metric.ball xโ‚€ ฮต โ†’ โˆฅF' x tโˆฅ โ‰ค bound t) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โˆ€แต (t : โ„) โˆ‚ฮผ, t โˆˆ set.interval_oc a b โ†’ โˆ€ (x : ๐•œ), x โˆˆ metric.ball xโ‚€ ฮต โ†’ has_deriv_at (ฮป (x : ๐•œ), F x t) (F' x t) x) :
interval_integrable (F' xโ‚€) ฮผ a b โˆง has_deriv_at (ฮป (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โ‚€.