From ba0469d4abe4245dcf55601061ea934ef9ad3565 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Sun, 25 Jan 2026 17:22:49 +0100 Subject: [PATCH] Cleanup --- Aristotle/Basic.lean | 17 ++++----- Aristotle/Basic_aristotle.lean | 69 ++++++++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+), 10 deletions(-) create mode 100644 Aristotle/Basic_aristotle.lean diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean index 331fcc7..43b97e2 100644 --- a/Aristotle/Basic.lean +++ b/Aristotle/Basic.lean @@ -1,15 +1,12 @@ import Mathlib +open Complex -theorem intervalIntegrable_iff_intervalIntegrable_smul - {E : Type*} [NormedAddCommGroup E] - {a b : ℝ} {μ : MeasureTheory.Measure ℝ} - {R : Type*} [NormedAddCommGroup R] [SMulZeroClass R E] [IsBoundedSMul R E] - {f : ℝ → E} {r : R} (hr : r ≠ 0) : - IntervalIntegrable f μ a b ↔ IntervalIntegrable (r • f) μ a b := by - sorry +/-- +Show that a function whose real part vanishes is constant. +-/ -theorem IntervalIntegrable.abs' - {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} (hf : Measurable f) : - IntervalIntegrable f μ a b ↔ IntervalIntegrable (fun x => |f x|) μ a b := by +theorem testCase {f : ℂ → ℂ} {U : Set ℂ} (h₁ : IsOpen U) (h₂ : IsConnected U) + (h₃ : AnalyticOnNhd ℂ f U) (h₄ : ∀ x ∈ U, (f x).re = 0) : + ∃ c : ℝ, ∀ x ∈ U, f x = c*I := by sorry diff --git a/Aristotle/Basic_aristotle.lean b/Aristotle/Basic_aristotle.lean new file mode 100644 index 0000000..f3e4b0d --- /dev/null +++ b/Aristotle/Basic_aristotle.lean @@ -0,0 +1,69 @@ +/- +This file was edited by Aristotle. + +Lean version: leanprover/lean4:v4.24.0 +Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 +This project request had uuid: 825f216f-5d20-41eb-9e65-b4815074842a + +To cite Aristotle, tag @Aristotle-Harmonic on GitHub PRs/issues, and add as co-author to commits: +Co-authored-by: Aristotle (Harmonic) + +The following was proved by Aristotle: + +- theorem testCase {f : ℂ → ℂ} {U : Set ℂ} (h₁ : IsOpen U) (h₂ : IsConnected U) + (h₃ : AnalyticOnNhd ℂ f U) (h₄ : ∀ x ∈ U, (f x).re = 0) : + ∃ c : ℝ, ∀ x ∈ U, f x = c*I +-/ + +import Mathlib + + +open Complex + +/-- +Show that a function whose real part vanishes is constant. +-/ + +theorem testCase {f : ℂ → ℂ} {U : Set ℂ} (h₁ : IsOpen U) (h₂ : IsConnected U) + (h₃ : AnalyticOnNhd ℂ f U) (h₄ : ∀ x ∈ U, (f x).re = 0) : + ∃ c : ℝ, ∀ x ∈ U, f x = c*I := by + -- By the maximum principle, since $|e^{f(x)}| = 1$ for all $x \in U$, $e^{f(x)}$ must be constant on $U$. + have h_exp_const : ∃ c : ℂ, ∀ x ∈ U, Complex.exp (f x) = c := by + -- Fix an arbitrary $z_0 \in U$. + obtain ⟨z₀, hz₀⟩ : ∃ z₀ ∈ U, True := by + exact Exists.elim ( h₂.nonempty ) fun x hx => ⟨ x, hx, trivial ⟩; + -- By the maximum principle, since $|e^{f(x)}| = 1$ for all $x \in U$, $e^{f(x)}$ must be constant on $U$. Hence, there exists $c \in \mathbb{C}$ such that $e^{f(x)} = c$ for all $x \in U$. + have h_exp_const : ∀ x ∈ U, Complex.exp (f x) = Complex.exp (f z₀) := by + apply_rules [ @Complex.eqOn_of_isPreconnected_of_isMaxOn_norm ]; + · exact h₂.isPreconnected; + · exact Complex.differentiable_exp.comp_differentiableOn h₃.differentiableOn; + · tauto; + · intro x hx; simp +decide [ Complex.norm_exp, h₄ x hx, h₄ z₀ hz₀.1 ] ; + use Complex.exp (f z₀); + cases' h_exp_const with c hc; + -- Since $e^{f(x)} = c$ for all $x \in U$, we have $f(x) = \log(c)$ for all $x \in U$. + have h_log : ∀ x ∈ U, f x ∈ {z : ℂ | Complex.exp z = c} := by + aesop; + -- Since $e^{f(x)} = c$ for all $x \in U$, we have $f(x) = \log(c) + 2k\pi i$ for some integer $k$. + have h_log_form : ∀ x ∈ U, ∃ k : ℤ, f x = Complex.log c + 2 * k * Real.pi * Complex.I := by + intro x hx; specialize h_log x hx; rw [ Set.mem_setOf_eq ] at h_log; rw [ ← Complex.exp_log ( show c ≠ 0 from fun h => by simpa [ h ] using hc x hx ) ] at h_log; rw [ Complex.exp_eq_exp_iff_exists_int ] at h_log; obtain ⟨ k, hk ⟩ := h_log; exact ⟨ k, by linear_combination hk ⟩ ; + choose! k hk using h_log_form; + -- Since $k$ is a function from $U$ to $\mathbb{Z}$, and $U$ is connected, $k$ must be constant. + have h_k_const : ∃ k₀ : ℤ, ∀ x ∈ U, k x = k₀ := by + have h_k_const : ContinuousOn k U := by + have h_k_const : ContinuousOn (fun x => (k x : ℂ)) U := by + have h_k_const : ContinuousOn (fun x => (f x - Complex.log c) / (2 * Real.pi * Complex.I)) U := by + exact ContinuousOn.div_const ( h₃.continuousOn.sub continuousOn_const ) _; + refine' h_k_const.congr fun x hx => _; + field_simp; + linear_combination -hk x hx; + rw [ Metric.continuousOn_iff ] at *; + intro b hb ε hε; specialize h_k_const b hb ε hε; rcases h_k_const with ⟨ δ, hδ, H ⟩ ; use δ, hδ; intro a ha hab; specialize H a ha hab; simp_all +decide [ Complex.dist_eq, Complex.normSq ] ; + erw [ Real.dist_eq ] ; norm_cast at *; + have h_k_const : IsPreconnected (k '' U) := by + exact h₂.isPreconnected.image _ h_k_const; + have := h_k_const.subsingleton; + exact ⟨ k ( Classical.choose h₂.nonempty ), fun x hx => this ( Set.mem_image_of_mem k hx ) ( Set.mem_image_of_mem k ( Classical.choose_spec h₂.nonempty ) ) ⟩; + cases' h_k_const with k₀ hk₀; use ( Complex.im ( Complex.log c ) + 2 * k₀ * Real.pi ) ; intro x hx; rw [ hk x hx, hk₀ x hx ] ; simp +decide [ Complex.ext_iff ] ; ring; + simp_all +decide [ Complex.log_re ]; + exact h₄ x hx \ No newline at end of file