OAI/Geometry/SurfaceImmersion/Correction/SmoothZeroFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact smooth division by a real coordinate vanishing at one point.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smoothZeroFactor line 13
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smoothZeroFactor_smooth line 16
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smoothZeroFactor_identity line 23
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smoothZeroFactor_self line 36
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.two_zero_smooth_factor line 41

    Source documentation

    Division by two distinct simple-zero coordinates is globally smooth.

    theorem two_zero_smooth_factor {f : ℝ → V} (hf : ContDiff ℝ ∞ f)
    {p q : ℝ} (hpq : p ≠ q) (hp : f p = 0) (hq : f q = 0) :
    ∃ d : ℝ → V, ContDiff ℝ ∞ d ∧
      (∀ t, f t = ((t-p)*(t-q)) • d t) ∧
      deriv f p = (p-q) • d p ∧ deriv f q = (q-p) • d q := by
…