SmoothParameterIntegral.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

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

def OAI.ClosedSurfaceR4.SmoothParameterIntegral.partialDerivative line 18
lemma OAI.ClosedSurfaceR4.SmoothParameterIntegral.contDiff_partialDerivative line 22
lemma OAI.ClosedSurfaceR4.SmoothParameterIntegral.partial_hasFDerivAt line 27
theorem OAI.ClosedSurfaceR4.SmoothParameterIntegral.hasFDerivAt_integral line 37
Source documentation
Compactness gives the domination required to differentiate under the integral. No uniform derivative bound is an extra premise.
```
theorem hasFDerivAt_integral {F : P × ℝ → E} (hF : ContDiff ℝ ∞ F)
    (a b : ℝ) (p₀ : P) :
    HasFDerivAt (fun p => ∫ t in a..b, F (p, t))
      (∫ t in a..b, partialDerivative F (p₀, t)) p₀ := by
…
```
Mentions: OAI.ClosedSurfaceR4.SmoothParameterIntegral.partialDerivative

theorem OAI.ClosedSurfaceR4.SmoothParameterIntegral.contDiff_integral_nat line 62

Source documentation

Induction on derivative order; the target Banach space is allowed to change to a continuous-linear-map space at each induction step.

theorem contDiff_integral_nat (a b : ℝ) (n : ℕ) :
    ∀ (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
      (F : P × ℝ → E), ContDiff ℝ ∞ F →
      ContDiff ℝ n (fun p => ∫ t in a..b, F (p, t)) := by
…

theorem OAI.ClosedSurfaceR4.SmoothParameterIntegral.contDiff_integral line 81
Source documentation
Integrating a smooth family on a fixed compact interval preserves all orders of smoothness.
```
theorem contDiff_integral {F : P × ℝ → E} (hF : ContDiff ℝ ∞ F) (a b : ℝ) :
    ContDiff ℝ ∞ (fun p => ∫ t in a..b, F (p, t)) := by
…
```