Derivatives of parametric circle integrals

In this file we restate theorems about derivatives of integrals depending on parameters for circle integrals ∮ z in C(c, R), F x z. These are direct analogues of the corresponding results for interval integrals, but these take hypotheses on the circle as a set in ℂ instead of on the interval Set.uIoc 0 (2 * π).

One notable difference: some of the assumptions for interval integrals which only require properties to hold almost everywhere have been changed so that they must hold everywhere on the circle. This means they are slightly less general, but we suspect they will be easier to use in practice. In the worst case, users can always fall back to interval integrals.

theorem hasFDerivAt_circleIntegral_of_dominated_loc_of_lip {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℂ E] [SMulCommClass 𝕜 ℂ E] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : ℂ} {R : ℝ} {s : Set H} {bound : ℂ → ℝ} {F : H → ℂ → E} {F' : ℂ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F x (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (hF_int : CircleIntegrable (F x₀) c R) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F' (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (h_lip : ∀ z ∈ Metric.sphere c |R|, LipschitzOnWith ‖bound z‖₊ (fun (x : H) => F x z) s) (bound_integrable : CircleIntegrable bound c R) (h_diff : ∀ z ∈ Metric.sphere c |R|, HasFDerivAt (fun (x : H) => F x z) (F' z) x₀) : CircleIntegrable F' c R ∧ HasFDerivAt (fun (x : H) => ∮ (z : ℂ) in C(c, R), F x z) (∮ (z : ℂ) in C(c, R), F' z) x₀

Differentiation under a parametric circle integral for x ↦ ∮ z in C(c, R), F x z at a given point x₀, assuming F x₀ is circle integrable, x ↦ F x z is Lipschitz on a neighborhood of x₀ for every z on the circle (with a neighborhood independent of z) with circle integrable Lipschitz bound, and F x is a.e. strongly measurable along circleMap c R for x in a possibly smaller neighborhood of x₀.

theorem hasFDerivAt_circleIntegral_of_dominated_of_fderiv_le {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℂ E] [SMulCommClass 𝕜 ℂ E] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : ℂ} {R : ℝ} {s : Set H} {bound : ℂ → ℝ} {F : H → ℂ → E} {F' : H → ℂ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F x (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (hF_int : CircleIntegrable (F x₀) c R) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F' x₀ (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (h_bound : ∀ z ∈ Metric.sphere c |R|, ∀ x ∈ s, ‖F' x z‖ ≤ bound z) (bound_integrable : CircleIntegrable bound c R) (h_diff : ∀ z ∈ Metric.sphere c |R|, ∀ x ∈ s, HasFDerivAt (fun (x : H) => F x z) (F' x z) x) : HasFDerivAt (fun (x : H) => ∮ (z : ℂ) in C(c, R), F x z) (∮ (z : ℂ) in C(c, R), F' x₀ z) x₀

Differentiation under a parametric circle integral for x ↦ ∮ z in C(c, R), F x z at a given point x₀, assuming F x₀ is circle integrable, x ↦ F x z is differentiable on a neighborhood of x₀ for every z on the circle with derivative norm uniformly bounded by a circle integrable function (the neighborhood independent of z), and F x is a.e. strongly measurable along circleMap c R for x in a possibly smaller neighborhood of x₀.

theorem hasDerivAt_circleIntegral_of_dominated_loc_of_lip {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℂ E] [SMulCommClass 𝕜 ℂ E] {c : ℂ} {R : ℝ} {bound : ℂ → ℝ} {F : 𝕜 → ℂ → E} {F' : ℂ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F x (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (hF_int : CircleIntegrable (F x₀) c R) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F' (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (h_lipsch : ∀ z ∈ Metric.sphere c |R|, LipschitzOnWith ‖bound z‖₊ (fun (x : 𝕜) => F x z) s) (bound_integrable : CircleIntegrable bound c R) (h_diff : ∀ z ∈ Metric.sphere c |R|, HasDerivAt (fun (x : 𝕜) => F x z) (F' z) x₀) : CircleIntegrable F' c R ∧ HasDerivAt (fun (x : 𝕜) => ∮ (z : ℂ) in C(c, R), F x z) (∮ (z : ℂ) in C(c, R), F' z) x₀

Derivative under a parametric circle integral for x ↦ ∮ z in C(c, R), F x z at a given point x₀ : 𝕜, 𝕜 = ℝ or 𝕜 = ℂ, assuming F x₀ is circle integrable, x ↦ F x z is Lipschitz on a neighborhood of x₀ for every z on the circle (with a neighborhood independent of z) with circle integrable Lipschitz bound, and F x is a.e. strongly measurable along circleMap c R for x in a possibly smaller neighborhood of x₀.

theorem hasDerivAt_circleIntegral_of_dominated_loc_of_deriv_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℂ E] [SMulCommClass 𝕜 ℂ E] {c : ℂ} {R : ℝ} {bound : ℂ → ℝ} {F F' : 𝕜 → ℂ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F x (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (hF_int : CircleIntegrable (F x₀) c R) (hF'_meas : MeasureTheory.AEStronglyMeasurable (fun (θ : ℝ) => F' x₀ (circleMap c R θ)) (MeasureTheory.volume.restrict (Set.uIoc 0 (2 * Real.pi)))) (h_bound : ∀ z ∈ Metric.sphere c |R|, ∀ x ∈ s, ‖F' x z‖ ≤ bound z) (bound_integrable : CircleIntegrable bound c R) (h_diff : ∀ z ∈ Metric.sphere c |R|, ∀ x ∈ s, HasDerivAt (fun (x : 𝕜) => F x z) (F' x z) x) : CircleIntegrable (F' x₀) c R ∧ HasDerivAt (fun (x : 𝕜) => ∮ (z : ℂ) in C(c, R), F x z) (∮ (z : ℂ) in C(c, R), F' x₀ z) x₀

Derivative under a parametric circle integral for x ↦ ∮ z in C(c, R), F x z at a given point x₀ : 𝕜, 𝕜 = ℝ or 𝕜 = ℂ, assuming F x₀ is circle integrable, x ↦ F x z is differentiable on a neighborhood of x₀ for every z on the circle (with a neighborhood independent of z) with derivative uniformly bounded by a circle integrable function, and F x is a.e. strongly measurable along circleMap c R for x in a possibly smaller neighborhood of x₀.