[{"type":"thinking","thinking":"All confirmed:\n- `Complex.div_re (z w : ℂ) : (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w` (Data/Complex/Basic.lean:705, in Complex namespace — opened)\n- `Complex.div_im` :708\n- `Complex.normSq_eq_norm_sq` (Analysis/Complex/Norm.lean:147)\n- `Complex.abs_re_le_norm` :38\n- `Complex.norm_ofReal`? The grep found `theorem norm_ofReal (r : ℝ) : ‖(r : K)‖ = |r|` in RCLike/Basic.lean:246 — that's `Complex.norm_ofReal` with K := ℂ? It's likely `Complex.norm_ofReal`... the RCLike one is generic `@norm_ofReal K _ r`? Hmm — line says `theorem norm_ofReal (r : ℝ) : ‖(r : K)‖ = |r|` inside some namespace (probably `RCLike` or `Complex`?). There's also the well-known `Complex.norm_ofReal : ‖(x : ℂ)‖ = |x|`. I'll try `Complex.norm_ofReal` and fall back to simp [Complex.norm_ofReal]/norm_ofReal if needed.\n- `Real.exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (n * x) = Real.exp x ^ n` ✓\n- `Real.add_one_le_exp (x : ℝ) : x + 1 ≤ Real.exp x` ✓\n- `sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a^2 ≤ b^2 ↔ a ≤ b` ✓\n- `pow_le_one₀ (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : a^n ≤ 1` ✓\n- `Real.mul_self_sqrt (h : 0 ≤ x) : √x * √x = x` ✓\n- `Complex.normSq_pos : 0 < normSq z ↔ z ≠ 0` ✓\n\nNow write §4. Draft:\n\n```lean\n/-! ## 4. L1: kernel norm bounds (D-036 §3) -/\n\n/-- On re s ≤ 1/2 the ratio satisfies ‖s/(s−1)‖ ≤ 1 (i.e. ‖s‖ ≤ ‖s−1‖). -/\ntheorem norm_div_sub_one_le_one {s : ℂ} (hs : s.re ≤ 1 / 2) : ‖s / (s - 1)‖ ≤ 1 := by\n  have hs1 : s ≠ 1 := by\n    intro h\n    rw [h] at hs\n    simp at hs  -- (1:ℂ).re = 1 ≤ 1/2 false\n  have hnorm : ‖s‖ ≤ ‖s - 1‖ := by\n    have h : Complex.normSq s ≤ Complex.normSq (s - 1) := by\n      rw [Complex.normSq_apply, Complex.normSq_apply]\n      simp only [sub_re, one_re, sub_im, one_im, sub_zero]\n      nlinarith [hs]\n    rw [Complex.normSq_eq_norm_sq, Complex.normSq_eq_norm_sq] at h\n    nlinarith [norm_nonneg s, norm_nonneg (s - 1), h]\n  have hpos : (0:ℝ) < ‖s - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)\n  rw [norm_div]\n  exact div_le_one hpos |>.mpr ... -- ‖s‖/‖s−1‖ ≤ 1 ⟺ ‖s‖ ≤ ‖s−1‖\n```\n\n`div_le_one (hb : 0 < b) : a / b ≤ b ↔ a ≤ b`?? No: `div_le_one (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b` ✓ (div_le_one). So `(div_le_one hpos).mpr hnorm`.\n\n`norm_pos_iff : 0 < ‖a‖ ↔ a ≠ 0` ✓.\n`simp at hs` after rw [h]: hs : (1:ℂ).re ≤ 1/2 — `Complex.one_re : (1:ℂ).re = 1` simp ⟹ 1 ≤ 1/2 — simp closes via norm_num? `simp at hs` might reduce to False and close the goal... hs : (1:ℝ) ≤ 1/2 after simp [Complex.one_re]... then `norm_num at hs`. Write:\n```lean\n  have hs1 : s ≠ 1 := by\n    intro h\n    rw [h, Complex.one_re] at hs  -- hmm hs : s.re ≤ 1/2; h : s = 1; rw [h] at hs : (1:ℂ).re ≤ 1/2\n    norm_num at hs\n```\n`Complex.one_re` — is it simp lemma? `Complex.one_re : (1 : ℂ).re = 1` ✓ exists (simp). So `rw [h] at hs; norm_num at hs` — norm_num should evaluate (1:ℂ).re... safer: `simp only [Complex.one_re] at hs; norm_num at hs`? or just:\n```lean\n  have hs1 : s ≠ 1 := by\n    rintro h\n    have : (1 : ℝ) ≤ 1 / 2 := h ▸ hs  -- hmm ▸ direction\n```\nh : s = 1; hs : s.re ≤ 1/2; h ▸ hs rewrites s to 1 in hs : (1:ℂ).re ≤ 1/2 — then need ((1:ℂ).re = 1): `Complex.one_re`. \n```lean\n    rw [h] at hs\n    simp only [Complex.one_re] at hs\n    norm_num at hs\n```\nOK.\n\nMain bound 1:\n```lean\n/-- **L1 (left side)**: ‖kFun n s‖ ≤ 2 for re s ≤ 1/2 (D-036 §3 (III)). -/\ntheorem kFun_norm_le_two {n : ℕ} {s : ℂ} (hs : s.re ≤ 1 / 2) : ‖kFun n s‖ ≤ 2 := by\n  have h1 := norm_div_sub_one_le_one hs\n  have h2 : ‖(s / (s - 1)) ^ n‖ ≤ 1 := by\n    rw [norm_pow]\n    exact pow_le_one₀ (norm_nonneg _) h1\n  calc ‖kFun n s‖ = ‖(s / (s - 1)) ^ n - 1‖ := rfl\n    _ ≤ ‖(s / (s - 1)) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _\n    _ ≤ 1 + 1 := by rw [norm_one]; linarith [h2]  -- hmm norm_one for ℂ: ‖1‖ = 1\n    _ = 2 := by norm_num\n```\nHmm `norm_one : ‖(1:ℂ)‖ = 1` ✓.\n\nThe shift form helper:\n```lean\n/-- kFun at the shifted point: kFun n (s+1) = (1 + 1/s)ⁿ − 1 (s ≠ 0). -/\ntheorem kFun_add_one {n : ℕ} {s : ℂ} (hs : s ≠ 0) :\n    kFun n (s + 1) = (1 + 1 / s) ^ n - 1 := by\n  have h : (s + 1) / (s + 1 - 1) = 1 + 1 / s := by field_simp\n  unfold kFun\n  rw [show s + 1 - 1 = s by ring]  -- (s+1)/(s) \n  field_simp\n```\nCareful: kFun n (s+1) = ((s+1)/(s+1−1))^n − 1; s+1−1 = s (ring, but it's defeq? (s+1)−1 — ring-normal... `show`+ring works but the expression `s + 1 - 1` is not syntactically s. `congr 1`? Let me write:\n```lean\ntheorem kFun_add_one {n : ℕ} {s : ℂ} (hs : s ≠ 0) :\n    kFun n (s + 1) = (1 + 1 / s) ^ n - 1 := by\n  have e : (s + 1) / (s + 1 - 1) = 1 + 1 / s := by\n    rw [show s + 1 - 1 = s by ring]\n    field_simp\n  unfold kFun\n  rw [e]\n```\nfield_simp with hs: (s+1)/s = 1 + 1/s ⟺ s+1 = s·(1+1/s) = s+1 ✓; field_simp [hs] then ring. ✓\n\nCore normSq comparison:\n```lean\n/-- The horizontal core: ‖1 + 1/s‖ ≤ 1 + (re s + 1)/normSq s (s ≠ 0).\nFrom ‖1+1/s‖² = 1 + (2σ+1)/D ≤ (1+(σ+1)/D)² with D = σ²+T². -/\ntheorem norm_one_add_one_div_le {s : ℂ} (hs : s ≠ 0) :\n    ‖1 + 1 / s‖ ≤ 1 + (s.re + 1) / Complex.normSq s := by\n  set D := Complex.normSq s with hD_def\n  have hD : (0:ℝ) < D := Complex.normSq_pos.mpr hs\n  have hre : (1 / s).re = s.re / D := by\n    rw [Complex.div_re]\n    simp [one_re, one_im, hD_def]\n  have him : (1 / s).im = -s.im / D := by\n    rw [Complex.div_im]\n    simp [one_re, one_im, hD_def]\n  have hsq : Complex.normSq (1 + 1 / s) = 1 + (2 * s.re + 1) / D := by\n    rw [Complex.normSq_apply]\n    simp only [add_re, one_re, add_im, one_im, hre, him]  -- hmm (1 + 1/s).re = 1 + (1/s).re = 1 + σ/D; im = 0 + (−T/D)\n    field_simp\n    rw [hD_def, Complex.normSq_apply]  -- D = σ² + T²\n    ring  -- (1+σ/D)² + (T/D)² = 1 + (2σ+1)/D ⟺ D² ... field_simp then ring with D = σ²+T²\n  have hRHS : (0:ℝ) ≤ 1 + (s.re + 1) / D := by\n    have : (0:ℝ) < D + (s.re + 1) := by\n      rw [hD_def, Complex.normSq_apply]\n      nlinarith [sq_nonneg (s.re + 1/2), sq_nonneg s.im]  -- σ²+T²+σ+1 = (σ+1/2)²+T²+3/4\n    have := ... (D + (σ+1))/D > 0\n    rw [add_div'... ] hmm: 1 + (σ+1)/D = (D + σ + 1)/D: (one_add_div?) \n    have e : 1 + (s.re + 1) / D = (D + (s.re + 1)) / D := by field_simp\n    rw [e]\n    positivity? (div_nonneg this.le hD.le) — need D + σ+1 ≥ 0 ✓ and D ≥ 0 ✓: `div_nonneg this.le hD.le`? this : 0 < D + (s.re+1): .le ✓. \n  -- square comparison\n  have hcmp : Complex.normSq (1 + 1 / s) ≤ (1 + (s.re + 1) / D)^2 := by\n    rw [hsq]\n    have e2 : (1 + (s.re + 1) / D)^2 = 1 + (2*s.re + 1)/D + (1/D + ((s.re+1)/D)^2) := by\n      field_simp; ring\n    rw [e2]\n    have : (0:ℝ) ≤ 1 / D + ((s.re + 1) / D)^2 := by positivity\n    linarith\n  -- take roots\n  rw [Complex.normSq_eq_norm_sq] at hcmp  -- hmm normSq (1+1/s) = ‖1+1/s‖²\n  -- hcmp : ‖1+1/s‖^2 ≤ (1 + (σ+1)/D)^2, both sides nonneg\n  exact (sq_le_sq₀ (norm_nonneg _) hRHS).mp hcmp\n```\nWait sq_le_sq₀ : a² ≤ b² ↔ a ≤ b with a, b ≥ 0. hcmp : ‖1+1/s‖^2 ≤ RHS^2 — but I need the form a^2 ≤ b^2: ✓ exactly. (sq_le_sq₀ (norm_nonneg _) hRHS).mp hcmp : ‖1+1/s‖ ≤ 1+(σ+1)/D ✓.\n\nfield_simp in hsq: goal after simp substitutions: (1 + σ/D)^2 + (−T/D)^2 = 1 + (2σ+1)/D. field_simp [hD.ne'] clears denominators: (D+σ)²·D²... messy but ring with D = σ²+T²: need the relation D = σ²+T² as hypothesis for ring: after `rw [hD_def, Complex.normSq_apply]` everywhere... hmm — in hsq the RHS has D (set variable), and σ²+T² appears after expansion... Let me restructure: don't `set D`; work with normSq s directly and use normSq_apply at the end. Or: keep set D, and have hD_eq : D = s.re^2 + s.im^2 := by rw [hD_def, Complex.normSq_apply]. Then in the ring step: field_simp [hD.ne']; then `nlinarith [hD_eq]`? or linear... the identity: (1+σ/D)² + (T/D)² = 1 + (2σ+1)/D ⟺ D(D + 2σ) + ... let me just multiply out: LHS·D² = (D+σ)² + T²·... no: (1+σ/D)² = (D+σ)²/D², (T/D)² = T²/D²: sum = ((D+σ)²+T²)/D². RHS = 1 + (2σ+1)/D = (D + 2σ + 1)/D. ⟺ ((D+σ)²+T²)/D² = (D+2σ+1)/D ⟺ (D+σ)² + T² = (D+2σ+1)·D ⟺ D² + 2σD + σ² + T² = D² + 2σD + D ⟺ σ² + T² = D ✓ (the relation). So after field_simp [hD.ne']: goal becomes something like (D+σ)^2 + T^2 = (D+2σ+1)*D — wait field_simp normalizes both sides: it might produce `(D + σ)^2 + s.im^2 = D + (2σ+1)*D`... then `nlinarith [hD_eq]`? it's linear in D after expansion... ring_nf then linear in atoms: substitute hD_eq: `rw [hD_eq]`? D appears on both sides... Actually simplest: avoid `set D` in hsq and instead:\n\n```lean\n  have hsq : Complex.normSq (1 + 1 / s) = 1 + (2 * s.re + 1) / Complex.normSq s := by\n    rw [Complex.normSq_apply, Complex.div_re, Complex.div_im]\n    simp only [add_re, one_re, add_im, one_im, one_re, one_im]\n    -- (1/s).re = (1*σ + 0*T)/D' = σ/D'; (1/s).im = (0*σ − 1*T)/D' = −T/D'\n    -- goal: (1 + σ/D')² + (0 + (−T/D'))²... = 1 + (2σ+1)/D'  where D' = normSq s\n    rw [Complex.normSq_apply]  -- D' = σ² + T² in the denominators too\n    field_simp\n    ring\n```\nHmm — order matters: the div_re/div_im introduce normSq s in denominators; then rw [Complex.normSq_apply] rewrites ALL normSq s occurrences including the LHS outer one (already rewritten to re²+im² form? I did normSq_apply FIRST on the LHS outer). Careful sequencing. This is the fiddly part — I'll iterate in the compiler. Let me instead structure:\n\n```lean\ntheorem norm_one_add_one_div_le {s : ℂ} (hs : s ≠ 0) :\n    ‖1 + 1 / s‖ ≤ 1 + (s.re + 1) / Complex.normSq s := by\n  have hD : (0:ℝ) < Complex.normSq s := Complex.normSq_pos.mpr hs\n  have hsq : Complex.normSq (1 + 1 / s) = 1 + (2 * s.re + 1) / Complex.normSq s := by\n    have h1 : (1 + 1 / s).re = 1 + s.re / Complex.normSq s := by\n      simp [add_re, one_re, Complex.div_re]\n    have h2 : (1 + 1 / s).im = -s.im / Complex.normSq s := by\n      simp [add_im, one_im, Complex.div_im]\n    rw [Complex.normSq_apply, h1, h2, Complex.normSq_apply]\n    field_simp\n    ring\n  ...\n```\nAfter rw [Complex.normSq_apply, h1, h2, Complex.normSq_apply]: LHS = (1 + σ/D')² + (−T/D')² where D' here — wait, the second Complex.normSq_apply rewrites the normSq s in the denominators to σ²+T² (re²+im² — normSq_apply : normSq z = z.re^2 + z.im^2 ✓ hmm exact form: `Complex.normSq_apply : normSq z = z.re * z.re + z.im * z.im`? It's `normSq z = z.re ^ 2 + z.im ^ 2`? Might be mul form `z.re * z.re`. field_simp + ring handles either as long as consistent.) Then field_simp clears the /D denominators (D ≠ 0 from hD.ne'), ring closes using D = σ²+T² relation which is now syntactic ✓.\n\nsimp [add_re, one_re, Complex.div_re] for h1: (1 + 1/s).re = (1:ℂ).re + (1/s).re = 1 + (1.re·s.re + 1.im·s.im)/normSq s = 1 + (1·σ + 0·T)/D = 1 + σ/D — simp should manage with div_re, one_re, one_im, add_re, add_im... Note: `Complex.div_re : (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w` — for z = 1: = 1*σ/D + 0*T/D = σ/D ✓ simp [Complex.div_re, Complex.one_re, Complex.one_im]. \n\nOK — horizontal lemma:\n\n```lean\n/-- **L1 (horizontals)**: ‖kFun n (s+1)‖ ≤ e⁴ + 1 for re s ≤ 3 and\nn ≤ (im s)² (D-036 §3 (II),(IV)): then |1+1/s| ≤ 1 + 4/n, and\n(1+4/n)ⁿ ≤ e⁴. -/\ntheorem kFun_shift_norm_le_exp_four_add_one {n : ℕ} {s : ℂ}\n    (hσ : s.re ≤ 3) (hT : (n : ℝ) ≤ s.im ^ 2) :\n    ‖kFun n (s + 1)‖ ≤ Real.exp 4 + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  · simp [hn, kFun]  -- kFun 0 = (..)^0 − 1 = 0; ‖0‖ ≤ e⁴+1: positivity\n  · have hTpos : 0 < s.im ^ 2 := lt_of_lt_of_le (by exact_mod_cast hn ... (0 < (n:ℝ))) hT\n    -- (n:ℝ) ≥ 1 > 0 ⟹ s.im² ≥ 1\n    have hs0 : s ≠ 0 := by\n      intro h\n      rw [h] at hT  -- s.im = 0 ⟹ (n:ℝ) ≤ 0 contradiction\n      simp at hT\n      linarith [show (1:ℝ) ≤ n from by exact_mod_cast hn]\n    set D := Complex.normSq s with hD_def\n    have hD : (0:ℝ) < D := Complex.normSq_pos.mpr hs0\n    have hDn : (n:ℝ) ≤ D := by\n      rw [hD_def, Complex.normSq_apply]\n      nlinarith [hT, sq_nonneg s.re]  -- D = σ²+T² ≥ T² ≥ n\n    have hcore := norm_one_add_one_div_le hs0\n    have hle : ‖1 + 1 / s‖ ≤ 1 + 4 / n := by\n      refine hcore.trans ?_\n      have h4 : (s.re + 1) / D ≤ 4 / n := by\n        -- (σ+1)/D ≤ 4/D ≤ 4/n — hmm 4/D ≤ 4/n needs D ≥ n ✓ and D > 0\n        have hσ4 : s.re + 1 ≤ 4 := by linarith\n        by_cases hσp : 0 ≤ s.re + 1\n        · calc (s.re + 1) / D ≤ 4 / D := by\n                exact div_le_div_of_nonneg_right? -- (σ+1)/D ≤ 4/D ⟺ σ+1 ≤ 4, D > 0\n              _ ≤ 4 / n := by ...\n        · -- σ+1 < 0: (σ+1)/D < 0 ≤ 4/n\n          have : (s.re + 1) / D ≤ 0 := div_nonpos_of_nonpos_of_nonneg (by linarith) hD.le\n          linarith [show (0:ℝ) ≤ 4/n by positivity]\n      linarith [h4]\n      ...\n```\n\n`div_le_div_of_nonneg_right`? The right lemma: `div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b` ✓ exists (div_le_div_right). So (σ+1)/D ≤ 4/D via (div_le_div_right hD).mpr hσ4. And 4/D ≤ 4/n via `div_le_div_left (h4 : 0 < 4) (hD : 0 < D) (hn' : 0 < n) ... `: `div_le_div_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b` — so (div_le_div_left four_pos hD hnR).mpr hDn ✓ where hnR : (0:ℝ) < n.\n\nThen:\n```lean\n    have hpow : ‖1 + 1 / s‖ ^ n ≤ Real.exp 4 := by\n      calc ‖1 + 1 / s‖ ^ n ≤ (1 + 4 / n) ^ n := pow_le_pow_left (norm_nonneg _) hle n\n        _ ≤ (Real.exp (4 / n)) ^ n := by\n            apply pow_le_pow_left (by positivity) _ n\n            -- 1 + 4/n ≤ exp(4/n): Real.add_one_le_exp\n            have := Real.add_one_le_exp (4 / (n:ℝ))\n            linarith [this]  -- x + 1 ≤ exp x with x = 4/n: 1 + 4/n = 4/n + 1 ✓ linarith\n        _ = Real.exp 4 := by\n            rw [← Real.exp_nat_mul]\n            congr 1\n            field_simp  -- n * (4/n) = 4, n ≠ 0\n    -- assemble\n    rw [kFun_add_one hs0]\n    calc ‖(1 + 1 / s) ^ n - 1‖ ≤ ‖(1 + 1 / s) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _\n      _ = ‖1 + 1 / s‖ ^ n + 1 := by rw [norm_pow, norm_one]\n      _ ≤ Real.exp 4 + 1 := by linarith [hpow]\n```\n\nWait — pow_le_pow_left signature: `pow_le_pow_left (ha : 0 ≤ a) (hab : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n` ✓.\n\n`Real.exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (n * x) = (Real.exp x) ^ n` ✓. So (exp(4/n))^n = exp (↑n * (4/n)) = exp 4: rw [← Real.exp_nat_mul] turns (exp(4/n))^n into exp(↑n * (4/n)); congr 1: goal ↑n * (4/↑n) = 4: field_simp with n ≠ 0 or `mul_div_cancel₀`: `mul_div_cancel_left₀`? n * (4/n) = 4: field_simp [Nat.cast_ne_zero.mpr hn.ne'] ✓.\n\nRight vertical:\n\n```lean\n/-- **L1 (right vertical)**: ‖kFun n (s+1)‖ ≤ e^{√n/2} + 1 for 0 < n and\n2√n ≤ re s (D-036 §3 (I)): then |1+1/s| ≤ 1 + 1/(2√n) and the n-th power\nis ≤ e^{√n/2}. -/\ntheorem kFun_shift_norm_le_exp_sqrt_half_add_one {n : ℕ} {s : ℂ}\n    (hn : 0 < n) (hσ : 2 * Real.sqrt (n : ℝ) ≤ s.re) :\n    ‖kFun n (s + 1)‖ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by\n  have hnR : (0:ℝ) < (n : ℝ) := by exact_mod_cast hn\n  have hsqrt : 0 < Real.sqrt (n : ℝ) := Real.sqrt_pos_of_pos hnR  -- name?\n  have hs0 : s ≠ 0 := by\n    intro h\n    rw [h] at hσ\n    simp at hσ  -- s.re = 0: 2√n ≤ 0 contradiction\n    linarith [hsqrt]\n  have hnorm_s : 2 * Real.sqrt (n : ℝ) ≤ ‖s‖ :=\n    hσ.trans (by rw [← abs_of_nonneg (by linarith [hsqrt.le] : 0 ≤ s.re)]; exact Complex.abs_re_le_norm s)\n  -- 1/‖s‖ ≤ 1/(2√n)\n  have h1 : ‖1 + 1 / s‖ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by\n    calc ‖1 + 1 / s‖ ≤ ‖(1 : ℂ)‖ + ‖1 / s‖ := norm_add_le _ _\n      _ = 1 + 1 / ‖s‖ := by rw [norm_one, norm_div, norm_one]\n      _ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by\n          have := (div_le_div_left one_pos hnorm_pos hnorm_pos').mpr hnorm_s  -- careful names\n          linarith [this]\n  ...\n```\n\nGetting long. The div comparisons: 1/‖s‖ ≤ 1/(2√n) ⟺ 2√n ≤ ‖s‖ (both positive): `div_le_div_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a/b ≤ a/c ↔ c ≤ b` — with a=1, b=‖s‖, c=2√n: (div_le_div_left one_pos hnorms h2sqrt).mpr hnorm_s where hnorms : 0 < ‖s‖ (from 2√n ≤ ‖s‖, 2√n > 0), h2sqrt : 0 < 2√n.\n\nThen (1 + 1/(2√n))^n ≤ exp(√n/2): add_one_le_exp (1/(2√n)): 1 + 1/(2√n) ≤ exp(1/(2√n)); ^n ≤ exp(n·(1/(2√n))) = exp(√n/2): n·(1/(2√n)) = n/(2√n) = √n/2: n = √n·√n: `Real.mul_self_sqrt hnR.le : √n·√n = n`. n/(2√n): = (√n·√n)/(2√n) = √n/2. In Lean: \n```lean\nhave hexp : ((Real.exp (1 / (2 * Real.sqrt (n:ℝ)))) ^ n) = Real.exp (Real.sqrt (n:ℝ) / 2) := by\n  rw [← Real.exp_nat_mul]\n  congr 1\n  field_simp [hsqrt.ne']  -- n * (1/(2√n)) = √n/2\n  -- n * (1/(2√n)) = n/(2√n); = √n/2 ⟺ 2n = 2√n·√n hmm\n  rw [Real.mul_self_sqrt hnR.le]  -- replace n by √n*√n? direction\n```\nGoal: ↑n * (1 / (2 * √↑n)) = √↑n / 2. field_simp: multiply out: ↑n * 2 = √↑n * (2 * √↑n)?? = 2·(√n)² = 2n ✓. So field_simp then need 2n = 2(√n)²: `ring_nf` then rw mul_self_sqrt... messy; do:\n```lean\n  have e : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ))) = Real.sqrt (n : ℝ) / 2 := by\n    field_simp\n    rw [mul_comm]  -- hmm\n    -- goal after field_simp: √n * (2 * √n) = n * 2? let me just: field_simp clears: n * 2 = √n * (2 * √n)?\n    -- then: √n * (2*√n) = 2*(√n*√n) = 2n ✓\n    rw [mul_comm (Real.sqrt (n:ℝ)) (2 * Real.sqrt (n:ℝ)), ← mul_assoc]  -- \n    ...\n```\nSimpler:\n```lean\n  have e : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ))) = Real.sqrt (n : ℝ) / 2 := by\n    rw [mul_one_div, eq_div_iff (by positivity : (0:ℝ) < 2)]\n    -- n / (2√n) = √n/2 ⟺ n = √n/2 · 2√n... eq_div_iff: a/c = b ↔ a = b * c: goal n = (√n/2)·(2√n)\n    have h := Real.mul_self_sqrt hnR.le\n    nlinarith [h]  -- (√n/2)*(2√n) = √n*√n = n\n```\nnlinarith with h : √n·√n = n: goal ↑n = (√↑n/2)*(2*√↑n): nlinarith should find: (√n/2)*(2*√n) = (√n*√n)·(2/2) = n ✓ — nlinarith multiplies hypotheses pairs; the equality is direct from h by ring-like: nlinarith can do it (it considers products). Or: `linear_combination h`?? (√n/2)*(2*√n) − n = √n·√n − n... `linear_combination h` works for linear combos: goal n = (√n/2)(2√n) ⟺ n − (√n/2)(2√n) = 0; h : √n·√n − n = 0... not linearly equal — it's equal as ring identity after expanding: (√n/2)(2√n) = √n√n·(2/2)= √n√n. `linear_combination h` handles: goal − 1·h = ... n − (√n/2)(2√n) − (√n√n − n) = 2n − √n√n − √n√n hmm that's not 0 as ring identity... 2n − 2√n√n — with h as atom? linear_combination treats √n·√n as nonlinear atom √n√n: goal LHS−RHS = n − √n√n·(2/2)... ugh. Let me just: `rw [div_mul_eq_mul_div, mul_comm, ← mul_assoc]`... \n\nCleanest:\n```lean\n  have e : (n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ))) = Real.sqrt (n : ℝ) / 2 := by\n    rw [mul_one_div, div_eq_div_iff (by positivity) (by norm_num : (0:ℝ) < 2)]\n    -- n * 2 = √n * (2 * √n)\n    rw [mul_comm (Real.sqrt _) (2 * _), ← mul_assoc 2 (Real.sqrt _) (Real.sqrt _), Real.mul_self_sqrt hnR.le]\n    ring\n```\ndiv_eq_div_iff (hb : 0 < b) (hd : 0 < d)? : a/b = c/d ↔ a*d = c*b ✓ exists (div_eq_div_iff). Goal: ↑n/(2√n) = √n/2 ⟺ ↑n·2 = √n·(2√n). RHS: √n·(2√n) = 2·√n·√n = 2n ✓. rw chain: mul_comm √n (2√n) : (2√n)·√n; ← mul_assoc: 2·(√n·√n); rw mul_self_sqrt: 2·n; ring closes n·2 = 2·n ✓. OK.\n\nHmm — Real.sqrt_pos_of_pos name: `Real.sqrt_pos_of_pos (h : 0 < x) : 0 < √x`? There's `Real.sqrt_pos.2`... `Real.sqrt_pos_of_pos` hmm: I recall `Real.sqrt_pos_of_pos : 0 < x → 0 < sqrt x`? or `Real.sqrt_pos.mpr`. positivity can also prove 0 < √n given hnR in context? positivity extension for sqrt: `Real.sqrt` positivity: 0 ≤ √x always; 0 < √x needs x ≠ 0 in context — positivity might not find it. Use `Real.sqrt_pos_of_pos hnR` and adjust if name wrong.\n\nkFun(−2):\n```lean\n/-- **L1 (trivial-zero term)**: kFun n (−2) = (2/3)ⁿ − 1. -/\ntheorem kFun_neg_two (n : ℕ) : kFun n (-2) = (2 / 3 : ℂ) ^ n - 1 := by\n  unfold kFun\n  congr 1\n  norm_num  -- (-2)/(-2-1) = 2/3\n```\n(-2 : ℂ)/(-2 - 1) = 2/3: norm_num should evaluate: (−2)/(−3) = 2/3 ✓ (norm_num handles division of numerals). congr 1 on ((−2)/(−2−1))^n − 1 = (2/3)^n − 1 gives ((−2)/(−2−1))^n = (2/3)^n then congr 1 again or `norm_num [kFun]`... Try `simp [kFun]; norm_num`.\n\n```lean\n/-- ‖kFun n (−2)‖ ≤ 1: the trivial-zero contribution is harmless. -/\ntheorem norm_kFun_neg_two_le_one (n : ℕ) : ‖kFun n (-2)‖ ≤ 1 := by\n  rw [kFun_neg_two]\n  have h : ((2 / 3 : ℂ) ^ n - 1) = (((2 / 3 : ℝ) ^ n - 1 : ℝ) : ℂ) := by\n    push_cast\n    ring  -- hmm ofReal_pow etc.\n  rw [h, Complex.norm_ofReal? ...]\n```\nThe cast: ((2/3 : ℂ)^n) = ((2/3:ℝ)^n : ℂ): (2/3 : ℂ) = ((2/3:ℝ) : ℂ) ✓ norm_num; ((↑r)^n = ↑(r^n)) `Complex.ofReal_pow` ✓ simp lemma. So:\n```lean\n  have h : (2 / 3 : ℂ) ^ n - 1 = (((2 / 3 : ℝ) ^ n - 1 : ℝ) : ℂ) := by\n    norm_cast  -- hmm: ((2/3:ℂ)^n − 1) vs ↑(2/3^n − 1): simp [Complex.ofReal_pow, ...]\n```\n`push_cast; ring`? push_cast turns ↑(r^n − 1) into (↑r)^n − 1... goal: (2/3:ℂ)^n − 1 = ↑((2/3)^n − 1): push_cast on RHS: ((2/3:ℝ):ℂ)^n − (1:ℂ)... then need ((2/3:ℂ)) = ((2/3:ℝ):ℂ): `norm_num1`? Try: `push_cast; ring`— after push_cast goal might be (2/3)^n − 1 = (2/3)^n − 1 with mixed casts — ring won't unify different atoms ((2/3:ℂ) vs ↑((2/3:ℝ))). Hmm. Do: `have h23 : (2/3 : ℂ) = ((2/3 : ℝ) : ℂ) := by norm_num` then rw [h23]; push_cast; ring? push_cast on goal ↑(2/3^n − 1) → (↑(2/3))^n − 1: ofReal_pow is a push_cast lemma ✓; ofReal_one... then ring? Atoms: ((2/3:ℝ):ℂ) same on both sides ✓ ring closes (or rfl).\n\nThen:\n```lean\n  rw [h, Complex.norm_ofReal]  -- ‖↑x‖ = |x|  (name check: Complex.norm_ofReal? or RCLike.norm_ofReal)\n  have h01 : (0:ℝ) ≤ (2/3)^n := by positivity\n  have h1le : (2/3 : ℝ)^n ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)\n  rw [abs_of_nonpos (by linarith)]\n  linarith\n```\nComplex.norm_ofReal: `Complex.norm_ofReal (r : ℝ) : ‖(r : ℂ)‖ = |r|`? I believe `Complex.norm_ofReal` exists — RCLike.norm_ofReal is `‖(r : K)‖ = |r|` (from the grep: RCLike/Basic.lean:246). So use `RCLike.norm_ofReal` or `Complex.norm_ofReal` (probably exists as alias). I'll write `Complex.norm_ofReal` and fix if needed.\n\nOK — that's the full §4 draft. Let me also double check `norm_div`, `norm_pow`, `norm_one`, `norm_add_le`, `norm_sub_le` — all standard ✓.\n\nOne thing in kFun_norm_le_two: nlinarith for hnorm: h : ‖s‖^2 ≤ ‖s−1‖^2, nonnegs ⟹ ‖s‖ ≤ ‖s−1‖: nlinarith needs to derive: if not, ‖s‖ > ‖s−1‖ ≥ 0 ⟹ ‖s‖² > ‖s−1‖²: nlinarith multiplies (‖s‖ − ‖s−1‖)(‖s‖ + ‖s−1‖) > 0 — nlinarith's product strategy should find: (‖s‖ − ‖s−1‖) > 0 assumed (negation), times (‖s‖ + ‖s−1‖) ≥ 0... nlinarith [norm_nonneg s, norm_nonneg (s-1), h] — goal ‖s‖ ≤ ‖s−1‖ — nlinarith proves by contradiction: assumes ‖s‖ > ‖s−1‖, needs ‖s‖^2 > ‖s−1‖^2: it can multiply the assumption by itself: (‖s‖ − ‖s−1‖) > 0 and (‖s‖ + ‖s−1‖) > 0 (from norm_nonneg + the assumption)... nlinarith considers pairwise products of hypotheses/goal-negation — (‖s‖−‖s−1‖)·(‖s‖+‖s−1‖) = ‖s‖²−‖s−1‖² > 0 needs the product of goal-negation with (‖s‖+‖s−1‖ > 0) — the latter isn't a hypothesis but follows from norm_nonneg s + assumption ‖s‖ > ‖s−1‖... nlinarith's preprocessing (positivity of products) might or might not find it. Safer: use sq_le_sq₀ directly: `(sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h` where h : ‖s‖^2 ≤ ‖s−1‖^2 ✓ CLEAN. sq_le_sq₀ : a^2 ≤ b^2 ↔ a ≤ b given nonneg — .mp h ✓.\n\nSimilarly hcmp at the end of norm_one_add_one_div_le: `(sq_le_sq₀ (norm_nonneg _) hRHS).mp hcmp` ✓.\n\nLet me now also double check `Complex.normSq_apply : normSq z = z.re ^ 2 + z.im ^ 2`? or mul form? Mathlib: `Complex.normSq_apply (z : ℂ) : normSq z = z.re * z.re + z.im * z.im` — I think it's mul form! (`normSq_mk : (⟨x, y⟩ : ℂ).normSq = x*x + y*y`.) OK — forms differ but field_simp/ring/nlinarith handle either as long as I rw consistently.\n\nIn norm_one_add_one_div_le's hsq: after rw [Complex.normSq_apply, h1, h2, Complex.normSq_apply]: LHS = (1 + σ/D')^2 + (−T/D')^2 — wait normSq_apply gives re^2... if mul form: (1+σ/D)*(1+σ/D) + ... fine. But CAREFUL: the second Complex.normSq_apply rewrites `normSq s` occurrences — which appear inside h1/h2-substituted terms as `Complex.normSq s`? h1 : (1+1/s).re = 1 + s.re / Complex.normSq s — after rw h1, the goal has normSq s occurrences; rw [Complex.normSq_apply] rewrites those to σ*σ+T*T ✓ (first normSq_apply already consumed the LHS outer one... rw rewrites ALL instances simultaneously! rw [Complex.normSq_apply] rewrites ALL normSq occurrences in one go. So `rw [Complex.normSq_apply, h1, h2]` — the first rw hits both the outer (1+1/s) normSq AND... no wait — at that point the goal is `normSq (1+1/s) = 1 + (2σ+1)/normSq s`: first rw [normSq_apply] would rewrite BOTH `normSq (1+1/s)` AND `normSq s` (all instances!). Hmm — that rewrites the RHS denominator too — fine actually! Then rw [h1, h2] — but h1/h2 mention `Complex.normSq s` which no longer appears (already rewritten to σ*σ+T*T)! rw [h1] fails (pattern not found). \n\nReorder: rw [h1, h2] FIRST? h1 : (1+1/s).re = ... — but the goal at that point is `normSq (1+1/s) = ...` — h1's LHS pattern `(1+1/s).re` doesn't appear. Need normSq_apply first to expose (1+1/s).re. ARGH — circular. Solution: `conv_lhs => rw [Complex.normSq_apply]` to target only LHS. Or: rw [Complex.normSq_apply (1 + 1/s)] — with explicit argument! `Complex.normSq_apply (1 + 1/s)` rewrites only that instance? rw with explicit arg rewrites instances of that specific application ✓ `rw [Complex.normSq_apply (1 + 1/s)]` targets normSq (1+1/s) only ✓. Then rw [h1, h2], then rw [Complex.normSq_apply s] for the denominator ✓.\n\nSimilarly elsewhere — be careful with rw + normSq_apply: use explicit args.\n\nAlso `simp [add_re, one_re, Complex.div_re]` for h1 — add_re : (z+w).re = z.re + w.re ✓ simp lemma; one_re ✓; div_re ✓. The goal: (1 + 1/s).re = 1 + s.re/normSq s: simp [Complex.add_re, Complex.one_re, Complex.div_re, Complex.one_im] then ring_nf? Let me just compute via simp then norm_num/field_simp+ring. I'll iterate.\n\nTime to write §4 and compile. Also `Finset.card_image_le` name check — it compiled already in §3 ✓.\n\nOne more name: `Real.sqrt_pos_of_pos`: I think it's `Real.sqrt_pos_of_pos (h : 0 < x) : 0 < sqrt x`? hmm — might be `Real.sqrt_pos.mpr : 0 < x → 0 < √x` (Real.sqrt_pos : 0 < √x ↔ 0 < x). I'll use `Real.sqrt_pos.mpr hnR` — safer bet (iff form standard).","signature":""},{"type":"text","text":"All names confirmed. Writing §4 (L1 kernel bounds) into LiContour.lean."},{"type":"tool_use","id":"Edit_81","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiContour.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 4. L1: kernel norm bounds (D-036 §3) -/\n\n/-- On re s ≤ 1/2 the ratio satisfies ‖s/(s−1)‖ ≤ 1 (i.e. ‖s‖ ≤ ‖s−1‖:\nre s ≤ 1/2 ⟺ 0 ≤ 1 − 2·re s ⟺ re s² + im s² ≤ (re s − 1)² + im s²). -/\ntheorem norm_div_sub_one_le_one {s : ℂ} (hs : s.re ≤ 1 / 2) : ‖s / (s - 1)‖ ≤ 1 := by\n  have hs1 : s ≠ 1 := by\n    rintro h\n    rw [h] at hs\n    simp only [Complex.one_re] at hs\n    norm_num at hs\n  have hnorm : ‖s‖ ≤ ‖s - 1‖ := by\n    have h : ‖s‖ ^ 2 ≤ ‖s - 1‖ ^ 2 := by\n      rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]\n      rw [Complex.normSq_apply s, Complex.normSq_apply (s - 1)]\n      simp only [sub_re, one_re, sub_im, one_im, sub_zero]\n      nlinarith [hs]\n    exact (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h\n  have hpos : (0:ℝ) < ‖s - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)\n  rw [norm_div]\n  exact (div_le_one hpos).mpr hnorm\n\n/-- **L1 (left side)**: ‖kFun n s‖ ≤ 2 for re s ≤ 1/2 (D-036 §3 (III)). -/\ntheorem kFun_norm_le_two {n : ℕ} {s : ℂ} (hs : s.re ≤ 1 / 2) : ‖kFun n s‖ ≤ 2 := by\n  have h1 := norm_div_sub_one_le_one hs\n  have h2 : ‖(s / (s - 1)) ^ n‖ ≤ 1 := by\n    rw [norm_pow]\n    exact pow_le_one₀ (norm_nonneg _) h1\n  calc ‖kFun n s‖ = ‖(s / (s - 1)) ^ n - 1‖ := rfl\n    _ ≤ ‖(s / (s - 1)) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _\n    _ ≤ 1 + 1 := by rw [norm_one]; linarith [h2]\n    _ = 2 := by norm_num\n\n/-- kFun at the shifted point: kFun n (s+1) = (1 + 1/s)ⁿ − 1 (s ≠ 0). -/\ntheorem kFun_add_one {n : ℕ} {s : ℂ} (hs : s ≠ 0) :\n    kFun n (s + 1) = (1 + 1 / s) ^ n - 1 := by\n  have e : (s + 1) / (s + 1 - 1) = 1 + 1 / s := by\n    rw [show s + 1 - 1 = s by ring]\n    field_simp\n  unfold kFun\n  rw [e]\n\n/-- The horizontal core estimate: ‖1 + 1/s‖ ≤ 1 + (re s + 1)/normSq s.\nFrom ‖1+1/s‖² = 1 + (2σ+1)/D ≤ (1+(σ+1)/D)² with D = normSq s = σ² + T². -/\ntheorem norm_one_add_one_div_le {s : ℂ} (hs : s ≠ 0) :\n    ‖1 + 1 / s‖ ≤ 1 + (s.re + 1) / Complex.normSq s := by\n  have hD : (0:ℝ) < Complex.normSq s := Complex.normSq_pos.mpr hs\n  have h1 : (1 + 1 / s).re = 1 + s.re / Complex.normSq s := by\n    simp [Complex.add_re, Complex.one_re, Complex.div_re, Complex.one_im]\n  have h2 : (1 + 1 / s).im = -s.im / Complex.normSq s := by\n    simp [Complex.add_im, Complex.one_im, Complex.div_im, Complex.one_re]\n  have hsq : Complex.normSq (1 + 1 / s) = 1 + (2 * s.re + 1) / Complex.normSq s := by\n    rw [Complex.normSq_apply (1 + 1 / s), h1, h2, Complex.normSq_apply s]\n    field_simp\n    ring\n  have hRHS : (0:ℝ) ≤ 1 + (s.re + 1) / Complex.normSq s := by\n    have hsum : (0:ℝ) < Complex.normSq s + (s.re + 1) := by\n      rw [Complex.normSq_apply s]\n      nlinarith [sq_nonneg (s.re + 1 / 2), sq_nonneg s.im]\n    have e : 1 + (s.re + 1) / Complex.normSq s\n        = (Complex.normSq s + (s.re + 1)) / Complex.normSq s := by\n      field_simp\n    rw [e]\n    exact div_nonneg hsum.le hD.le\n  have hcmp : ‖1 + 1 / s‖ ^ 2 ≤ (1 + (s.re + 1) / Complex.normSq s) ^ 2 := by\n    rw [← Complex.normSq_eq_norm_sq, hsq]\n    have e : (1 + (s.re + 1) / Complex.normSq s) ^ 2\n        = 1 + (2 * s.re + 1) / Complex.normSq s\n          + (1 / Complex.normSq s + ((s.re + 1) / Complex.normSq s) ^ 2) := by\n      field_simp\n      ring\n    rw [e]\n    have hpos : (0:ℝ) ≤ 1 / Complex.normSq s + ((s.re + 1) / Complex.normSq s) ^ 2 := by\n      positivity\n    linarith\n  exact (sq_le_sq₀ (norm_nonneg _) hRHS).mp hcmp\n\n/-- **L1 (horizontals)**: ‖kFun n (s+1)‖ ≤ e⁴ + 1 for re s ≤ 3 and\nn ≤ (im s)² (D-036 §3 (II),(IV)): then |1+1/s| ≤ 1 + 4/n, and\n(1 + 4/n)ⁿ ≤ (e^{4/n})ⁿ = e⁴. -/\ntheorem kFun_shift_norm_le_exp_four_add_one {n : ℕ} {s : ℂ}\n    (hσ : s.re ≤ 3) (hT : (n : ℝ) ≤ s.im ^ 2) :\n    ‖kFun n (s + 1)‖ ≤ Real.exp 4 + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  · subst hn\n    simp only [kFun, pow_zero]\n    have : (0:ℝ) ≤ Real.exp 4 := Real.exp_nonneg 4\n    simp [this]\n  · have hnR : (1:ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n    have hTim : 0 < s.im ^ 2 := by nlinarith [hT, hnR]\n    have hs0 : s ≠ 0 := by\n      rintro h\n      rw [h, Complex.zero_im] at hTim\n      norm_num at hTim\n    have hD : (0:ℝ) < Complex.normSq s := Complex.normSq_pos.mpr hs0\n    have hDn : (n:ℝ) ≤ Complex.normSq s := by\n      rw [Complex.normSq_apply s]\n      nlinarith [hT, sq_nonneg s.re]\n    have hle : ‖1 + 1 / s‖ ≤ 1 + 4 / (n : ℝ) := by\n      refine (norm_one_add_one_div_le hs0).trans ?_\n      have hσ4 : s.re + 1 ≤ 4 := by linarith\n      have h4 : (s.re + 1) / Complex.normSq s ≤ 4 / (n : ℝ) := by\n        rcases le_or_lt 0 (s.re + 1) with hσp | hσn\n        · calc (s.re + 1) / Complex.normSq s ≤ 4 / Complex.normSq s :=\n              (div_le_div_right hD).mpr hσ4\n            _ ≤ 4 / (n : ℝ) :=\n              (div_le_div_left (by norm_num) hD (by positivity)).mpr hDn\n        · have hneg : (s.re + 1) / Complex.normSq s ≤ 0 :=\n            div_nonpos_of_nonpos_of_nonneg hσn.le hD.le\n          have hpos4 : (0:ℝ) ≤ 4 / (n : ℝ) := by positivity\n          linarith\n      linarith [h4]\n    have hpow : ‖1 + 1 / s‖ ^ n ≤ Real.exp 4 := by\n      calc ‖1 + 1 / s‖ ^ n ≤ (1 + 4 / (n : ℝ)) ^ n :=\n            pow_le_pow_left (norm_nonneg _) hle n\n        _ ≤ (Real.exp (4 / (n : ℝ))) ^ n := by\n            have h := Real.add_one_le_exp (4 / (n : ℝ))\n            exact pow_le_pow_left (by positivity) (by linarith) n\n        _ = Real.exp 4 := by\n            rw [← Real.exp_nat_mul]\n            congr 1\n            field_simp\n    rw [kFun_add_one hs0]\n    calc ‖(1 + 1 / s) ^ n - 1‖ ≤ ‖(1 + 1 / s) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _\n      _ = ‖1 + 1 / s‖ ^ n + 1 := by rw [norm_pow, norm_one]\n      _ ≤ Real.exp 4 + 1 := by linarith [hpow]\n\n/-- **L1 (right vertical)**: ‖kFun n (s+1)‖ ≤ e^{√n/2} + 1 for 0 < n and\n2√n ≤ re s (D-036 §3 (I)): then |1+1/s| ≤ 1 + 1/(2√n), whose n-th power\nis ≤ e^{n/(2√n)} = e^{√n/2}. -/\ntheorem kFun_shift_norm_le_exp_sqrt_half_add_one {n : ℕ} {s : ℂ}\n    (hn : 0 < n) (hσ : 2 * Real.sqrt (n : ℝ) ≤ s.re) :\n    ‖kFun n (s + 1)‖ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by\n  have hnR : (0:ℝ) < (n : ℝ) := by exact_mod_cast hn\n  have hsqrt : 0 < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr hnR\n  have hre0 : (0:ℝ) ≤ s.re := by linarith [hsqrt.le]\n  have hnorm_s : 2 * Real.sqrt (n : ℝ) ≤ ‖s‖ :=\n    hσ.trans (abs_of_nonneg hre0 ▸ Complex.abs_re_le_norm s)\n  have hs0 : s ≠ 0 := by\n    rintro h\n    rw [h, norm_zero] at hnorm_s\n    linarith [hsqrt]\n  have hnorm_pos : (0:ℝ) < ‖s‖ := by linarith [hsqrt]\n  have h1 : ‖1 + 1 / s‖ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by\n    calc ‖1 + 1 / s‖ ≤ ‖(1 : ℂ)‖ + ‖1 / s‖ := norm_add_le _ _\n      _ = 1 + 1 / ‖s‖ := by rw [norm_one, norm_div, norm_one]\n      _ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by\n          have h := (div_le_div_left one_pos hnorm_pos (by positivity)).mpr hnorm_s\n          linarith [h]\n  have hpow : ‖1 + 1 / s‖ ^ n ≤ Real.exp (Real.sqrt (n : ℝ) / 2) := by\n    calc ‖1 + 1 / s‖ ^ n ≤ (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n :=\n          pow_le_pow_left (norm_nonneg _) h1 n\n      _ ≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ)))) ^ n := by\n          have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : ℝ)))\n          exact pow_le_pow_left (by positivity) (by linarith) n\n      _ = Real.exp (Real.sqrt (n : ℝ) / 2) := by\n          rw [← Real.exp_nat_mul]\n          congr 1\n          rw [mul_one_div, div_eq_div_iff (by positivity) (by norm_num : (0:ℝ) < 2)]\n          rw [mul_comm (Real.sqrt (n : ℝ)) (2 * Real.sqrt (n : ℝ)),\n            ← mul_assoc 2 (Real.sqrt (n : ℝ)) (Real.sqrt (n : ℝ)),\n            Real.mul_self_sqrt hnR.le]\n          ring\n  rw [kFun_add_one hs0]\n  calc ‖(1 + 1 / s) ^ n - 1‖ ≤ ‖(1 + 1 / s) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _\n    _ = ‖1 + 1 / s‖ ^ n + 1 := by rw [norm_pow, norm_one]\n    _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by linarith [hpow]\n\n/-- **L1 (trivial-zero term)**: kFun n (−2) = (2/3)ⁿ − 1. -/\ntheorem kFun_neg_two (n : ℕ) : kFun n (-2) = (2 / 3 : ℂ) ^ n - 1 := by\n  unfold kFun\n  norm_num\n\n/-- The trivial-zero contribution is harmless: ‖kFun n (−2)‖ ≤ 1\n(it equals 1 − (2/3)ⁿ as a real absolute value). -/\ntheorem norm_kFun_neg_two_le_one (n : ℕ) : ‖kFun n (-2)‖ ≤ 1 := by\n  rw [kFun_neg_two]\n  have h23 : (2 / 3 : ℂ) = ((2 / 3 : ℝ) : ℂ) := by norm_num\n  rw [h23]\n  have h : (((2 / 3 : ℝ) : ℂ) ^ n - 1) = (((2 / 3 : ℝ) ^ n - 1 : ℝ) : ℂ) := by\n    push_cast\n    ring\n  rw [h, Complex.norm_ofReal]\n  have h01 : (0:ℝ) ≤ (2 / 3 : ℝ) ^ n := by positivity\n  have h1le : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)\n  rw [abs_of_nonpos (by linarith)]\n  linarith\n\nend NguyenRH1\n\nend"},"extra_content":null}]