Smooth parameter dependence of an actual integral over a compact interval.

noncomputable def EulerCompactParameterIntegral.parameterDerivative {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : X × ℝ → E) (p : X × ℝ) : X →L[ℝ] E

Parameter derivative, given by (fderiv ℝ F p).comp (ContinuousLinearMap.inl ℝ X ℝ).

Equations

• EulerCompactParameterIntegral.parameterDerivative F p = fderiv ℝ F p ∘SL ContinuousLinearMap.inl ℝ X ℝ

theorem EulerCompactParameterIntegral.parameterDerivative_contDiff {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : X × ℝ → E) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (parameterDerivative F)

theorem EulerCompactParameterIntegral.integral_hasFDerivAt {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [ProperSpace X] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (hab : a ≤ b) (F : X × ℝ → E) (hF : ContDiff ℝ (↑⊤) F) (x : X) : HasFDerivAt (fun (y : X) => ∫ (t : ℝ) in a..b, F (y, t)) (∫ (t : ℝ) in a..b, parameterDerivative F (x, t)) x

theorem EulerCompactParameterIntegral.integral_contDiff_finite {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [ProperSpace X] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (a b : ℝ) (hab : a ≤ b) (F : X × ℝ → E) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ ↑n fun (y : X) => ∫ (t : ℝ) in a..b, F (y, t)

theorem EulerCompactParameterIntegral.integral_contDiff {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [ProperSpace X] {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a b : ℝ) (hab : a ≤ b) (F : X × ℝ → E) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ ↑⊤ fun (y : X) => ∫ (t : ℝ) in a..b, F (y, t)