LocalPeriodicPrimitive.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Smooth normalized primitives on the open admissible parameter domain.

theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.contDiffOn_primitive_joint line 20

Source documentation

The primitive is jointly smooth wherever the parameter family is smooth.

theorem contDiffOn_primitive_joint {F : P × ℝ → E} {S : Set P} (hS : IsOpen S)
    (hF : ContDiffOn ℝ ∞ F (S ×ˢ univ)) :
    ContDiffOn ℝ ∞ (fun z : P × ℝ => primitive (fun t => F (z.1, t)) z.2) (S ×ˢ univ) := by
…