Space curves with a tangent line at every point

DefinitionTangent line to a closed space curve#✓fully proved

A 1-periodic continuous injective-on-[0, 1) curve γ : ℝ → ℝ³ has an (oriented) tangent line at t if there is a unit direction v such that every nearby secant vector γ s - γ t is arbitrarily close, relative to its length, to the line spanned by v.

def HasTangentLineAt (γ : ℝ → EuclideanSpace ℝ (Fin 3)) (t : ℝ) : Prop :=
  ∃ v : EuclideanSpace ℝ (Fin 3), ‖v‖ = 1 ∧
    ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧ ∀ s : ℝ,
      0 < |s - t| → |s - t| < δ →
      ‖(γ s - γ t) - ⟪γ s - γ t, v⟫_ℝ • v‖ ≤ ε * ‖γ s - γ t‖

Used by 1

Used byThe claim of Fréchet's Problem 117

DefinitionThe claim of Fréchet's Problem 117#✓fully proved

The claim of Fréchet's Problem 117 from the Scottish Book is the statement that for every \(1\)-periodic continuous map \(\gamma : \mathbb{R} \to \mathbb{R}^3\) that is injective on \([0, 1)\) and has a tangent line at every \(t \in \mathbb{R}\), there is a \(1\)-periodic continuous map \(p : \mathbb{R} \to \mathbb{R}^3\) that is injective on \([0, 1)\), has the same image as \(\gamma\), and is differentiable at every \(t \in \mathbb{R}\) with \(p'(t) \ne 0\).

def ScottishBookProblem117Claim : Prop :=
  ∀ γ : ℝ → EuclideanSpace ℝ (Fin 3),
    (∀ t, γ (t + 1) = γ t) →
    Continuous γ →
    Set.InjOn γ (Set.Ico (0 : ℝ) 1) →
    (∀ t, HasTangentLineAt γ t) →
    ∃ p : ℝ → EuclideanSpace ℝ (Fin 3),
      (∀ t, p (t + 1) = p t) ∧
      Continuous p ∧
      Set.InjOn p (Set.Ico (0 : ℝ) 1) ∧
      Set.range p = Set.range γ ∧
      ∀ t, DifferentiableAt ℝ p t ∧ deriv p t ≠ 0

Uses 1 · Used by 1

Statement usesTangent line to a closed space curve

Used byFréchet's Problem 117 has a negative answer

TheoremFréchet's Problem 117 has a negative answer#●ready to prove

There is a \(1\)-periodic continuous map \(\gamma : \mathbb{R} \to \mathbb{R}^3\), injective on \([0, 1)\), that has a tangent line at every parameter \(t\), such that no \(1\)-periodic continuous map \(p : \mathbb{R} \to \mathbb{R}^3\) that is injective on \([0, 1)\) and has the same image as \(\gamma\) is differentiable at every \(t\) with \(p'(t) \neq 0\).

Here \(\gamma\) has a tangent line at \(t\) when there is a unit vector \(v\) such that for every \(\varepsilon > 0\) there is \(\delta > 0\) with \(\|w - \langle w, v \rangle v\| \le \varepsilon \|w\|\), where \(w = \gamma(s) - \gamma(t)\), whenever \(0 < |s - t| < \delta\).

theorem_wanted frechet117_refuted : ¬ ScottishBookProblem117Claim

Sources

• M. Fréchet, Problem 117 of the Scottish Book; in general, no, by A. J. Ward, Fundamenta Mathematicae 28 (1937), cited in the typescript addendum Ad 117. Ward also gives a representation whose derivatives exist and are not all zero except on a null set of parameter values whose points have Carathéodory measure zero.

Uses 1

Statement usesThe claim of Fréchet's Problem 117

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.