OAI/Analysis/AffineBernstein/CompactDifferentiation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.hasDerivAt_setIntegral_compact line 16

   Source comment

   Differentiation over a fixed compact set from smoothness in a neighbourhood of the zero-parameter slice. The uniform bound is obtained by compactness.

   theorem hasDerivAt_setIntegral_compact {K : Set E} (hK : IsCompact K)
       {U : Set (ℝ × E)} (hU : IsOpen U) (h0K : {0} ×ˢ K ⊆ U)
       {F : ℝ × E → ℝ} (hF : ContDiffOn ℝ ∞ F U) :
       HasDerivAt (fun t : ℝ => ∫ x in K, F (t,x) ∂μ)
         (∫ x in K, fderiv ℝ F (0,x) (1,0) ∂μ) 0 := by
   …