OAI/Geometry/SurfaceImmersion/Correction/SmoothPeriodicPrimitive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Jointly smooth normalized primitives with parameters.

  1. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.contDiff_rawPrimitive_joint line 19
  2. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.contDiff_primitive_joint line 36

    Source documentation

    Normalization by the mean preserves joint smoothness in the parameter and the real periodic argument.

    theorem contDiff_primitive_joint {F : P × ℝ → E} (hF : ContDiff ℝ ∞ F) :
    ContDiff ℝ ∞ (fun z : P × ℝ => primitive (fun t => F (z.1, t)) z.2) := by
…

    Mentions: OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive

  3. lemma OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_zero line 43
  4. lemma OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_zero_at_parameter line 48