← Session 28 — ii′-5e: partial-fraction identity (zero series + F entire)
thinking (689 chars)
Now also fix the digammaSeriesPartSub M-test lambdas (same (j : ℂ) coercion issue) — in §6's hu I wrote `(fun j => fun w : ℂ => (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))` — j unpinned: the if-condition j = n−1 forces j : ℕ ✓ (n : ℕ) — actually that pins j : ℕ already ✓. And the limit `digammaSeriesPartSub n` — same def-vs-lambda issue in the apply: `apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum` — the conclusion HasSumUniformlyOn f (fun x => ∑' n, f n x) s vs goal with digammaSeriesPartSub n — same unification failure. Fix identically: state hu with the tsum-lambda limit and convert at the end via hdiff2. Let me fix §6's hu/htend/hdiff/ending.
Now the same lambda/def treatment in §6's `digammaSeriesPartSub_analyticOn`.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean",
"old_string": " have hsum : Summable (fun j : \u2115 => (2 * (n : \u211d) + 1) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun j => fun w : \u2102 => (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (digammaSeriesPartSub n) (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum",
"new_string": " have hsum : Summable (fun j : \u2115 => (2 * (n : \u211d) + 1) / ((j : \u211d) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun (j : \u2115) => fun w : \u2102 =>\n (if j = n - 1 then 0 else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (fun w => \u2211' j : \u2115, (if j = n - 1 then (0 : \u2102)\n else (1 / ((j : \u2102) + 1) - 1 / (w + j + 1))))\n (Metric.ball (-(n : \u2102)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now also fix the digammaSeriesPartSub M-test lambdas (same (j : ℂ) coercion issue) — in §6's hu I wrote `(fun j => fun w : ℂ => (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))` — j unpinned: the if-condition j = n−1 forces j : ℕ ✓ (n : ℕ) — actually that pins j : ℕ already ✓. And the limit `digammaSeriesPartSub n` — same def-vs-lambda issue in the apply: `apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum` — the conclusion HasSumUniformlyOn f (fun x => ∑' n, f n x) s vs goal with digammaSeriesPartSub n — same unification failure. Fix identically: state hu with the tsum-lambda limit and convert at the end via hdiff2. Let me fix §6's hu/htend/hdiff/ending.","signature":""},{"type":"text","text":"Now the same lambda/def treatment in §6's `digammaSeriesPartSub_analyticOn`."},{"type":"tool_use","id":"Edit_156","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean","old_string":" have hsum : Summable (fun j : ℕ => (2 * (n : ℝ) + 1) / ((j : ℝ) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun j => fun w : ℂ => (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))\n (digammaSeriesPartSub n) (Metric.ball (-(n : ℂ)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum","new_string":" have hsum : Summable (fun j : ℕ => (2 * (n : ℝ) + 1) / ((j : ℝ) + 1) ^ 2) :=\n summable_div_add_one_sq _\n have hu : HasSumUniformlyOn\n (fun (j : ℕ) => fun w : ℂ =>\n (if j = n - 1 then 0 else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))\n (fun w => ∑' j : ℕ, (if j = n - 1 then (0 : ℂ)\n else (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))))\n (Metric.ball (-(n : ℂ)) (1 / 2)) := by\n apply HasSumUniformlyOn.of_norm_le_summable_eventually hsum"},"extra_content":null}]