OAI/Geometry/SurfaceImmersion/Primitive/PeriodicCalculus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.PeriodicCalculus.exists_circle_primitive line 21

   Source documentation

   The real primitive descends to the circle without losing smoothness or its normalization.

   theorem exists_circle_primitive {f : Period → E}
       (hf : ContDiff ℝ ∞ (fun t : ℝ => f (t : Period)))
       (hm : (∫ t, f t ∂AddCircle.haarAddCircle) = 0) :
       ∃ F : Period → E, Continuous F ∧
         ContDiff ℝ ∞ (fun t : ℝ => F (t : Period)) ∧
         (∫ t, F t ∂AddCircle.haarAddCircle) = 0 ∧
         ∀ t : ℝ, HasDerivAt (fun s : ℝ => F (s : Period)) (f (t : Period)) t := by
   …

2. lemma OAI.ClosedSurfaceR4.PeriodicCalculus.periodic_deriv line 36
3. theorem OAI.ClosedSurfaceR4.PeriodicCalculus.exists_circle_derivative line 44

   Source documentation

   A smooth circle function has a smooth circle derivative of mean zero.

   theorem exists_circle_derivative {f : Period → E}
       (hf : ContDiff ℝ ∞ (fun t : ℝ => f (t : Period))) :
       ∃ D : Period → E, Continuous D ∧
         ContDiff ℝ ∞ (fun t : ℝ => D (t : Period)) ∧
         (∫ t, D t ∂AddCircle.haarAddCircle) = 0 ∧
         ∀ t : ℝ, HasDerivAt (fun s : ℝ => f (s : Period)) (D (t : Period)) t := by
   …