From 80c9ce7ed15b0f624a56cbdc71a57b6f71e42c18 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sat, 26 Sep 2026 22:04:22 +0800 Subject: [PATCH 1/2] =?UTF-8?q?feat(Analysis):=20from=20C=C2=B9-manifold?= =?UTF-8?q?=20to=20real=20analytic?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanEval/Analysis/C1ToAnalytic.lean | 57 +++++++++++++++++++++++++++++ manifests/problems/c1_analytic.toml | 15 ++++++++ 2 files changed, 72 insertions(+) create mode 100644 LeanEval/Analysis/C1ToAnalytic.lean create mode 100644 manifests/problems/c1_analytic.toml diff --git a/LeanEval/Analysis/C1ToAnalytic.lean b/LeanEval/Analysis/C1ToAnalytic.lean new file mode 100644 index 000000000..0f8ab0be8 --- /dev/null +++ b/LeanEval/Analysis/C1ToAnalytic.lean @@ -0,0 +1,57 @@ +import Mathlib +import EvalTools.Markers + +/-! +# From C¹-manifold to real analytic + +If 1 ≤ k ≤ n where k and n are integers, ∞ or ω, every Cᵏ-structure on a (paracompact, Hausdorff) +manifold can be upgraded to a compatible Cⁿ structure, and uniquely so in the sense that any +two Cⁿ-structures inducing the given Cᵏ-structure are connected by an isotopy through +Cᵏ-diffeomorphisms. + +This essentially says the classification of Cᵏ-manifolds (k ≥ 1) is the same problem as +the classification of smooth (or real analytic) manifolds. + +## References + +* Koji Shiga. Some aspects of real-analytic manifolds and differentiable manifolds. + J. Math. Soc. Japan 16(2): 128-142 (April, 1964). DOI: 10.2969/jmsj/01620128 + +* https://mathoverflow.net/questions/8789/can-every-manifold-be-given-an-analytic-structure/8799 + mentions work of Morrey, Grauert and Whitney in the real analytic case. + +* https://en.wikipedia.org/wiki/Differential_structure#Existence_and_uniqueness_theorems +-/ + +namespace LeanEval.Analysis.C1ToAnalytic + +variable (k n : WithTop ℕ∞) +variable (M N V W : Type*) [TopologicalSpace M] [TopologicalSpace N] +variable [NormedAddCommGroup V] [NormedSpace ℝ V] +variable [NormedAddCommGroup W] [NormedSpace ℝ W] + +open scoped Manifold + +/-- A Cᵏ-structure on a manifold can be upgraded to a compatible Cⁿ-structure if `1 ≤ k ≤ n` +(if `n ≤ k` this is trivial). We use two isomorphic model vector spaces V and W in the statement +to avoid introducing two `ChartedSpace V M` instances. The `k ≥ n` case is trivial. -/ +@[eval_problem] +theorem exists_isManifold_of_le (hk : 1 ≤ k) [FiniteDimensional ℝ V] (e : V ≃ₗ[ℝ] W) + [ChartedSpace V M] [IsManifold 𝓘(ℝ,V) k M] [T2Space M] [ParacompactSpace M] : + ∃ (_ : ChartedSpace W M) (_ : IsManifold 𝓘(ℝ,W) n M) + (f : M ≃ₘ^k⟮𝓘(ℝ,V), 𝓘(ℝ,W)⟯ M), f.toHomeomorph = .refl _ := by + sorry + +/-- If `1 ≤ k ≤ n`, then any Cᵏ-diffeomorphism between two Cⁿ-manifolds is Cᵏ-isotopic to a +Cⁿ-diffeomorphism via Cᵏ-diffeomorphisms. Again, this is probably trivially true fo `n ≤ k`, +and the model spaces are automatically isomorphic given the diffeomorphism unless both spaces +are empty. -/ +@[eval_problem] +theorem exists_homotopy_of_diffeomorph (hk : 1 ≤ k) (hkn : k ≤ n) [FiniteDimensional ℝ V] + [ChartedSpace V M] [IsManifold 𝓘(ℝ,V) n M] [ChartedSpace W N] [IsManifold 𝓘(ℝ,W) n N] + [T2Space M] [ParacompactSpace M] (e : V ≃ₗ[ℝ] W) (f : M ≃ₘ^k⟮𝓘(ℝ,V), 𝓘(ℝ,W)⟯ N) : + ∃ H : ℝ × M → N, ContMDiff (𝓘(ℝ,ℝ).prod 𝓘(ℝ,V)) 𝓘(ℝ,W) k H ∧ + (H ⟨0, ·⟩) = f ∧ ∃ g : M ≃ₘ^n⟮𝓘(ℝ,V), 𝓘(ℝ,W)⟯ N, (H ⟨1, ·⟩) = g := by + sorry + +end LeanEval.Analysis.C1ToAnalytic diff --git a/manifests/problems/c1_analytic.toml b/manifests/problems/c1_analytic.toml new file mode 100644 index 000000000..2f6ce421a --- /dev/null +++ b/manifests/problems/c1_analytic.toml @@ -0,0 +1,15 @@ +id = "c1_analytic" +title = "From C¹-manifold to real analytic" +group = "formalization-evaluation" +status = "archived" +visible = true +statement_revision = 1 +tags = [] +module = "LeanEval.Analysis.C1ToAnalytic" +holes = ["exists_isManifold_of_le", "exists_homotopy_of_diffeomorph"] +submitter = "Junyan Xu" + +[[status_history]] +status = "archived" +effective_date = "2026-09-26" +reason = "policy" From 7a177a4dcd0f3b15b11eae16161a232e00abd109 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 27 Sep 2026 00:23:04 +0800 Subject: [PATCH 2/2] add comment and remove namespace causing CI failure --- LeanEval/Analysis/C1ToAnalytic.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/LeanEval/Analysis/C1ToAnalytic.lean b/LeanEval/Analysis/C1ToAnalytic.lean index 0f8ab0be8..d3e71866d 100644 --- a/LeanEval/Analysis/C1ToAnalytic.lean +++ b/LeanEval/Analysis/C1ToAnalytic.lean @@ -12,6 +12,11 @@ Cᵏ-diffeomorphisms. This essentially says the classification of Cᵏ-manifolds (k ≥ 1) is the same problem as the classification of smooth (or real analytic) manifolds. +Counterexamples abound if the Hausdorff assumption is removed, but it is not clear whether the +paracompact assumption is necessary. https://en.wikipedia.org/wiki/Long_line_(topology)#Properties +claims that every smooth structure on the long line extends to infinitely many real analytic +structures, but this appears to be an overclaim, see https://mathoverflow.net/questions/404692. + ## References * Koji Shiga. Some aspects of real-analytic manifolds and differentiable manifolds. @@ -23,8 +28,6 @@ the classification of smooth (or real analytic) manifolds. * https://en.wikipedia.org/wiki/Differential_structure#Existence_and_uniqueness_theorems -/ -namespace LeanEval.Analysis.C1ToAnalytic - variable (k n : WithTop ℕ∞) variable (M N V W : Type*) [TopologicalSpace M] [TopologicalSpace N] variable [NormedAddCommGroup V] [NormedSpace ℝ V] @@ -34,7 +37,7 @@ open scoped Manifold /-- A Cᵏ-structure on a manifold can be upgraded to a compatible Cⁿ-structure if `1 ≤ k ≤ n` (if `n ≤ k` this is trivial). We use two isomorphic model vector spaces V and W in the statement -to avoid introducing two `ChartedSpace V M` instances. The `k ≥ n` case is trivial. -/ +to avoid introducing two `ChartedSpace V M` instances. -/ @[eval_problem] theorem exists_isManifold_of_le (hk : 1 ≤ k) [FiniteDimensional ℝ V] (e : V ≃ₗ[ℝ] W) [ChartedSpace V M] [IsManifold 𝓘(ℝ,V) k M] [T2Space M] [ParacompactSpace M] : @@ -53,5 +56,3 @@ theorem exists_homotopy_of_diffeomorph (hk : 1 ≤ k) (hkn : k ≤ n) [FiniteDim ∃ H : ℝ × M → N, ContMDiff (𝓘(ℝ,ℝ).prod 𝓘(ℝ,V)) 𝓘(ℝ,W) k H ∧ (H ⟨0, ·⟩) = f ∧ ∃ g : M ≃ₘ^n⟮𝓘(ℝ,V), 𝓘(ℝ,W)⟯ N, (H ⟨1, ·⟩) = g := by sorry - -end LeanEval.Analysis.C1ToAnalytic