From 85a699710d89bee7f0609d26ea4c0e0d4ab2b0eb Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Sat, 14 Feb 2026 18:42:04 +0100 Subject: [PATCH 1/5] analytic part --- .../NumberTheory/Transcendental/AnalyticPart | 85 +++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 Mathlib/NumberTheory/Transcendental/AnalyticPart diff --git a/Mathlib/NumberTheory/Transcendental/AnalyticPart b/Mathlib/NumberTheory/Transcendental/AnalyticPart new file mode 100644 index 00000000000000..a181ca0722054c --- /dev/null +++ b/Mathlib/NumberTheory/Transcendental/AnalyticPart @@ -0,0 +1,85 @@ +/- +Copyright (c) 2025 Michail Karatarakis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michail Karatarakis +-/ +module + +public import Mathlib.Analysis.Complex.CauchyIntegral +public import Mathlib.Analysis.Normed.Module.Connected + +/-! +Auxiliary lemmata covering the analytic part of the proof of the Gelfond–Schneider theorem. +Move to appropriate files in Analysis/Complex or Analysis/Analytic and change docstring accordingly. +-/ + +@[expose] public section + +open AnalyticOnNhd AnalyticAt Set + +lemma analyticOrderAt_deriv_eq_top_iff_of_eq_zero (z₀ : ℂ) (f : ℂ → ℂ) (hf : AnalyticAt ℂ f z₀) + (hzero : f z₀ = 0) : analyticOrderAt (deriv f) z₀ = ⊤ ↔ analyticOrderAt f z₀ = ⊤ := by + repeat rw [analyticOrderAt_eq_top, Metric.eventually_nhds_iff_ball] + have ⟨r₁, hr₁, hB⟩ := exists_ball_analyticOnNhd hf + refine ⟨fun ⟨r₂, hr₂, hball⟩ ↦ ?_, fun ⟨r₂, hr₂, hball⟩ ↦ ?_⟩ + · refine ⟨_, lt_min hr₁ hr₂, Metric.isOpen_ball.eqOn_of_deriv_eq ?_ ?_ ?_ ?_ ?_ hzero⟩ + · exact (Metric.isConnected_ball <| by grind).isPreconnected + · intro x hx + exact (hB x <| Metric.ball_subset_ball (min_le_left ..) hx).differentiableWithinAt + · exact differentiableOn_const 0 + · intro x hx + simpa using hball x <| Metric.ball_subset_ball (min_le_right r₁ r₂) hx + · simpa using lt_min hr₁ hr₂ + · refine ⟨_, lt_min hr₁ hr₂, fun x hx ↦ ?_⟩ + rw [← derivWithin_of_mem_nhds <| Metric.isOpen_ball.mem_nhds hx] + trans derivWithin 0 (Metric.ball z₀ (min r₁ r₂)) x + · refine Filter.EventuallyEq.derivWithin_eq_of_nhds <| Filter.eventually_iff_exists_mem.mpr ?_ + refine ⟨_, Metric.isOpen_ball.mem_nhds hx, fun z hz ↦ hball z ?_⟩ + exact Metric.ball_subset_ball (min_le_right r₁ r₂) hz + simp + +lemma analyticOrderAt_eq_succ_iff_deriv_order_eq_pred {z₀ : ℂ} {f : ℂ → ℂ} (hf : AnalyticAt ℂ f z₀) + {n : ℕ} (hzero : f z₀ = 0) (horder : analyticOrderAt (deriv f) z₀ = n) : + analyticOrderAt f z₀ = n + 1 := by + cases Hn' : analyticOrderAt f z₀ with + | top => grind [ENat.coe_ne_top, analyticOrderAt_deriv_eq_top_iff_of_eq_zero] + | coe n' => + cases n' with + | zero => exact hf.analyticOrderAt_eq_zero.mp Hn' hzero |>.elim + | succ n'' => + have := horder ▸ Complex.analyticOrderAt_deriv_of_pos hf Hn' + norm_cast at this ⊢ + have hchar : ringChar ℂ = 0 := by aesop + aesop + +lemma analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero {z₀ : ℂ} (n : ℕ) : + ∀ (f : ℂ → ℂ) (_ : AnalyticAt ℂ f z₀), + ((∀ k < n, deriv^[k] f z₀ = 0) ∧ deriv^[n] f z₀ ≠ 0) ↔ analyticOrderAt f z₀ = n := by + induction n with + | zero => + simp only [ne_eq, not_lt_zero', IsEmpty.forall_iff, implies_true, true_and, CharP.cast_eq_zero] + exact fun f hf ↦ (AnalyticAt.analyticOrderAt_eq_zero hf).symm + | succ n IH => + refine fun f hf ↦ ⟨fun ⟨hz, hnz⟩ ↦ ?_, ?_⟩ + · have IH' := IH (deriv f) (AnalyticAt.deriv hf) + · exact analyticOrderAt_eq_succ_iff_deriv_order_eq_pred hf (hz 0 (by grind)) + (by simpa using ((IH').1 ⟨fun k hk => hz (k + 1) (Nat.succ_lt_succ hk), hnz⟩)) + · refine fun ho ↦ ⟨fun k hk ↦ (analyticOrderAt_ne_zero.mp ?_).2, ?_⟩ + · grind only [(Complex.analyticOrderAt_iterated_deriv (f:=f) hf k (n := (n + 1)) + ho.symm (by grind) hk.le), Nat.cast_ne_zero] + · have := Complex.analyticOrderAt_iterated_deriv (f := f) hf (n + 1) (n := n + 1) + ho.symm (by grind) (by grind) + grind only [AnalyticAt.analyticOrderAt_eq_zero (hf := iterated_deriv hf (n + 1))] + +lemma analyticOrderAt_eq_nat_imp_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) + (n : ℕ) : analyticOrderAt f z₀ = n → (∀ k < n, deriv^[k] f z₀ = 0) ∧ (deriv^[n] f z₀ ≠ 0) := + fun h ↦ (analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero n (f := f) hf).mpr h + +lemma le_analyticOrderAt_iff_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} + (hf : AnalyticAt ℂ f z₀) (n : ℕ) (ho : analyticOrderAt f z₀ ≠ ⊤) : + (∀ k < n, (deriv^[k] f) z₀ = 0) → n ≤ analyticOrderAt f z₀ := by + intro hkn + obtain ⟨m, Hm⟩ := ENat.ne_top_iff_exists (n := analyticOrderAt f z₀).mp ho + rw [← Hm, ENat.coe_le_coe] + by_contra! h + exact ((analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero (n := m) f hf).mpr (Hm.symm)).2 (hkn m h) From 478d987b0c2990b96d1cb877f692b58766cf6e86 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Sat, 14 Feb 2026 22:17:10 +0100 Subject: [PATCH 2/5] lean extension + docstring --- .../Transcendental/{AnalyticPart => AnalyticPart.lean} | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) rename Mathlib/NumberTheory/Transcendental/{AnalyticPart => AnalyticPart.lean} (97%) diff --git a/Mathlib/NumberTheory/Transcendental/AnalyticPart b/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean similarity index 97% rename from Mathlib/NumberTheory/Transcendental/AnalyticPart rename to Mathlib/NumberTheory/Transcendental/AnalyticPart.lean index a181ca0722054c..7212f09eb03c6d 100644 --- a/Mathlib/NumberTheory/Transcendental/AnalyticPart +++ b/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean @@ -1,10 +1,11 @@ /- -Copyright (c) 2025 Michail Karatarakis. All rights reserved. +Copyright (c) 2026 Michail Karatarakis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Michail Karatarakis -/ module +public import Mathlib.Analysis.Analytic.Order public import Mathlib.Analysis.Complex.CauchyIntegral public import Mathlib.Analysis.Normed.Module.Connected From ba7ef9afcff8e5540e75e24cf72480c37f3e32dc Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Thu, 26 Mar 2026 19:03:34 +0100 Subject: [PATCH 3/5] fix errors --- Mathlib/NumberTheory/Transcendental/AnalyticPart.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean b/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean index 7212f09eb03c6d..f6df6e568fea7e 100644 --- a/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean +++ b/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean @@ -48,7 +48,7 @@ lemma analyticOrderAt_eq_succ_iff_deriv_order_eq_pred {z₀ : ℂ} {f : ℂ → cases n' with | zero => exact hf.analyticOrderAt_eq_zero.mp Hn' hzero |>.elim | succ n'' => - have := horder ▸ Complex.analyticOrderAt_deriv_of_pos hf Hn' + have := horder ▸ analyticOrderAt_deriv_of_pos hf Hn' norm_cast at this ⊢ have hchar : ringChar ℂ = 0 := by aesop aesop @@ -66,10 +66,10 @@ lemma analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero {z₀ : ℂ} (n : ℕ) : · exact analyticOrderAt_eq_succ_iff_deriv_order_eq_pred hf (hz 0 (by grind)) (by simpa using ((IH').1 ⟨fun k hk => hz (k + 1) (Nat.succ_lt_succ hk), hnz⟩)) · refine fun ho ↦ ⟨fun k hk ↦ (analyticOrderAt_ne_zero.mp ?_).2, ?_⟩ - · grind only [(Complex.analyticOrderAt_iterated_deriv (f:=f) hf k (n := (n + 1)) + · grind only [(analyticOrderAt_iterated_deriv (f:=f) hf (n := (n + 1)) ho.symm (by grind) hk.le), Nat.cast_ne_zero] - · have := Complex.analyticOrderAt_iterated_deriv (f := f) hf (n + 1) (n := n + 1) - ho.symm (by grind) (by grind) + · have := analyticOrderAt_iterated_deriv (f := f) hf (k := n + 1) (n := n + 1) + ho.symm (by grind) (by omega) grind only [AnalyticAt.analyticOrderAt_eq_zero (hf := iterated_deriv hf (n + 1))] lemma analyticOrderAt_eq_nat_imp_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) From e8a9205318ef890bc88dd495546eb447899ceeb7 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Thu, 26 Mar 2026 19:14:59 +0100 Subject: [PATCH 4/5] mk all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index afbd14b2167acd..77e0d3342fe42e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5662,6 +5662,7 @@ public import Mathlib.NumberTheory.SmoothNumbers public import Mathlib.NumberTheory.SumFourSquares public import Mathlib.NumberTheory.SumPrimeReciprocals public import Mathlib.NumberTheory.SumTwoSquares +public import Mathlib.NumberTheory.Transcendental.AnalyticPart public import Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart public import Mathlib.NumberTheory.Transcendental.Liouville.Basic public import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber From 4c96ca4bce747452e4a40727387bc4a9dffe794e Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 31 Mar 2026 09:54:54 +0200 Subject: [PATCH 5/5] reviews --- .../Transcendental/AnalyticPart.lean | 54 +++++++++---------- 1 file changed, 26 insertions(+), 28 deletions(-) diff --git a/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean b/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean index f6df6e568fea7e..0a6d7b5b6ff25c 100644 --- a/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean +++ b/Mathlib/NumberTheory/Transcendental/AnalyticPart.lean @@ -39,42 +39,40 @@ lemma analyticOrderAt_deriv_eq_top_iff_of_eq_zero (z₀ : ℂ) (f : ℂ → ℂ) exact Metric.ball_subset_ball (min_le_right r₁ r₂) hz simp -lemma analyticOrderAt_eq_succ_iff_deriv_order_eq_pred {z₀ : ℂ} {f : ℂ → ℂ} (hf : AnalyticAt ℂ f z₀) - {n : ℕ} (hzero : f z₀ = 0) (horder : analyticOrderAt (deriv f) z₀ = n) : +lemma analyticOrderAt_deriv_order_eq_succ {z₀ : ℂ} {f : ℂ → ℂ} (hf : AnalyticAt ℂ f z₀) {n : ℕ} + (hzero : f z₀ = 0) (horder : analyticOrderAt (deriv f) z₀ = n) : analyticOrderAt f z₀ = n + 1 := by - cases Hn' : analyticOrderAt f z₀ with - | top => grind [ENat.coe_ne_top, analyticOrderAt_deriv_eq_top_iff_of_eq_zero] - | coe n' => - cases n' with - | zero => exact hf.analyticOrderAt_eq_zero.mp Hn' hzero |>.elim - | succ n'' => - have := horder ▸ analyticOrderAt_deriv_of_pos hf Hn' - norm_cast at this ⊢ - have hchar : ringChar ℂ = 0 := by aesop - aesop + match Hn' : analyticOrderAt f z₀ with + | none => + have Hn_top : analyticOrderAt f z₀ = ⊤ := Hn' + have h_deriv_top := (analyticOrderAt_deriv_eq_top_iff_of_eq_zero z₀ f hf hzero).mpr Hn_top + grind [ENat.coe_ne_top] + | some 0 => + have Hn_zero : analyticOrderAt f z₀ = 0 := Hn' + exact hf.analyticOrderAt_eq_zero.mp Hn_zero hzero |>.elim + | some (n'' + 1) => + have Hn_coe : analyticOrderAt f z₀ = ↑(n'' + 1) := Hn' + have := horder ▸ analyticOrderAt_deriv_of_pos hf Hn_coe + norm_cast at this ⊢ + have hchar : ringChar ℂ = 0 := by aesop + aesop -lemma analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero {z₀ : ℂ} (n : ℕ) : - ∀ (f : ℂ → ℂ) (_ : AnalyticAt ℂ f z₀), - ((∀ k < n, deriv^[k] f z₀ = 0) ∧ deriv^[n] f z₀ ≠ 0) ↔ analyticOrderAt f z₀ = n := by - induction n with - | zero => - simp only [ne_eq, not_lt_zero', IsEmpty.forall_iff, implies_true, true_and, CharP.cast_eq_zero] - exact fun f hf ↦ (AnalyticAt.analyticOrderAt_eq_zero hf).symm +lemma analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} {n : ℕ} + (hf : AnalyticAt ℂ f z₀) : + analyticOrderAt f z₀ = n ↔ (∀ k < n, deriv^[k] f z₀ = 0) ∧ deriv^[n] f z₀ ≠ 0 := by + induction n generalizing f with + | zero => simpa using (AnalyticAt.analyticOrderAt_eq_zero hf) | succ n IH => - refine fun f hf ↦ ⟨fun ⟨hz, hnz⟩ ↦ ?_, ?_⟩ - · have IH' := IH (deriv f) (AnalyticAt.deriv hf) - · exact analyticOrderAt_eq_succ_iff_deriv_order_eq_pred hf (hz 0 (by grind)) - (by simpa using ((IH').1 ⟨fun k hk => hz (k + 1) (Nat.succ_lt_succ hk), hnz⟩)) + refine ⟨?_, fun ⟨hz, hnz⟩ ↦ ?_⟩ · refine fun ho ↦ ⟨fun k hk ↦ (analyticOrderAt_ne_zero.mp ?_).2, ?_⟩ · grind only [(analyticOrderAt_iterated_deriv (f:=f) hf (n := (n + 1)) ho.symm (by grind) hk.le), Nat.cast_ne_zero] · have := analyticOrderAt_iterated_deriv (f := f) hf (k := n + 1) (n := n + 1) ho.symm (by grind) (by omega) grind only [AnalyticAt.analyticOrderAt_eq_zero (hf := iterated_deriv hf (n + 1))] - -lemma analyticOrderAt_eq_nat_imp_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) - (n : ℕ) : analyticOrderAt f z₀ = n → (∀ k < n, deriv^[k] f z₀ = 0) ∧ (deriv^[n] f z₀ ≠ 0) := - fun h ↦ (analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero n (f := f) hf).mpr h + · have IH' := IH (AnalyticAt.deriv hf) + exact analyticOrderAt_deriv_order_eq_succ hf (hz 0 (by grind)) + (by simpa using (IH'.2 ⟨fun k hk => hz (k + 1) (Nat.succ_lt_succ hk), hnz⟩)) lemma le_analyticOrderAt_iff_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (n : ℕ) (ho : analyticOrderAt f z₀ ≠ ⊤) : @@ -83,4 +81,4 @@ lemma le_analyticOrderAt_iff_iteratedDeriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ obtain ⟨m, Hm⟩ := ENat.ne_top_iff_exists (n := analyticOrderAt f z₀).mp ho rw [← Hm, ENat.coe_le_coe] by_contra! h - exact ((analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero (n := m) f hf).mpr (Hm.symm)).2 (hkn m h) + exact ((analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero hf).mp (Hm.symm)).2 (hkn m h)