OAI/Analysis/AffineBernstein/EntireGraphComplete.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.graphEDist_le_segment_fderiv_bound line 18
2. lemma OAI.AffineBernstein.euclideanGraphComplete_entire line 51

   Source documentation

   An entire C∞ graph is complete for the literal induced Euclidean path metric, not merely for the ambient chord metric. Straight segments and a local derivative bound produce intrinsic convergence of every Cauchy sequence.

   lemma euclideanGraphComplete_entire {n : ℕ} {f : Space n → ℝ}
       (hf : ContDiff ℝ ∞ f) : EuclideanGraphComplete univ f := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete