[{"type":"thinking","thinking":"No `convex_halfspace_re_gt` in this Mathlib. The half-plane convexity: {z : ℂ | c < z.re} = (Complex.re)⁻¹' (Ioi c) — convex as the preimage of a convex set under a LINEAR map: `Convex.preimage` with Complex.reCLM? There's `Complex.reCLM : ℂ →L[ℝ] ℝ`? or `Complex.reLinearMap`? The preimage of convex under a linear map: `Convex.preimage (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F)?? : Convex 𝕜 (f ⁻¹' s)`? There's `Convex.linear_preimage`? or `LinearMap.convex_preimage`? Let me think — simplest: prove convexity of {c < re z} directly: x, y in set, a,b ≥ 0, a+b=1: re(a•x + b•y) = a·re x + b·re y > a·c + b·c = c ✓ — short:\n```lean\nhave hconvex_re : Convex ℝ {z : ℂ | -1 < z.re} := by\n  apply convex_iff_forall_pos.mpr?  -- or direct:\n  intro x hx y hy a b ha hb hab\n  -- re(a•x + b•y) = a re x + b re y > c\n  simp only [Set.mem_setOf_eq] at hx hy ⊢\n  rw [add_re, smul_re, smul_re]  -- re(a • x) = a * re x\n  nlinarith [hx, hy, ha, hb, hab]\n```\nHmm — smul_re: Complex.smul_re : (c • z).re = c * z.re ✓ (real smul). a • x with a : ℝ: in ℂ: (a:ℂ)·x: re = a·re x ✓. The convex definition: `Convex 𝕜 s` unfolds to ∀ x ∈ s, y ∈ s, a b ≥ 0, a + b = 1 → a • x + b • y ∈ s. nlinarith: a·re x + b·re y > ... need > −1: a·re x > a·(−1), b·re y > b·(−1) with a,b ≥ 0, a+b = 1 (not both zero): a·re x + b·re y > −(a+b)·1 = −1 — needs strictness: if a > 0: a·re x > −a; b·re y ≥ −b: sum > −1 ✓; nlinarith with case analysis — nlinarith can handle: from hab : a + b = 1, ha : 0 ≤ a, hb : 0 ≤ b: not both zero; a·re x ≥ −a (if a = 0 equality, else strict); nlinarith can multiply (re x + 1 > 0)·(a ≥ 0) etc. — should manage with hints: nlinarith [mul_nonneg ha (by linarith : (0:ℝ) ≤ re x + 1), mul_nonneg hb (by linarith : (0:ℝ) ≤ re y + 1), ...]. The strictness: need SOME positive coefficient: from ha hb hab: a > 0 ∨ b > 0 — nlinarith might struggle with the disjunction... do by_cases: if a = 0 then b = 1 simp; else a > 0: then strict from a·re x > −a and b·re y ≥ −b:\n```lean\n  nlinarith [mul_pos_of_pos_of_nonneg (show 0 < a by ...) (show 0 < re x + 1 by linarith), mul_nonneg hb (show 0 ≤ re y + 1 by linarith)]\n```\nGetting fiddly; alternative: use the linear-map preimage: `Complex.reCLM`? grep for it: there's `Complex.reCLM : ℂ →L[ℝ] ℝ` ✓ I believe. Then {c < re} = reCLM ⁻¹' (Ioi c): Convex.preimage: `Convex.preimage (hs : Convex 𝕜 s) (hf : IsLinearMap...)`? The standard: `Convex.linear_preimage (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f ⁻¹' s)`? name: `Convex.linear_preimage`? or `LinearMap.convex_preimage`? — there's definitely something. And isOpen: preimage of open under continuous ✓ (I already used isOpen_lt continuous_const Complex.continuous_re ✓ that worked).\n\nHonestly — the direct proof is short enough. Let me write it with the case split. Actually even simpler: `Convex.preimage` — let me check quickly what's available... you know what, let me just write the direct proof with a clean case split:\n\n```lean\ntheorem convex_halfplane_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re} := by\n  intro x hx y hy a b ha hb hab\n  simp only [Set.mem_setOf_eq] at hx hy ⊢\n  have hre : (a • x + b • y).re = a * x.re + b * y.re := by\n    simp [add_re, smul_re]\n  rw [hre]\n  have h1 : a * x.re ≥ a * c := mul_le_mul_of_nonneg_left hx.le ha\n  have h2 : b * y.re ≥ b * c := mul_le_mul_of_nonneg_left hy.le hb\n  -- strict from a+b = 1, both nonneg, strict somewhere\n  rcases eq_or_ne a 0 with ha0 | ha0\n  · subst ha0\n    simp at hab\n    subst hab\n    simp at h1 h2 ⊢\n    linarith [hy]\n  · have ha' : 0 < a := lt_of_le_of_ne ha (Ne.symm ha0)\n    have hb' : 0 ≤ b := hb\n    have : b * y.re ≥ b * c := h2\n    have h3 : a * x.re > a * c := mul_lt_mul_of_pos_left hx ha'\n    nlinarith [h3, h2, hab]\n```\nHmm the first branch: a = 0 ⟹ b = 1: goal 0·x.re + 1·y.re > c ⟹ y.re > c ✓ hy. OK workable. Let me simplify with a slicker one-liner attempt: `nlinarith [mul_lt_mul_of_pos_left ...]`... fine.\n\nHmm — actually wait, there IS a simpler standard trick: `Convex.inter` of... no. Or use `convex_Ioi` + preimage under linear map: \n```lean\ntheorem convex_halfplane_re_gt (c : ℝ) : Convex ℝ {z : ℂ | c < z.re} :=\n  convex_Ioi c |>.linear_preimage Complex.reLM?...\n```\nLet me check `Complex.reCLM`/`Complex.reLinearMap` existence... `Complex.reCLM : ℂ →L[ℝ] ℝ` exists I'm fairly sure (in Complex/Basic or Analysis/Complex/Basic: `Complex.reCLM`). And `Convex.linear_preimage (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f ⁻¹' s)`? — hmm the name: `Convex.linear_preimage (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F)`? There's `Convex.is_linear_image`/`Convex.linear_image`? and preimage: `Convex.linear_preimage`? Let me just grep once.","signature":""},{"type":"text","text":"Checking the linear-map preimage route for half-plane convexity."},{"type":"tool_use","id":"Bash_280","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem Convex.linear_preimage\\|lemma Convex.linear_preimage\\|def reCLM\\|reCLM :\" Mathlib/Analysis/ -r --include=*.lean | head -5; grep -rn \"theorem convex_Ioi\\b\" Mathlib/Order/ -r --include=*.lean | head -2","description":"Check linear preimage and reCLM"},"extra_content":null}]