ParametricIntegralC1

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Differentiating compact parametric integrals

This file supplies the fixed-compact-set calculus bridge used to construct scalar primitives for divergence-form forcing. Mathlib provides differentiation under the integral and continuity of compact parametric integrals separately; the theorem below packages them into a C¹ result on Vec d.

theorem DivergenceFormProcess.contDiff_one_setIntegral_of_continuous_hasFDerivAt {d : ℕ} {K : Set ℝ} (hK : IsCompact K) {F : HCPolySupport.Vec d → ℝ → ℝ} {F' : HCPolySupport.Vec d → ℝ → HCPolySupport.Vec d →L[ℝ] ℝ} (hF : Continuous (Function.uncurry F)) (hF' : Continuous (Function.uncurry F')) (hdiff : ∀ (x : HCPolySupport.Vec d) (t : ℝ), HasFDerivAt (fun (y : HCPolySupport.Vec d) => F y t) (F' x t) x) : ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => ∫ (t : ℝ) in K, F x t

A jointly continuous family of scalar functions with a jointly continuous Fréchet derivative can be integrated over a compact real set without losing C¹ regularity in the Vec d parameter.