← Session 21 — Tier ii′ planning + launch: close SfBoundProp in Lean (D-064)
thinking (7085 chars)
The MapsTo lemma names:
- `mapsTo_rectangleBorder_left_re` (left vertical: z.re + yI)
- `mapsTo_rectangleBorder_right_re` (right vertical: w.re + yI)
- `mapsTo_rectangleBorder_left_im` (bottom: x + z.im·I)
- `mapsTo_rectangleBorder_right_im` (top: x + w.im·I)
Now let me write the FTC lemma cleanly with these. The RectangleIntegral:
= H bottom(z.im) − H top(w.im) + I·V right(w.re) − I·V left(z.re)
HIntegral G' z.re w.re y = G(w.re + yI) − G(z.re + yI) for y ∈ {z.im, w.im} — wait, the FTC gives it for any y (given differentiability on the segment). VIntegral G' x y₁ y₂ = I·∫_{y₁}^{y₂} G'(x + yI) dy = I·[G(x + y₂I) − G(x + y₁I)]/I?? — no: the parametrization y ↦ G(x + yI) has derivative G'(x+yI)·I: ∫_{y₁}^{y₂} G'(x+yI)·I dy = G(x+y₂I) − G(x+y₁I). And VIntegral G' x y₁ y₂ = I·∫ G'(x+yI) dy — the integrand is G'(x+yI) (NOT times I). So ∫_{y₁}^{y₂} G'(x+yI) dy = (G(x+y₂I) − G(x+y₁I))/I. Then I·[that] = G(x+y₂I) − G(x+y₁I) ✓.
Hmm wait — I need ∫ G'(x+yI) dy where G' = deriv G: the parametrized derivative of y ↦ G(x+yI) is deriv G (x+yI) * I (chain rule with inner deriv I). So ∫_{y₁}^{y₂} [deriv G (x+yI) * I] dy = G(x+y₂I) − G(x+y₁I). So ∫ G'(x+yI) dy = (G(x+y₂I) − G(x+y₁I))/I = −I·(G(x+y₂I) − G(x+y₁I)) (since 1/I = −I). Then VIntegral = I·∫ = I·(−I)·(ΔG) = ΔG ✓ — wait: I·(−I) = −I² = 1 ✓. So VIntegral G' x y₁ y₂ = G(x + y₂I) − G(x + y₁I).
Sum: H_bottom − H_top + V_right − V_left
= [G(b) − G(a)] − [G(d) − G(c)] + [G(d) − G(b)] − [G(c) − G(a)] where a = z.re+z.im·I (bottom-left), b = w.re+z.im·I (bottom-right), c = z.re+w.im·I (top-left), d = w.re+w.im·I (top-right).
Wait — careful with VIntegral signs: V right = VIntegral G' w.re z.im w.im = G(w.re + w.im·I) − G(w.re + z.im·I) = G(d) − G(b). V left = VIntegral G' z.re z.im w.im = G(z.re + w.im·I) − G(z.re + z.im·I) = G(c) − G(a). H bottom = HIntegral G' z.re w.re z.im = G(b) − G(a). H top = HIntegral G' z.re w.re w.im = G(d) − G(c).
Sum: (G(b)−G(a)) − (G(d)−G(c)) + (G(d)−G(b)) − (G(c)−G(a)) = 0 ✓✓ telescopes.
In Lean, the VIntegral handling: VIntegral f x y₁ y₂ = I • ∫ y in y₁..y₂, f (x + y * I). The parametrized FTC: ∫_{y₁}^{y₂} deriv G (x + y*I) dy — via integral_deriv_eq_sub on (fun y => G (x + y*I)) with derivative (fun y => I * deriv G (x + y*I))?? — chain rule: d/dy [G(x + yI)] = deriv G (x+yI) · d/dy[x + yI] = deriv G (x+yI) · I. So the integrand of VIntegral is deriv G (x+yI), and FTC applies to the integrand (fun y => I * deriv G (x+yI))... mismatch: VIntegral's integrand is deriv G (x+yI) (no I factor). So ∫ deriv G (x+yI) dy ≠ directly G-diff. Instead: ∫_{y₁}^{y₂} deriv G (x+yI) dy = (1/I)·∫ I·deriv G (x+yI) dy = (1/I)(G(x+y₂I) − G(x+y₁I)) — via integral_deriv_eq_sub on (fun y => I * deriv G (x+yI))... the lemma needs the integrand to BE the derivative of the parametrized function: parametrized P(y) = G(x+yI), P'(y) = I·deriv G(x+yI). So ∫ P' = P(y₂) − P(y₁): ∫ I·deriv G (x+yI) dy = G(x+y₂I) − G(x+y₁I). Then ∫ deriv G (x+yI) dy = (1/I)·∫ I·deriv G (x+yI) dy = −I·(G(x+y₂I) − G(x+y₁I)). And VIntegral = I•that = I·(−I)·Δ = Δ ✓.
In Lean:
```
have hsideV : ∀ x : ℝ, ∫ y in y₁..y₂, deriv G (x + y * I) = -I * (G (x + y₂ * I) - G (x + y₁ * I)) := by
intro x
have hd : ∀ y ∈ Set.uIcc y₁ y₂, HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by
intro y hy
have hG' := (hG _ (hymap y hy)).hasDerivAt
have h2 : HasDerivAt (fun y => x + y * I) I y := by
-- derivative of y ↦ x + yI is I
have hid := hasDerivAt_id y
-- y ↦ x + y·I = const + (y ↦ yI); derivative = I
...
convert hG'.comp y h2 using 1
ring
have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume y₁ y₂ := ...
have hftc := intervalIntegral.integral_deriv_eq_sub hd hint
-- ∫ I * deriv G = G(x+y₂I) − G(x+y₁I)
have h3 : ∫ y in y₁..y₂, deriv G (x + y * I) = (-I) * (G (x + y₂ * I) - G (x + y₁ * I)) := by
have h4 : ∫ y in y₁..y₂, I * deriv G (x + y * I) = G (x + y₂ * I) - G (x + y₁ * I) := hftc
rw [← h4]
rw [integral_smul] -- hmm I is a constant: ∫ I * f = I * ∫ f
field_simp [Complex.I_ne_zero]
-- (1/I) = -I
exact h3
```
Then VIntegral G' x y₁ y₂ = I • ∫ = I•(−I•Δ) = Δ:
```
rw [VIntegral, hsideV]
-- I • (-I • (G2 - G1)) = G2 - G1: smul_smul, I*I = -1: I * (-I * X) = -(I*I)*X = -(-1)*X = X
rw [smul_eq_mul, smul_eq_mul]
simp [Complex.I_mul_I]
```
OK. The HasDerivAt for y ↦ x + y·I: derivative I:
```
have h2 : HasDerivAt (fun y => x + y * I) I y := by
have h1 : HasDerivAt (fun y => y * I) I y := by
have hid := hasDerivAt_id y
convert hid.mul_const I using 1
simp
have hconst : HasDerivAt (fun y => x) 0 y := hasDerivAt_const y x
convert hconst.add h1 using 1
simp
```
hasDerivAt_id y : HasDerivAt id 1 y? — `hasDerivAt_id (x) : HasDerivAt id 1 x` ✓. mul_const: HasDerivAt (id * const)... hmm — `HasDerivAt.mul_const (hf : HasDerivAt f f' x) (c) : HasDerivAt (fun x => f x * c) (f' * c) x` — with f = id, f' = 1: HasDerivAt (fun x => x * I) (1 * I) x = (· * I) I ✓. Simpler: `hasDerivAt_mul_const`? For (fun y => y * I): `HasDerivAt.mul_const (hasDerivAt_id y) I : HasDerivAt (fun y => y * I) (1 * I) y` — then simp [one_mul].
And for the x-side: HasDerivAt (fun x => x + y*I) 1 x:
```
have h2 : HasDerivAt (fun x => x + y * I) 1 x := by
have hid := hasDerivAt_id x
have hconst : HasDerivAt (fun x => y * I) 0 x := hasDerivAt_const x _
convert hid.add hconst using 1
simp
```
hid.add hconst : HasDerivAt (fun x => x + y*I) (1 + 0) x ✓ simp.
The border membership maps: hymap for V-sides: `mapsTo_rectangleBorder_right_re z w : MapsTo (fun y => ↑w.re + ↑y * I) [[z.im, w.im]] (RectangleBorder z w)` — for the RIGHT side x = w.re. For LEFT side x = z.re: `mapsTo_rectangleBorder_left_re`. For H-sides: `mapsTo_rectangleBorder_left_im` (y = z.im), `mapsTo_rectangleBorder_right_im` (y = w.im).
Note the MapsTo functions use `↑x + z.im * I` with ↑x — the cast of x : ℝ to ℂ — same as (x + z.im * I) with x coerced ✓ (the `↑x` IS the coercion).
IntervalIntegrable: for the parametrized derivative: `ContinuousOn.intervalIntegrable (h : ContinuousOn f (uIcc a b))`: deriv G continuous on the segment ⟸ ContinuousAt at each border point (hGc hypothesis) — I'll pass hGc : ∀ s ∈ border, ContinuousAt (deriv G) s. Hmm — ContinuousOn from pointwise ContinuousAt on the set: `ContinuousAt.continuousOn`? No — ContinuousOn s f ⟺ ∀ x ∈ s, ContinuousWithinAt f s x. ContinuousAt ⟹ ContinuousWithinAt ✓:
```
intro x hx
exact (hGc _ (hymap x hx)).continuousWithinAt
```
And intervalIntegrable of ContinuousOn on uIcc: `ContinuousOn.intervalIntegrable (h : ContinuousOn f (Set.uIcc a b)) : IntervalIntegrable f volume a b` ✓ exists.
Also for the HasDerivAt pieces I need hG at the segment points via the mapsTo — `hymap : ∀ y ∈ uIcc, (x + y*I) ∈ border` from the MapsTo lemmas (MapsTo f s t : ∀ x ∈ s, f x ∈ t ✓).
OK — the whole FTC lemma is now clear. Let me rewrite LiPrincipal.lean's rectInt_deriv_eq_zero properly with a helper for each side, then the P assembly. Also need `Complex.I_ne_zero` and `smul_smul`.
Let me rewrite the whole file with the completed proof.
The MapsTo border lemmas exist with exact names. Rewriting LiPrincipal.lean with the complete FTC proof.
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiPrincipal.lean",
"content": "/-\nNguyenRH1/LiPrincipal.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b(ii) (D-064 \u00a74 R1):\nthe principal-part integral. For the explicit principal part\n P(w) = \u03a3_{i=1}^{n+1} A_i/(w\u22121)^i, A_i = F^{(n+1\u2212i)}(1)/(n+1\u2212i)!,\nwith F(w) = (w\u207f\u2212(w\u22121)\u207f)\u00b7hLi(w), on any rectangle with 1 in its interior:\n RectangleIntegral' P z w = A_1 = ResW1 n.\n\nMethod: P = A_1/(w\u22121) + (\u03a3_{i\u22652} A_i/(w\u22121)^i). The first term is handled\nby the vendored `ResidueTheoremInRectangle`; the tail has the explicit\nglobal primitive G(w) = \u2212\u03a3_{i\u22652} A_i/((i\u22121)(w\u22121)^{i\u22121}), differentiable\non the border (1 is interior, hence off the border), so its rectangle\nintegral vanishes by per-side FTC (`rectInt_deriv_eq_zero`).\n\nArchive references: D-036, D-064 (R1), journal-016.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ResidueCalcOnRectangles\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Linearity of rectangle integrals -/\n\nlemma HIntegral_add (f g : \u2102 \u2192 \u2102) (x\u2081 x\u2082 y : \u211d)\n (hf : IntervalIntegrable (fun x => f (x + y * I)) volume x\u2081 x\u2082)\n (hg : IntervalIntegrable (fun x => g (x + y * I)) volume x\u2081 x\u2082) :\n HIntegral (f + g) x\u2081 x\u2082 y = HIntegral f x\u2081 x\u2082 y + HIntegral g x\u2081 x\u2082 y := by\n rw [HIntegral, HIntegral, HIntegral]\n have e : (fun x => (f + g) (x + y * I)) = (fun x => f (x + y * I) + g (x + y * I)) := by\n funext x\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg]\n\nlemma VIntegral_add (f g : \u2102 \u2192 \u2102) (x y\u2081 y\u2082 : \u211d)\n (hf : IntervalIntegrable (fun y => f (x + y * I)) volume y\u2081 y\u2082)\n (hg : IntervalIntegrable (fun y => g (x + y * I)) volume y\u2081 y\u2082) :\n VIntegral (f + g) x y\u2081 y\u2082 = VIntegral f x y\u2081 y\u2082 + VIntegral g x y\u2081 y\u2082 := by\n rw [VIntegral, VIntegral, VIntegral]\n have e : (fun y => (f + g) (x + y * I)) = (fun y => f (x + y * I) + g (x + y * I)) := by\n funext y\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg, smul_add]\n\nlemma RectangleIntegral_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w := by\n rw [RectangleIntegral, RectangleIntegral, RectangleIntegral]\n obtain \u27e8\u27e8hf1, hf2\u27e9, hf3, hf4\u27e9 := hf\n obtain \u27e8\u27e8hg1, hg2\u27e9, hg3, hg4\u27e9 := hg\n rw [HIntegral_add f g _ _ _ hf1 hg1, HIntegral_add f g _ _ _ hf2 hg2,\n VIntegral_add f g _ _ _ hf3 hg3, VIntegral_add f g _ _ _ hf4 hg4]\n ring\n\nlemma RectangleIntegral'_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by\n rw [RectangleIntegral', RectangleIntegral_add f g z w hf hg, RectangleIntegral', RectangleIntegral',\n smul_add]\n\n/-! ## 2. Parametrized side derivatives and integrability -/\n\nlemma hasDerivAt_add_const_I (y : \u211d) (x : \u211d) :\n HasDerivAt (fun t => t + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun _ => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n\nlemma hasDerivAt_const_add_I (x y : \u211d) :\n HasDerivAt (fun t => x + t * I) I y := by\n have h1 : HasDerivAt (fun t => t * I) I y := by\n have := (hasDerivAt_id y).mul_const I\n simpa using this\n have hconst : HasDerivAt (fun _ => x) 0 y := hasDerivAt_const y x\n convert hconst.add h1 using 1\n simp\n\n/-- FTC on a horizontal side: \u222b_{x\u2081}^{x\u2082} (deriv G)(x + yI) dx\n= G(x\u2082 + yI) \u2212 G(x\u2081 + yI). -/\nlemma HIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (y : \u211d)\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun x : \u211d => \u2191x + y * I) [[z.re, w.re]] (RectangleBorder z w)) :\n \u222b x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by\n have hd : \u2200 x \u2208 Set.uIcc z.re w.re,\n HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by\n intro x hx\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hx |>.elim (fun h => h.1) |>.1))).hasDerivAt\n have h2 : HasDerivAt (fun x => x + y * I) 1 x := hasDerivAt_add_const_I y x\n have hcomp := h1.comp x h2\n convert hcomp using 1\n simp\n have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by\n apply ContinuousOn.intervalIntegrable\n intro x hx\n have hmem : (x + y * I) \u2208 RectangleBorder z w := by\n apply hmap\n rcases Set.uIcc_of_le (by simp [Set.uIcc]) hx with h | h\n \u00b7 exact h.1\n \u00b7 exact h.1\n exact (hGc _ hmem).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n convert hftc using 1\n \u00b7 simp\n \u00b7 simp\n\n/-- FTC on a vertical side: \u222b_{y\u2081}^{y\u2082} (deriv G)(x + yI) dy\n= \u2212I\u00b7(G(x + y\u2082I) \u2212 G(x + y\u2081I)). -/\nlemma VIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (x : \u211d)\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun y : \u211d => \u2191x + \u2191y * I) [[z.im, w.im]] (RectangleBorder z w)) :\n \u222b y in z.im..w.im, deriv G (x + y * I) =\n -I * (G (x + w.im * I) - G (x + z.im * I)) := by\n have hd : \u2200 y \u2208 Set.uIcc z.im w.im,\n HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by\n intro y hy\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hy |>.elim (fun h => h.1) |>.1))).hasDerivAt\n have h2 : HasDerivAt (fun y => x + y * I) I y := hasDerivAt_const_add_I x y\n have hcomp := h1.comp y h2\n convert hcomp using 1\n ring\n have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume z.im w.im := by\n apply ContinuousOn.intervalIntegrable\n intro y hy\n apply ContinuousWithinAt.mul continuousWithinAt_const\n have hmem : (x + y * I) \u2208 RectangleBorder z w := by\n apply hmap\n rcases Set.uIcc_of_le (by simp [Set.uIcc]) hy with h | h\n \u00b7 exact h.1\n \u00b7 exact h.1\n exact (hGc _ hmem).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n rw [\u2190 hftc]\n rw [integral_smul]\n field_simp [Complex.I_ne_zero]\n\n/-- If `G : \u2102 \u2192 \u2102` is differentiable at every point of the rectangle\nborder, then the rectangle integral of `deriv G` vanishes (each side\ntelescopes by FTC). -/\nlemma rectInt_deriv_eq_zero {G : \u2102 \u2192 \u2102} {z w : \u2102}\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s) :\n RectangleIntegral (fun s => deriv G s) z w = 0 := by\n rw [RectangleIntegral]\n rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),\n HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]\n have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)\n have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)\n rw [VIntegral, VIntegral, hVr, hVl]\n simp [Complex.I_mul_I]\n ring\n\nend NguyenRH1\n"
}
result 2026-08-21 21:29:27Z → 2026-08-21 21:29:27Z
{
"type": "update",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiPrincipal.lean",
"content": "/-\nNguyenRH1/LiPrincipal.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b(ii) (D-064 \u00a74 R1):\nthe principal-part integral. For the explicit principal part\n P(w) = \u03a3_{i=1}^{n+1} A_i/(w\u22121)^i, A_i = F^{(n+1\u2212i)}(1)/(n+1\u2212i)!,\nwith F(w) = (w\u207f\u2212(w\u22121)\u207f)\u00b7hLi(w), on any rectangle with 1 in its interior:\n RectangleIntegral' P z w = A_1 = ResW1 n.\n\nMethod: P = A_1/(w\u22121) + (\u03a3_{i\u22652} A_i/(w\u22121)^i). The first term is handled\nby the vendored `ResidueTheoremInRectangle`; the tail has the explicit\nglobal primitive G(w) = \u2212\u03a3_{i\u22652} A_i/((i\u22121)(w\u22121)^{i\u22121}), differentiable\non the border (1 is interior, hence off the border), so its rectangle\nintegral vanishes by per-side FTC (`rectInt_deriv_eq_zero`).\n\nArchive references: D-036, D-064 (R1), journal-016.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ResidueCalcOnRectangles\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Linearity of rectangle integrals -/\n\nlemma HIntegral_add (f g : \u2102 \u2192 \u2102) (x\u2081 x\u2082 y : \u211d)\n (hf : IntervalIntegrable (fun x => f (x + y * I)) volume x\u2081 x\u2082)\n (hg : IntervalIntegrable (fun x => g (x + y * I)) volume x\u2081 x\u2082) :\n HIntegral (f + g) x\u2081 x\u2082 y = HIntegral f x\u2081 x\u2082 y + HIntegral g x\u2081 x\u2082 y := by\n rw [HIntegral, HIntegral, HIntegral]\n have e : (fun x => (f + g) (x + y * I)) = (fun x => f (x + y * I) + g (x + y * I)) := by\n funext x\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg]\n\nlemma VIntegral_add (f g : \u2102 \u2192 \u2102) (x y\u2081 y\u2082 : \u211d)\n (hf : IntervalIntegrable (fun y => f (x + y * I)) volume y\u2081 y\u2082)\n (hg : IntervalIntegrable (fun y => g (x + y * I)) volume y\u2081 y\u2082) :\n VIntegral (f + g) x y\u2081 y\u2082 = VIntegral f x y\u2081 y\u2082 + VIntegral g x y\u2081 y\u2082 := by\n rw [VIntegral, VIntegral, VIntegral]\n have e : (fun y => (f + g) (x + y * I)) = (fun y => f (x + y * I) + g (x + y * I)) := by\n funext y\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg, smul_add]\n\nlemma RectangleIntegral_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w := by\n rw [RectangleIntegral, RectangleIntegral, RectangleIntegral]\n obtain \u27e8\u27e8hf1, hf2\u27e9, hf3, hf4\u27e9 := hf\n obtain \u27e8\u27e8hg1, hg2\u27e9, hg3, hg4\u27e9 := hg\n rw [HIntegral_add f g _ _ _ hf1 hg1, HIntegral_add f g _ _ _ hf2 hg2,\n VIntegral_add f g _ _ _ hf3 hg3, VIntegral_add f g _ _ _ hf4 hg4]\n ring\n\nlemma RectangleIntegral'_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by\n rw [RectangleIntegral', RectangleIntegral_add f g z w hf hg, RectangleIntegral', RectangleIntegral',\n smul_add]\n\n/-! ## 2. Parametrized side derivatives and integrability -/\n\nlemma hasDerivAt_add_const_I (y : \u211d) (x : \u211d) :\n HasDerivAt (fun t => t + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun _ => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n\nlemma hasDerivAt_const_add_I (x y : \u211d) :\n HasDerivAt (fun t => x + t * I) I y := by\n have h1 : HasDerivAt (fun t => t * I) I y := by\n have := (hasDerivAt_id y).mul_const I\n simpa using this\n have hconst : HasDerivAt (fun _ => x) 0 y := hasDerivAt_const y x\n convert hconst.add h1 using 1\n simp\n\n/-- FTC on a horizontal side: \u222b_{x\u2081}^{x\u2082} (deriv G)(x + yI) dx\n= G(x\u2082 + yI) \u2212 G(x\u2081 + yI). -/\nlemma HIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (y : \u211d)\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun x : \u211d => \u2191x + y * I) [[z.re, w.re]] (RectangleBorder z w)) :\n \u222b x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by\n have hd : \u2200 x \u2208 Set.uIcc z.re w.re,\n HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by\n intro x hx\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hx |>.elim (fun h => h.1) |>.1))).hasDerivAt\n have h2 : HasDerivAt (fun x => x + y * I) 1 x := hasDerivAt_add_const_I y x\n have hcomp := h1.comp x h2\n convert hcomp using 1\n simp\n have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by\n apply ContinuousOn.intervalIntegrable\n intro x hx\n have hmem : (x + y * I) \u2208 RectangleBorder z w := by\n apply hmap\n rcases Set.uIcc_of_le (by simp [Set.uIcc]) hx with h | h\n \u00b7 exact h.1\n \u00b7 exact h.1\n exact (hGc _ hmem).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n convert hftc using 1\n \u00b7 simp\n \u00b7 simp\n\n/-- FTC on a vertical side: \u222b_{y\u2081}^{y\u2082} (deriv G)(x + yI) dy\n= \u2212I\u00b7(G(x + y\u2082I) \u2212 G(x + y\u2081I)). -/\nlemma VIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (x : \u211d)\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun y : \u211d => \u2191x + \u2191y * I) [[z.im, w.im]] (RectangleBorder z w)) :\n \u222b y in z.im..w.im, deriv G (x + y * I) =\n -I * (G (x + w.im * I) - G (x + z.im * I)) := by\n have hd : \u2200 y \u2208 Set.uIcc z.im w.im,\n HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by\n intro y hy\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hy |>.elim (fun h => h.1) |>.1))).hasDerivAt\n have h2 : HasDerivAt (fun y => x + y * I) I y := hasDerivAt_const_add_I x y\n have hcomp := h1.comp y h2\n convert hcomp using 1\n ring\n have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume z.im w.im := by\n apply ContinuousOn.intervalIntegrable\n intro y hy\n apply ContinuousWithinAt.mul continuousWithinAt_const\n have hmem : (x + y * I) \u2208 RectangleBorder z w := by\n apply hmap\n rcases Set.uIcc_of_le (by simp [Set.uIcc]) hy with h | h\n \u00b7 exact h.1\n \u00b7 exact h.1\n exact (hGc _ hmem).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n rw [\u2190 hftc]\n rw [integral_smul]\n field_simp [Complex.I_ne_zero]\n\n/-- If `G : \u2102 \u2192 \u2102` is differentiable at every point of the rectangle\nborder, then the rectangle integral of `deriv G` vanishes (each side\ntelescopes by FTC). -/\nlemma rectInt_deriv_eq_zero {G : \u2102 \u2192 \u2102} {z w : \u2102}\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s) :\n RectangleIntegral (fun s => deriv G s) z w = 0 := by\n rw [RectangleIntegral]\n rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),\n HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]\n have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)\n have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)\n rw [VIntegral, VIntegral, hVr, hVl]\n simp [Complex.I_mul_I]\n ring\n\nend NguyenRH1\n",
"structuredPatch": [
{
"oldStart": 61,
"oldLines": 7,
"newStart": 61,
"newLines": 85,
"lines": [
" rw [RectangleIntegral', RectangleIntegral_add f g z w hf hg, RectangleIntegral', RectangleIntegral',",
" smul_add]",
" ",
"-/-! ## 2. The per-side FTC vanishing lemma -/",
"+/-! ## 2. Parametrized side derivatives and integrability -/",
"+",
"+lemma hasDerivAt_add_const_I (y : \u211d) (x : \u211d) :",
"+ HasDerivAt (fun t => t + y * I) 1 x := by",
"+ have hid := hasDerivAt_id x",
"+ have hconst : HasDerivAt (fun _ => y * I) 0 x := hasDerivAt_const x _",
"+ convert hid.add hconst using 1",
"+ simp",
"+",
"+lemma hasDerivAt_const_add_I (x y : \u211d) :",
"+ HasDerivAt (fun t => x + t * I) I y := by",
"+ have h1 : HasDerivAt (fun t => t * I) I y := by",
"+ have := (hasDerivAt_id y).mul_const I",
"+ simpa using this",
"+ have hconst : HasDerivAt (fun _ => x) 0 y := hasDerivAt_const y x",
"+ convert hconst.add h1 using 1",
"+ simp",
"+",
"+/-- FTC on a horizontal side: \u222b_{x\u2081}^{x\u2082} (deriv G)(x + yI) dx",
"+= G(x\u2082 + yI) \u2212 G(x\u2081 + yI). -/",
"+lemma HIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (y : \u211d)",
"+ (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)",
"+ (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)",
"+ (hmap : MapsTo (fun x : \u211d => \u2191x + y * I) [[z.re, w.re]] (RectangleBorder z w)) :",
"+ \u222b x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by",
"+ have hd : \u2200 x \u2208 Set.uIcc z.re w.re,",
"+ HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by",
"+ intro x hx",
"+ have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=",
"+ (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hx |>.elim (fun h => h.1) |>.1))).hasDerivAt",
"+ have h2 : HasDerivAt (fun x => x + y * I) 1 x := hasDerivAt_add_const_I y x",
"+ have hcomp := h1.comp x h2",
"+ convert hcomp using 1",
"+ simp",
"+ have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by",
"+ apply ContinuousOn.intervalIntegrable",
"+ intro x hx",
"+ have hmem : (x + y * I) \u2208 RectangleBorder z w := by",
"+ apply hmap",
"+ rcases Set.uIcc_of_le (by simp [Set.uIcc]) hx with h | h",
"+ \u00b7 exact h.1",
"+ \u00b7 exact h.1",
"+ exact (hGc _ hmem).continuousWithinAt",
"+ have hftc := intervalIntegral.integral_deriv_eq_sub hd hint",
"+ convert hftc using 1",
"+ \u00b7 simp",
"+ \u00b7 simp",
"+",
"+/-- FTC on a vertical side: \u222b_{y\u2081}^{y\u2082} (deriv G)(x + yI) dy",
"+= \u2212I\u00b7(G(x + y\u2082I) \u2212 G(x + y\u2081I)). -/",
"+lemma VIntegral_deriv {G : \u2102 \u2192 \u2102} {z w : \u2102} (x : \u211d)",
"+ (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)",
"+ (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s)",
"+ (hmap : MapsTo (fun y : \u211d => \u2191x + \u2191y * I) [[z.im, w.im]] (RectangleBorder z w)) :",
"+ \u222b y in z.im..w.im, deriv G (x + y * I) =",
"+ -I * (G (x + w.im * I) - G (x + z.im * I)) := by",
"+ have hd : \u2200 y \u2208 Set.uIcc z.im w.im,",
"+ HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by",
"+ intro y hy",
"+ have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=",
"+ (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hy |>.elim (fun h => h.1) |>.1))).hasDerivAt",
"+ have h2 : HasDerivAt (fun y => x + y * I) I y := hasDerivAt_const_add_I x y",
"+ have hcomp := h1.comp y h2",
"+ convert hcomp using 1",
"+ ring",
"+ have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume z.im w.im := by",
"+ apply ContinuousOn.intervalIntegrable",
"+ intro y hy",
"+ apply ContinuousWithinAt.mul continuousWithinAt_const",
"+ have hmem : (x + y * I) \u2208 RectangleBorder z w := by",
"+ apply hmap",
"+ rcases Set.uIcc_of_le (by simp [Set.uIcc]) hy with h | h",
"+ \u00b7 exact h.1",
"+ \u00b7 exact h.1",
"+ exact (hGc _ hmem).continuousWithinAt",
"+ have hftc := intervalIntegral.integral_deriv_eq_sub hd hint",
"+ rw [\u2190 hftc]",
"+ rw [integral_smul]",
"+ field_simp [Complex.I_ne_zero]",
" ",
" /-- If `G : \u2102 \u2192 \u2102` is differentiable at every point of the rectangle",
" border, then the rectangle integral of `deriv G` vanishes (each side"
]
},
{
"oldStart": 71,
"oldLines": 31,
"newStart": 149,
"newLines": 13,
"lines": [
" (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s) :",
" RectangleIntegral (fun s => deriv G s) z w = 0 := by",
" rw [RectangleIntegral]",
"- have hsideH : \u2200 y : \u211d, (\u2200 x : \u211d, x \u2208 Set.uIcc z.re w.re \u2192 (x + y * I) \u2208 RectangleBorder z w) \u2192",
"- \u222b x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by",
"- intro y hy",
"- have hd : \u2200 x \u2208 Set.uIcc z.re w.re,",
"- HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by",
"- intro x hx",
"- have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=",
"- (hG _ (hy x hx)).hasDerivAt",
"- have h2 : HasDerivAt (fun x => x + y * I) 1 x := by",
"- have hid := hasDerivAt_id x",
"- have hconst : HasDerivAt (fun x => y * I) 0 x := hasDerivAt_const x _",
"- convert hid.add hconst using 1",
"- simp",
"- have := h1.comp x h2",
"- convert this using 1",
"- simp",
"- have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by",
"- apply ContinuousOn.intervalIntegrable_of_Icc (a := z.re) (b := w.re)",
"- intro x hx",
"- have hmem : (x + y * I) \u2208 RectangleBorder z w := hy x (Set.uIcc_of_le ?_ hx |>.elim (fun h => h.1) )",
"- \u00b7 exact (hGc _ hmem).continuousWithinAt",
"- \u00b7 sorry",
"- have := intervalIntegral.integral_deriv_eq_sub hd hint",
"- convert this using 1",
"- sorry",
"+ rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),",
"+ HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]",
"+ have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)",
"+ have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)",
"+ rw [VIntegral, VIntegral, hVr, hVl]",
"+ simp [Complex.I_mul_I]",
"+ ring",
" ",
" end NguyenRH1",
" "
]
}
],
"originalFile": "/-\nNguyenRH1/LiPrincipal.lean \u2014 tier ii\u2032 sub-stage ii\u2032-1b(ii) (D-064 \u00a74 R1):\nthe principal-part integral. For the explicit principal part\n P(w) = \u03a3_{i=1}^{n+1} A_i/(w\u22121)^i, A_i = F^{(n+1\u2212i)}(1)/(n+1\u2212i)!,\nwith F(w) = (w\u207f\u2212(w\u22121)\u207f)\u00b7hLi(w), on any rectangle with 1 in its interior:\n RectangleIntegral' P z w = A_1 = ResW1 n.\n\nMethod: P = A_1/(w\u22121) + (\u03a3_{i\u22652} A_i/(w\u22121)^i). The first term is handled\nby the vendored `ResidueTheoremInRectangle`; the tail has the explicit\nglobal primitive G(w) = \u2212\u03a3_{i\u22652} A_i/((i\u22121)(w\u22121)^{i\u22121}), differentiable\non the border (1 is interior, hence off the border), so its rectangle\nintegral vanishes by per-side FTC (`rectInt_deriv_eq_zero`).\n\nArchive references: D-036, D-064 (R1), journal-016.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ResidueCalcOnRectangles\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Linearity of rectangle integrals -/\n\nlemma HIntegral_add (f g : \u2102 \u2192 \u2102) (x\u2081 x\u2082 y : \u211d)\n (hf : IntervalIntegrable (fun x => f (x + y * I)) volume x\u2081 x\u2082)\n (hg : IntervalIntegrable (fun x => g (x + y * I)) volume x\u2081 x\u2082) :\n HIntegral (f + g) x\u2081 x\u2082 y = HIntegral f x\u2081 x\u2082 y + HIntegral g x\u2081 x\u2082 y := by\n rw [HIntegral, HIntegral, HIntegral]\n have e : (fun x => (f + g) (x + y * I)) = (fun x => f (x + y * I) + g (x + y * I)) := by\n funext x\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg]\n\nlemma VIntegral_add (f g : \u2102 \u2192 \u2102) (x y\u2081 y\u2082 : \u211d)\n (hf : IntervalIntegrable (fun y => f (x + y * I)) volume y\u2081 y\u2082)\n (hg : IntervalIntegrable (fun y => g (x + y * I)) volume y\u2081 y\u2082) :\n VIntegral (f + g) x y\u2081 y\u2082 = VIntegral f x y\u2081 y\u2082 + VIntegral g x y\u2081 y\u2082 := by\n rw [VIntegral, VIntegral, VIntegral]\n have e : (fun y => (f + g) (x + y * I)) = (fun y => f (x + y * I) + g (x + y * I)) := by\n funext y\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg, smul_add]\n\nlemma RectangleIntegral_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w := by\n rw [RectangleIntegral, RectangleIntegral, RectangleIntegral]\n obtain \u27e8\u27e8hf1, hf2\u27e9, hf3, hf4\u27e9 := hf\n obtain \u27e8\u27e8hg1, hg2\u27e9, hg3, hg4\u27e9 := hg\n rw [HIntegral_add f g _ _ _ hf1 hg1, HIntegral_add f g _ _ _ hf2 hg2,\n VIntegral_add f g _ _ _ hf3 hg3, VIntegral_add f g _ _ _ hf4 hg4]\n ring\n\nlemma RectangleIntegral'_add (f g : \u2102 \u2192 \u2102) (z w : \u2102)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by\n rw [RectangleIntegral', RectangleIntegral_add f g z w hf hg, RectangleIntegral', RectangleIntegral',\n smul_add]\n\n/-! ## 2. The per-side FTC vanishing lemma -/\n\n/-- If `G : \u2102 \u2192 \u2102` is differentiable at every point of the rectangle\nborder, then the rectangle integral of `deriv G` vanishes (each side\ntelescopes by FTC). -/\nlemma rectInt_deriv_eq_zero {G : \u2102 \u2192 \u2102} {z w : \u2102}\n (hG : \u2200 s \u2208 RectangleBorder z w, DifferentiableAt \u2102 G s)\n (hGc : \u2200 s \u2208 RectangleBorder z w, ContinuousAt (deriv G) s) :\n RectangleIntegral (fun s => deriv G s) z w = 0 := by\n rw [RectangleIntegral]\n have hsideH : \u2200 y : \u211d, (\u2200 x : \u211d, x \u2208 Set.uIcc z.re w.re \u2192 (x + y * I) \u2208 RectangleBorder z w) \u2192\n \u222b x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by\n intro y hy\n have hd : \u2200 x \u2208 Set.uIcc z.re w.re,\n HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by\n intro x hx\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hy x hx)).hasDerivAt\n have h2 : HasDerivAt (fun x => x + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun x => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n have := h1.comp x h2\n convert this using 1\n simp\n have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by\n apply ContinuousOn.intervalIntegrable_of_Icc (a := z.re) (b := w.re)\n intro x hx\n have hmem : (x + y * I) \u2208 RectangleBorder z w := hy x (Set.uIcc_of_le ?_ hx |>.elim (fun h => h.1) )\n \u00b7 exact (hGc _ hmem).continuousWithinAt\n \u00b7 sorry\n have := intervalIntegral.integral_deriv_eq_sub hd hint\n convert this using 1\n sorry\n\nend NguyenRH1\n",
"autoRead": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"The MapsTo lemma names:\n- `mapsTo_rectangleBorder_left_re` (left vertical: z.re + yI)\n- `mapsTo_rectangleBorder_right_re` (right vertical: w.re + yI)\n- `mapsTo_rectangleBorder_left_im` (bottom: x + z.im·I)\n- `mapsTo_rectangleBorder_right_im` (top: x + w.im·I)\n\nNow let me write the FTC lemma cleanly with these. The RectangleIntegral:\n= H bottom(z.im) − H top(w.im) + I·V right(w.re) − I·V left(z.re)\n\nHIntegral G' z.re w.re y = G(w.re + yI) − G(z.re + yI) for y ∈ {z.im, w.im} — wait, the FTC gives it for any y (given differentiability on the segment). VIntegral G' x y₁ y₂ = I·∫_{y₁}^{y₂} G'(x + yI) dy = I·[G(x + y₂I) − G(x + y₁I)]/I?? — no: the parametrization y ↦ G(x + yI) has derivative G'(x+yI)·I: ∫_{y₁}^{y₂} G'(x+yI)·I dy = G(x+y₂I) − G(x+y₁I). And VIntegral G' x y₁ y₂ = I·∫ G'(x+yI) dy — the integrand is G'(x+yI) (NOT times I). So ∫_{y₁}^{y₂} G'(x+yI) dy = (G(x+y₂I) − G(x+y₁I))/I. Then I·[that] = G(x+y₂I) − G(x+y₁I) ✓.\n\nHmm wait — I need ∫ G'(x+yI) dy where G' = deriv G: the parametrized derivative of y ↦ G(x+yI) is deriv G (x+yI) * I (chain rule with inner deriv I). So ∫_{y₁}^{y₂} [deriv G (x+yI) * I] dy = G(x+y₂I) − G(x+y₁I). So ∫ G'(x+yI) dy = (G(x+y₂I) − G(x+y₁I))/I = −I·(G(x+y₂I) − G(x+y₁I)) (since 1/I = −I). Then VIntegral = I·∫ = I·(−I)·(ΔG) = ΔG ✓ — wait: I·(−I) = −I² = 1 ✓. So VIntegral G' x y₁ y₂ = G(x + y₂I) − G(x + y₁I). \n\nSum: H_bottom − H_top + V_right − V_left\n= [G(b) − G(a)] − [G(d) − G(c)] + [G(d) − G(b)] − [G(c) − G(a)] where a = z.re+z.im·I (bottom-left), b = w.re+z.im·I (bottom-right), c = z.re+w.im·I (top-left), d = w.re+w.im·I (top-right).\nWait — careful with VIntegral signs: V right = VIntegral G' w.re z.im w.im = G(w.re + w.im·I) − G(w.re + z.im·I) = G(d) − G(b). V left = VIntegral G' z.re z.im w.im = G(z.re + w.im·I) − G(z.re + z.im·I) = G(c) − G(a). H bottom = HIntegral G' z.re w.re z.im = G(b) − G(a). H top = HIntegral G' z.re w.re w.im = G(d) − G(c).\nSum: (G(b)−G(a)) − (G(d)−G(c)) + (G(d)−G(b)) − (G(c)−G(a)) = 0 ✓✓ telescopes.\n\nIn Lean, the VIntegral handling: VIntegral f x y₁ y₂ = I • ∫ y in y₁..y₂, f (x + y * I). The parametrized FTC: ∫_{y₁}^{y₂} deriv G (x + y*I) dy — via integral_deriv_eq_sub on (fun y => G (x + y*I)) with derivative (fun y => I * deriv G (x + y*I))?? — chain rule: d/dy [G(x + yI)] = deriv G (x+yI) · d/dy[x + yI] = deriv G (x+yI) · I. So the integrand of VIntegral is deriv G (x+yI), and FTC applies to the integrand (fun y => I * deriv G (x+yI))... mismatch: VIntegral's integrand is deriv G (x+yI) (no I factor). So ∫ deriv G (x+yI) dy ≠ directly G-diff. Instead: ∫_{y₁}^{y₂} deriv G (x+yI) dy = (1/I)·∫ I·deriv G (x+yI) dy = (1/I)(G(x+y₂I) − G(x+y₁I)) — via integral_deriv_eq_sub on (fun y => I * deriv G (x+yI))... the lemma needs the integrand to BE the derivative of the parametrized function: parametrized P(y) = G(x+yI), P'(y) = I·deriv G(x+yI). So ∫ P' = P(y₂) − P(y₁): ∫ I·deriv G (x+yI) dy = G(x+y₂I) − G(x+y₁I). Then ∫ deriv G (x+yI) dy = (1/I)·∫ I·deriv G (x+yI) dy = −I·(G(x+y₂I) − G(x+y₁I)). And VIntegral = I•that = I·(−I)·Δ = Δ ✓.\n\nIn Lean: \n```\nhave hsideV : ∀ x : ℝ, ∫ y in y₁..y₂, deriv G (x + y * I) = -I * (G (x + y₂ * I) - G (x + y₁ * I)) := by\n intro x\n have hd : ∀ y ∈ Set.uIcc y₁ y₂, HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by\n intro y hy\n have hG' := (hG _ (hymap y hy)).hasDerivAt\n have h2 : HasDerivAt (fun y => x + y * I) I y := by\n -- derivative of y ↦ x + yI is I\n have hid := hasDerivAt_id y\n -- y ↦ x + y·I = const + (y ↦ yI); derivative = I\n ...\n convert hG'.comp y h2 using 1\n ring\n have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume y₁ y₂ := ...\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n -- ∫ I * deriv G = G(x+y₂I) − G(x+y₁I)\n have h3 : ∫ y in y₁..y₂, deriv G (x + y * I) = (-I) * (G (x + y₂ * I) - G (x + y₁ * I)) := by\n have h4 : ∫ y in y₁..y₂, I * deriv G (x + y * I) = G (x + y₂ * I) - G (x + y₁ * I) := hftc\n rw [← h4]\n rw [integral_smul] -- hmm I is a constant: ∫ I * f = I * ∫ f\n field_simp [Complex.I_ne_zero]\n -- (1/I) = -I\n exact h3\n```\nThen VIntegral G' x y₁ y₂ = I • ∫ = I•(−I•Δ) = Δ: \n```\n rw [VIntegral, hsideV]\n -- I • (-I • (G2 - G1)) = G2 - G1: smul_smul, I*I = -1: I * (-I * X) = -(I*I)*X = -(-1)*X = X\n rw [smul_eq_mul, smul_eq_mul]\n simp [Complex.I_mul_I]\n```\n\nOK. The HasDerivAt for y ↦ x + y·I: derivative I:\n```\nhave h2 : HasDerivAt (fun y => x + y * I) I y := by\n have h1 : HasDerivAt (fun y => y * I) I y := by\n have hid := hasDerivAt_id y\n convert hid.mul_const I using 1\n simp\n have hconst : HasDerivAt (fun y => x) 0 y := hasDerivAt_const y x\n convert hconst.add h1 using 1\n simp\n```\nhasDerivAt_id y : HasDerivAt id 1 y? — `hasDerivAt_id (x) : HasDerivAt id 1 x` ✓. mul_const: HasDerivAt (id * const)... hmm — `HasDerivAt.mul_const (hf : HasDerivAt f f' x) (c) : HasDerivAt (fun x => f x * c) (f' * c) x` — with f = id, f' = 1: HasDerivAt (fun x => x * I) (1 * I) x = (· * I) I ✓. Simpler: `hasDerivAt_mul_const`? For (fun y => y * I): `HasDerivAt.mul_const (hasDerivAt_id y) I : HasDerivAt (fun y => y * I) (1 * I) y` — then simp [one_mul]. \n\nAnd for the x-side: HasDerivAt (fun x => x + y*I) 1 x:\n```\nhave h2 : HasDerivAt (fun x => x + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun x => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n```\nhid.add hconst : HasDerivAt (fun x => x + y*I) (1 + 0) x ✓ simp.\n\nThe border membership maps: hymap for V-sides: `mapsTo_rectangleBorder_right_re z w : MapsTo (fun y => ↑w.re + ↑y * I) [[z.im, w.im]] (RectangleBorder z w)` — for the RIGHT side x = w.re. For LEFT side x = z.re: `mapsTo_rectangleBorder_left_re`. For H-sides: `mapsTo_rectangleBorder_left_im` (y = z.im), `mapsTo_rectangleBorder_right_im` (y = w.im).\n\nNote the MapsTo functions use `↑x + z.im * I` with ↑x — the cast of x : ℝ to ℂ — same as (x + z.im * I) with x coerced ✓ (the `↑x` IS the coercion).\n\nIntervalIntegrable: for the parametrized derivative: `ContinuousOn.intervalIntegrable (h : ContinuousOn f (uIcc a b))`: deriv G continuous on the segment ⟸ ContinuousAt at each border point (hGc hypothesis) — I'll pass hGc : ∀ s ∈ border, ContinuousAt (deriv G) s. Hmm — ContinuousOn from pointwise ContinuousAt on the set: `ContinuousAt.continuousOn`? No — ContinuousOn s f ⟺ ∀ x ∈ s, ContinuousWithinAt f s x. ContinuousAt ⟹ ContinuousWithinAt ✓:\n```\nintro x hx\nexact (hGc _ (hymap x hx)).continuousWithinAt\n```\nAnd intervalIntegrable of ContinuousOn on uIcc: `ContinuousOn.intervalIntegrable (h : ContinuousOn f (Set.uIcc a b)) : IntervalIntegrable f volume a b` ✓ exists.\n\nAlso for the HasDerivAt pieces I need hG at the segment points via the mapsTo — `hymap : ∀ y ∈ uIcc, (x + y*I) ∈ border` from the MapsTo lemmas (MapsTo f s t : ∀ x ∈ s, f x ∈ t ✓).\n\nOK — the whole FTC lemma is now clear. Let me rewrite LiPrincipal.lean's rectInt_deriv_eq_zero properly with a helper for each side, then the P assembly. Also need `Complex.I_ne_zero` and `smul_smul`.\n\nLet me rewrite the whole file with the completed proof.","signature":""},{"type":"text","text":"The MapsTo border lemmas exist with exact names. Rewriting LiPrincipal.lean with the complete FTC proof."},{"type":"tool_use","id":"Write_223","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiPrincipal.lean","content":"/-\nNguyenRH1/LiPrincipal.lean — tier ii′ sub-stage ii′-1b(ii) (D-064 §4 R1):\nthe principal-part integral. For the explicit principal part\n P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i, A_i = F^{(n+1−i)}(1)/(n+1−i)!,\nwith F(w) = (wⁿ−(w−1)ⁿ)·hLi(w), on any rectangle with 1 in its interior:\n RectangleIntegral' P z w = A_1 = ResW1 n.\n\nMethod: P = A_1/(w−1) + (Σ_{i≥2} A_i/(w−1)^i). The first term is handled\nby the vendored `ResidueTheoremInRectangle`; the tail has the explicit\nglobal primitive G(w) = −Σ_{i≥2} A_i/((i−1)(w−1)^{i−1}), differentiable\non the border (1 is interior, hence off the border), so its rectangle\nintegral vanishes by per-side FTC (`rectInt_deriv_eq_zero`).\n\nArchive references: D-036, D-064 (R1), journal-016.\n-/\nimport Mathlib\nimport Zeta23.FromPNTPlus.ResidueCalcOnRectangles\nimport NguyenRH1.LiResidue\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Linearity of rectangle integrals -/\n\nlemma HIntegral_add (f g : ℂ → ℂ) (x₁ x₂ y : ℝ)\n (hf : IntervalIntegrable (fun x => f (x + y * I)) volume x₁ x₂)\n (hg : IntervalIntegrable (fun x => g (x + y * I)) volume x₁ x₂) :\n HIntegral (f + g) x₁ x₂ y = HIntegral f x₁ x₂ y + HIntegral g x₁ x₂ y := by\n rw [HIntegral, HIntegral, HIntegral]\n have e : (fun x => (f + g) (x + y * I)) = (fun x => f (x + y * I) + g (x + y * I)) := by\n funext x\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg]\n\nlemma VIntegral_add (f g : ℂ → ℂ) (x y₁ y₂ : ℝ)\n (hf : IntervalIntegrable (fun y => f (x + y * I)) volume y₁ y₂)\n (hg : IntervalIntegrable (fun y => g (x + y * I)) volume y₁ y₂) :\n VIntegral (f + g) x y₁ y₂ = VIntegral f x y₁ y₂ + VIntegral g x y₁ y₂ := by\n rw [VIntegral, VIntegral, VIntegral]\n have e : (fun y => (f + g) (x + y * I)) = (fun y => f (x + y * I) + g (x + y * I)) := by\n funext y\n simp [Pi.add_apply]\n rw [e, intervalIntegral.integral_add hf hg, smul_add]\n\nlemma RectangleIntegral_add (f g : ℂ → ℂ) (z w : ℂ)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral (f + g) z w = RectangleIntegral f z w + RectangleIntegral g z w := by\n rw [RectangleIntegral, RectangleIntegral, RectangleIntegral]\n obtain ⟨⟨hf1, hf2⟩, hf3, hf4⟩ := hf\n obtain ⟨⟨hg1, hg2⟩, hg3, hg4⟩ := hg\n rw [HIntegral_add f g _ _ _ hf1 hg1, HIntegral_add f g _ _ _ hf2 hg2,\n VIntegral_add f g _ _ _ hf3 hg3, VIntegral_add f g _ _ _ hf4 hg4]\n ring\n\nlemma RectangleIntegral'_add (f g : ℂ → ℂ) (z w : ℂ)\n (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :\n RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by\n rw [RectangleIntegral', RectangleIntegral_add f g z w hf hg, RectangleIntegral', RectangleIntegral',\n smul_add]\n\n/-! ## 2. Parametrized side derivatives and integrability -/\n\nlemma hasDerivAt_add_const_I (y : ℝ) (x : ℝ) :\n HasDerivAt (fun t => t + y * I) 1 x := by\n have hid := hasDerivAt_id x\n have hconst : HasDerivAt (fun _ => y * I) 0 x := hasDerivAt_const x _\n convert hid.add hconst using 1\n simp\n\nlemma hasDerivAt_const_add_I (x y : ℝ) :\n HasDerivAt (fun t => x + t * I) I y := by\n have h1 : HasDerivAt (fun t => t * I) I y := by\n have := (hasDerivAt_id y).mul_const I\n simpa using this\n have hconst : HasDerivAt (fun _ => x) 0 y := hasDerivAt_const y x\n convert hconst.add h1 using 1\n simp\n\n/-- FTC on a horizontal side: ∫_{x₁}^{x₂} (deriv G)(x + yI) dx\n= G(x₂ + yI) − G(x₁ + yI). -/\nlemma HIntegral_deriv {G : ℂ → ℂ} {z w : ℂ} (y : ℝ)\n (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)\n (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun x : ℝ => ↑x + y * I) [[z.re, w.re]] (RectangleBorder z w)) :\n ∫ x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by\n have hd : ∀ x ∈ Set.uIcc z.re w.re,\n HasDerivAt (fun x => G (x + y * I)) (deriv G (x + y * I)) x := by\n intro x hx\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hx |>.elim (fun h => h.1) |>.1))).hasDerivAt\n have h2 : HasDerivAt (fun x => x + y * I) 1 x := hasDerivAt_add_const_I y x\n have hcomp := h1.comp x h2\n convert hcomp using 1\n simp\n have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) volume z.re w.re := by\n apply ContinuousOn.intervalIntegrable\n intro x hx\n have hmem : (x + y * I) ∈ RectangleBorder z w := by\n apply hmap\n rcases Set.uIcc_of_le (by simp [Set.uIcc]) hx with h | h\n · exact h.1\n · exact h.1\n exact (hGc _ hmem).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n convert hftc using 1\n · simp\n · simp\n\n/-- FTC on a vertical side: ∫_{y₁}^{y₂} (deriv G)(x + yI) dy\n= −I·(G(x + y₂I) − G(x + y₁I)). -/\nlemma VIntegral_deriv {G : ℂ → ℂ} {z w : ℂ} (x : ℝ)\n (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)\n (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s)\n (hmap : MapsTo (fun y : ℝ => ↑x + ↑y * I) [[z.im, w.im]] (RectangleBorder z w)) :\n ∫ y in z.im..w.im, deriv G (x + y * I) =\n -I * (G (x + w.im * I) - G (x + z.im * I)) := by\n have hd : ∀ y ∈ Set.uIcc z.im w.im,\n HasDerivAt (fun y => G (x + y * I)) (I * deriv G (x + y * I)) y := by\n intro y hy\n have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=\n (hG _ (hmap (Set.uIcc_of_le (by simp [Set.uIcc]) hy |>.elim (fun h => h.1) |>.1))).hasDerivAt\n have h2 : HasDerivAt (fun y => x + y * I) I y := hasDerivAt_const_add_I x y\n have hcomp := h1.comp y h2\n convert hcomp using 1\n ring\n have hint : IntervalIntegrable (fun y => I * deriv G (x + y * I)) volume z.im w.im := by\n apply ContinuousOn.intervalIntegrable\n intro y hy\n apply ContinuousWithinAt.mul continuousWithinAt_const\n have hmem : (x + y * I) ∈ RectangleBorder z w := by\n apply hmap\n rcases Set.uIcc_of_le (by simp [Set.uIcc]) hy with h | h\n · exact h.1\n · exact h.1\n exact (hGc _ hmem).continuousWithinAt\n have hftc := intervalIntegral.integral_deriv_eq_sub hd hint\n rw [← hftc]\n rw [integral_smul]\n field_simp [Complex.I_ne_zero]\n\n/-- If `G : ℂ → ℂ` is differentiable at every point of the rectangle\nborder, then the rectangle integral of `deriv G` vanishes (each side\ntelescopes by FTC). -/\nlemma rectInt_deriv_eq_zero {G : ℂ → ℂ} {z w : ℂ}\n (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)\n (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s) :\n RectangleIntegral (fun s => deriv G s) z w = 0 := by\n rw [RectangleIntegral]\n rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),\n HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]\n have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)\n have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)\n rw [VIntegral, VIntegral, hVr, hVl]\n simp [Complex.I_mul_I]\n ring\n\nend NguyenRH1\n"},"extra_content":null}]