OAI/Geometry/SurfaceImmersion/Primitive/PeriodicPrimitive.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The normalized periodic antiderivative used by the finite periodic expansion. The primitive is constructed by integration, followed by subtraction of its mean. The period is one, matching UnitAddCircle.

  1. def OAI.ClosedSurfaceR4.PeriodicPrimitive.rawPrimitive line 20
  2. def OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive line 22
  3. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.rawPrimitive_hasDerivAt line 25
  4. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.rawPrimitive_continuous line 29
  5. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.rawPrimitive_contDiff line 34
  6. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.rawPrimitive_periodic line 44
  7. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_hasDerivAt line 52
  8. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_continuous line 56
  9. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_contDiff line 60
  10. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_periodic line 65
  11. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.primitive_mean_zero line 71
  12. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.exists_smooth_periodic_primitive line 80

    Source documentation

    A smooth mean-zero periodic function has a smooth mean-zero periodic primitive, with no solvability hypothesis beyond its vanishing mean.

    theorem exists_smooth_periodic_primitive {f : ℝ → E} (hf : ContDiff ℝ ∞ f)
    (hperiod : Function.Periodic f 1) (hmean : (∫ t in 0..1, f t) = 0) :
    ∃ F : ℝ → E, ContDiff ℝ ∞ F ∧ Function.Periodic F 1 ∧
      (∀ x, HasDerivAt F (f x) x) ∧ (∫ t in 0..1, F t) = 0 :=
…
  13. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.integral_lift_eq_haar line 88
  14. theorem OAI.ClosedSurfaceR4.PeriodicPrimitive.exists_smooth_primitive_of_haar_mean_zero line 97

    Source documentation

    Vanishing normalized Haar mean gives a smooth mean-zero periodic primitive.

    theorem exists_smooth_primitive_of_haar_mean_zero {f : UnitAddCircle → E}
    (hf : ContDiff ℝ ∞ (fun t : ℝ => f (t : UnitAddCircle)))
    (hmean : (∫ t, f t ∂AddCircle.haarAddCircle) = 0) :
    ∃ F : ℝ → E, ContDiff ℝ ∞ F ∧ Function.Periodic F 1 ∧
      (∀ x : ℝ, HasDerivAt F (f (x : UnitAddCircle)) x) ∧ (∫ t in 0..1, F t) = 0 := by
…