Cleanup

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

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) <aristotle-harmonic@harmonic.fun>
+
+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