← Session 25 — ii′-5 R-bound: design + level-2 EM disc bound
thinking (12389 chars)
Now append §8 (Cf/g machinery): collProd, Cf characterizations, analyticity, nonvanishing, center log-norm, sphere bound, ball bound. Insert before `end NguyenRH1`.
For the sphere bound, statement:
```lean
theorem Cf_collZeros_norm_le_sphere {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
(hw : ‖w‖ = rC ht) :
‖Cf (rC ht) (scaledZeta t) w‖ ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht
```
And ball bound:
```lean
theorem Cf_collZeros_norm_le_ball {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
(hw : w ∈ Metric.closedBall 0 (rC ht)) :
‖Cf (rC ht) (scaledZeta t) w‖ ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht
```
via AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC) (R := (1+rC)/2).
For the max-modulus I need AnalyticOn ℂ B (closedBall 0 R) — from Cf_collZeros_analytic (AnalyticOnNhd on closedBall(0, R)) .analyticOn. Sphere membership: z ∈ Metric.sphere 0 (rC ht) ⟺ ‖z‖ = rC ht (mem_sphere_iff_norm, sub_zero). ✓
Then §9 in the next chunk: J_B + BC + main theorem.
Let me write §8 now. Careful details:
collProd:
```lean
/-- The product over the collected zeros, P(w) = ∏ (w−ρ)^{m_ρ}. -/
noncomputable def collProd {t : ℝ} (ht : 10 ≤ |t|) (w : ℂ) : ℂ :=
∏ ρ ∈ collZeros ht, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ
```
Cf char lemmas as drafted. Note: in Cf_eq_div_collProd, after `unfold Cf`, the goal: Cf's body with dite — need `classical` for the dite instance? The Cf def was ELABORATED with Classical open in Zeta23 — the instance is Classical.propDecidable baked into the term. simp only [hfin, ↓reduceDIte] — hfin : the proposition — simp only [h : p] rewrites p to True; ↓reduceDIte reduces dite True ... ✓ this is the Zeta23 pattern. I don't need `classical` in MY proof (the instance is in the term already). But to be safe add it.
Wait — one concern: `unfold Cf` — Cf is noncomputable def with the dite inside. unfold should work.
After simp only [hfin, ↓reduceDIte]: goal `Cf r_c F w = ...` — hmm unfold replaces `Cf (rC ht) (scaledZeta t) w` by its body — but Cf has (f) (r) (z) args — `unfold Cf` unfolds all Cf occurrences ✓. Then the body: `if finite_zeros_mono : (SetOfZeros (rC ht) (scaledZeta t)).Finite then (if w ∈ SetOfZeros (rC ht) (scaledZeta t) then ZeroFactor ... / ∏ ρ ∈ finite_zeros_mono.toFinset \ {w}, ... else scaledZeta t w / ∏ ρ ∈ finite_zeros_mono.toFinset, ...) else 1`. simp only [hfin, ↓reduceDIte] reduces the outer (hfin matches `finite_zeros_mono`'s TYPE — simp only [hfin] uses it as rewrite p → True; ↓reduceDIte then needs a Decidable (True)... the Zeta23 proofs did exactly this and it worked (with `open Classical` in scope — the instance for the reduced dite True: `Classical.propDecidable`...). Hmm — ↓reduceDIte is a simproc: dite c a b with c replaced by True and a decidable instance... it produces `a (of_decide_eq_true ...)`-ish. The Zeta23 pattern worked there; mirror it. Then the inner: `rw [dif_neg hw]` / `rw [dif_pos hw]` — dif_neg (h : ¬c) : (if h : c then a else b) = b — for dite: `dif_neg (hnc : ¬c) : (if h : c then a h else b h) = b hnc`?? the RHS is `b hnc`?? no — dif_neg : ¬c → dite c ta ea = ea (hnc)? Signature: `dif_neg (h : ¬c) {u : c → Sort _} {v : ¬c → Sort _}??` no. Standard: `dif_neg (h : ¬c) : (if h : c then a h else b h) = b h` ✓ (b takes the proof). OK.
Then the product finset: finite_zeros_mono.toFinset — with finite_zeros_mono the PROOF introduced by the dite — it's an arbitrary proof of (SetOfZeros r_c F).Finite. My hfin is MY proof — after simp only [hfin, ↓reduceDIte], the dite's branch value uses the dite-BOUND proof (finite_zeros_mono), NOT my hfin!! Hmm — when simp reduces dite c (λ h => val h) ..., the result is val (proof-of-c-from-True)... i.e. the term becomes `scaledZeta t w / ∏ ρ ∈ (hproof).toFinset, ...` where hproof is some proof of the finiteness (from of_decide or from hfin's rewrite?). When simp only [hfin] rewrites the PROPOSITION to True, then ↓reduceDIte gives `val (of_decide_eq_true (decide ...))`? or with eq_true hfin: dite True (λ h => ...) — the application needs a proof of True — the simproc supplies `of_decide_eq_true rfl` or trivial. Either way the resulting toFinset uses SOME proof — and collZeros_toFinset_eq works for ANY proof (toFinset_inj.mpr rfl) — so I rewrite with `collZeros_toFinset_eq ht ⟨the proof⟩` — but I can't name the simproc-generated proof! Hmm. Alternative: `Set.Finite.toFinset_congr`? or just convert the product via Finset.prod_congr after proving the finsets equal by ext:
```lean
have hfinset : ∀ (h1 h2 : (SetOfZeros (rC ht) (scaledZeta t)).Finite),
h1.toFinset = collZeros ht := fun h1 h2 => Set.Finite.toFinset_inj.mpr rfl
```
and then in the proof after simp/rw: `rw [hfinset _ _]`? Can't reference the anonymous proof term in rw...
Alternative approach: use `Set.Finite.toFinset_eq` hmm. OR: congruence: the goal after the dite reductions: `scaledZeta t w / ∏ ρ ∈ PF.toFinset, (w − ρ)^m = scaledZeta t w / collProd ht w` where PF is the anonymous proof. `congr 1` ⟹ `PF.toFinset = collZeros ht`?? congr on HDiv: f a b = f a' b' → a = a' ∧ b = b': congr 1 gives goals scaledZeta t w = scaledZeta t w (rfl-closed) and ∏ ... = collProd ht w — then unfold collProd: ∏ ρ ∈ PF.toFinset, F₁ ρ = ∏ ρ ∈ collZeros ht, F₁ ρ — congr 1 again on Finset.prod: PF.toFinset = collZeros ht ∧ (fun ρ => ...) = (fun ρ => ...) — the first: Set.Finite.toFinset_inj.mpr rfl — but congr needs to produce the subgoal: `Finset.prod_congr rfl (fun _ _ => rfl)`? Finset.prod_congr (h₁ : s₁ = s₂) (h₂ : ∀ x ∈ s₂, f x = g x) : s₁.prod f = s₂.prod g. So:
```lean
apply Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl)
intro ρ hρ
rfl
```
Hmm but the target is `∏ ρ ∈ PF.toFinset, ... = collProd ht w` — collProd is a def: apply Finset.prod_congr needs the RHS to be a prod application syntactically — `show _ = ∏ ρ ∈ collZeros ht, (w − ρ)^analyticOrderNatAt (scaledZeta t) ρ`? collProd ht w unfolds (delta) to that — `show` with defeq ✓. Or `unfold collProd` first. OK:
```lean
theorem Cf_eq_div_collProd {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
(hw : w ∉ SetOfZeros (rC ht) (scaledZeta t)) :
Cf (rC ht) (scaledZeta t) w = scaledZeta t w / collProd ht w := by
classical
have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=
scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by
obtain ⟨h1, h2⟩ := hx
exact ⟨h1.trans (rC_lt_one ht).le, h2⟩
unfold Cf collProd
simp only [hfin, ↓reduceDIte]
rw [dif_neg hw]
apply congrArg (fun X => scaledZeta t w / X)
exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)
```
Hmm — `apply congrArg (fun X => scaledZeta t w / X)`: goal becomes PF.toFinset.prod f = collZeros... wait goal after rw: `scaledZeta t w / ∏ ρ ∈ PF.toFinset, (w-ρ)^m = scaledZeta t w / ∏ ρ ∈ collZeros ht, (w-ρ)^m` (after unfold collProd — the RHS is the unfolded prod). congrArg (fun X => F w / X) : a = b → F w / a = F w / b — apply: goal matches F w / a = F w / b with a := ∏..., b := ∏... — new goal a = b ✓ (apply congrArg with the lambda — unification of F w / ?a = F w / ?b ✓). Then Finset.prod_congr (h₁ : PF.toFinset = collZeros ht) (h₂ : ∀ x ∈ collZeros ht, f x = f x): Finset.prod_congr : s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g ✓. toFinset_inj.mpr rfl : PF.toFinset = collZeros ht — toFinset_inj : hs.toFinset = ht.toFinset ↔ s = t: hs := PF (the anonymous), ht := subset-derived, s = SetOfZeros (rC ht) F = t ✓ rfl ✓. But — will `Set.Finite.toFinset_inj.mpr rfl` UNIFY hs with PF? The goal a = b with a = PF.toFinset: apply/exact toFinset_inj.mpr rfl: the lemma's hs, ht metavars unified by the goal ✓.
Hmm — but actually will `simp only [hfin, ↓reduceDIte]` maybe produce `hfin.toFinset`?? When simp rewrites the Prop `(SetOfZeros ...).Finite` to True using hfin, the dite's motive... The dite value branch: `λ finite_zeros_mono => ...` — after the condition becomes True, the simproc must supply a True proof, and the value becomes `... (proof-of-True).toFinset ...`. So PF is anonymous ✓ my approach handles it.
Actually — maybe simpler: avoid the issue entirely with `Set.Finite.toFinset_congr`?? Hmm — there's `Set.Finite.toFinset_eq_toFinset` (line 78: h.toFinset = s.toFinset for [Fintype s])... Let me also prepare a fallback: prove the two prod-terms equal via `Finset.prod_congr rfl`? If the finsets are DEFINITIONALLY equal (proof irrelevance!) — PF.toFinset vs subset-derived.toFinset — both are toFinset of proofs of the same set-finiteness — proof irrelevance makes PF ≡ subset-proof definitionally (Subsingleton of Prop) ⟹ the finsets are defeq ⟹ the prods are defeq ⟹ `rfl` might just close it! Finset.prod's first arg is the finset — defeq terms ⟹ rfl works. So maybe just `rfl` after the rw [dif_neg hw] + unfold. Try rfl first, fallback congrArg+prod_congr.
Hmm — toFinset OF a proof: `Set.Finite.toFinset (hs : s.Finite) : Finset α` — its definition uses hs.fintype... Classical choice stuff — proof irrelevance: hs ≡ hs' (Subsingleton) ⟹ toFinset hs ≡ toFinset hs' by congruence of defeq ✓ rfl should work.
For the pos branch similarly.
Also — `hw : w ∉ SetOfZeros (rC ht) (scaledZeta t)` vs the dite's condition `w ∈ SetOfZeros (rC ht) (scaledZeta t)`: dif_neg hw ✓ types match.
Now — one more important check: Cf's r argument is `rC ht` — Cf (rC ht) (scaledZeta t) w — unfold Cf gives body with r := rC ht ✓.
Now §8's remaining: analyticity (as drafted), nonvanishing (as drafted), center log-norm, sphere bound, ball bound.
For the center log-norm proof I need collProd at 0: ∏ (0−ρ)^m = ∏ (−ρ)^m; norm: ∏ ‖ρ‖^m. And ρ ≠ 0 for ρ ∈ collZeros (since F 0 = 1 ≠ 0 = F ρ... wait F ρ = 0 and F 0 = 1: if ρ = 0 then F ρ = F 0 = 1 ≠ 0 contradiction with F ρ = 0 — so ρ ≠ 0 ✓).
log‖B 0‖ ≥ 0: B 0 = F 0 / collProd 0 = 1/collProd 0. ‖B 0‖ = 1/‖collProd 0‖ = 1/∏‖ρ‖^m. log(1/x) = −log x; −log x ≥ 0 ⟺ log x ≤ 0 ⟸ 0 < x ≤ 1. x = ∏‖ρ‖^m ≤ 1: each factor ≤ 1 (‖ρ‖ ≤ rC − gapD ≤ rC ≤ 24/25 ≤ 1: pow_le_one₀ (norm_nonneg) (‖ρ‖ ≤ 1)) ✓; x > 0: each factor > 0 (‖ρ‖ > 0: ρ ≠ 0; pow_pos) ✓.
Real.log identities: goal 0 ≤ Real.log ‖B 0‖; ‖B 0‖ = 1/x: rw norm-div chain then Real.log_div? log(1/x) = log 1 − log x (Real.log_div (one_ne_zero) (x ≠ 0)) = −log x. 0 ≤ −log x ⟺ log x ≤ 0: Real.log_nonpos (0 ≤ x) (x ≤ 1) ✓.
Now write the whole §8 block. Also keep in mind `norm_prod` name: `norm_prod : ‖∏ i ∈ s, f i‖ = ∏ i ∈ s, ‖f i‖` ✓ (norm_prod in Mathlib.Analysis.Normed... exists).
Also Finset.prod_pos : (∀ i ∈ s, 0 < f i) → 0 < ∏ i ∈ s, f i ✓.
For the sphere bound: after establishing ‖B w‖ ≤ X/δ^M, done. Note δ^M with M : ℕ and δ : ℝ: gapD t ^ collMultSum ht ✓ nat pow.
One catch — collMultSum ht = Σ orders over collZeros; the product lower bound: ∏ ‖w−ρ‖^m ≥ ∏ δ^m = δ^(Σ m) — Finset.prod_pow_eq_pow_sum : ∏ i ∈ s, a ^ f i = a ^ (∑ i ∈ s, f i) ✓. So ∏ ‖w−ρ‖^m ≥ δ^(collMultSum ht): Finset.prod_le_prod (each ≥ 0: pow_nonneg (norm... δ ≥ 0)) (each δ^m ≤ ‖w−ρ‖^m: pow_le_pow_left₀ δ≥0 (δ ≤ ‖w−ρ‖) m) — prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : ∏ f ≤ ∏ g ✓ with f = fun ρ => δ^(order ρ), g = fun ρ => ‖w−ρ‖^(order ρ). Then = δ^(Σ order) = δ^(collMultSum ht) via Finset.prod_pow_eq_pow_sum + collMultSum def (unfold).
div bound assembly as planned.
Then ball bound:
```lean
theorem Cf_collZeros_norm_le_ball {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
(hw : w ∈ Metric.closedBall 0 (rC ht)) :
‖Cf (rC ht) (scaledZeta t) w‖ ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by
apply AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC ht) (R := (1 + rC ht) / 2)
· -- r ≤ R
have h1 := rC_lt_one ht
linarith [rC_pos ht]
· exact (Cf_collZeros_analytic ht).analyticOn
· intro z hz
rw [Metric.mem_sphere_iff_norm, sub_zero] at hz
exact Cf_collZeros_norm_le_sphere ht hz
· exact hw
```
Wait signature: AnalyticOn.norm_le_of_norm_le_on_sphere (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ Metric.closedBall 0 r) — with f, C, w implicit. `apply` with (r := rC ht) (R := ...) named — r, R are explicit-ish implicit? In the def: {C r R : ℝ} {f} {w} — all implicit. So provide via apply ... (r := rC ht) (R := (1+rC ht)/2) then 4 goals. ✓ mem_sphere_iff_norm : z ∈ Metric.sphere 0 r ↔ ‖z − 0‖ = r — rw [Metric.mem_sphere_iff_norm, sub_zero] at hz gives ‖z‖ = rC ht ✓.
AnalyticOnNhd.analyticOn — AnalyticOnNhd ℂ f s → AnalyticOn ℂ f s: `AnalyticOnNhd.analyticOn` ✓.
Write §8 now.
Now appending §8 (the Cf/g machinery) before `end NguyenRH1`.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
"old_string": "/-- The mult-weighted count over the collected zeros, as a natural. -/\nnoncomputable def collMultSum {t : \u211d} (ht : 10 \u2264 |t|) : \u2115 :=\n \u2211 \u03c1 \u2208 collZeros ht, analyticOrderNatAt (scaledZeta t) \u03c1\n\nend NguyenRH1",
"new_string": "/-- The mult-weighted count over the collected zeros, as a natural. -/\nnoncomputable def collMultSum {t : \u211d} (ht : 10 \u2264 |t|) : \u2115 :=\n \u2211 \u03c1 \u2208 collZeros ht, analyticOrderNatAt (scaledZeta t) \u03c1\n\n/-! ## 8. The Blaschke quotient g = Cf r_c F -/\n\n/-- The product over the collected zeros, P(w) = \u220f (w\u2212\u03c1)^{m_\u03c1}. -/\nnoncomputable def collProd {t : \u211d} (ht : 10 \u2264 |t|) (w : \u2102) : \u2102 :=\n \u220f \u03c1 \u2208 collZeros ht, (w - \u03c1) ^ analyticOrderNatAt (scaledZeta t) \u03c1\n\n/-- Off the collected zero set, the Blaschke quotient Cf is F/P. -/\ntheorem Cf_eq_div_collProd {t : \u211d} (ht : 10 \u2264 |t|) {w : \u2102}\n (hw : w \u2209 SetOfZeros (rC ht) (scaledZeta t)) :\n Cf (rC ht) (scaledZeta t) w = scaledZeta t w / collProd ht w := by\n classical\n have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=\n scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by\n obtain \u27e8h1, h2\u27e9 := hx\n exact \u27e8h1.trans (rC_lt_one ht).le, h2\u27e9\n unfold Cf collProd\n simp only [hfin, \u2193reduceDIte]\n rw [dif_neg hw]\n apply congrArg (fun X => scaledZeta t w / X)\n exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)\n\n/-- At a collected zero, Cf is the zero-factor cofactor over the remaining\nproduct. -/\ntheorem Cf_eq_zeroFactor_div {t : \u211d} (ht : 10 \u2264 |t|) {w : \u2102}\n (hw : w \u2208 SetOfZeros (rC ht) (scaledZeta t)) :\n Cf (rC ht) (scaledZeta t) w = ZeroFactor (scaledZeta t) w /\n \u220f \u03c1 \u2208 collZeros ht \\ {w}, (w - \u03c1) ^ analyticOrderNatAt (scaledZeta t) \u03c1 := by\n classical\n have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=\n scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by\n obtain \u27e8h1, h2\u27e9 := hx\n exact \u27e8h1.trans (rC_lt_one ht).le, h2\u27e9\n unfold Cf\n simp only [hfin, \u2193reduceDIte]\n rw [dif_pos hw]\n apply congrArg (fun X => ZeroFactor (scaledZeta t) w / X)\n exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)\n\n/-- g is analytic on a closed disc slightly larger than closedBall(0, r_c). -/\ntheorem Cf_collZeros_analytic {t : \u211d} (ht : 10 \u2264 |t|) :\n AnalyticOnNhd \u2102 (Cf (rC ht) (scaledZeta t))\n (Metric.closedBall 0 ((1 + rC ht) / 2)) := by\n apply CfAnalytic\n \u00b7 have h1 := rC_lt_one ht\n linarith [rC_pos ht]\n \u00b7 have h1 := rC_lt_one ht\n linarith\n \u00b7 exact scaledZeta_analytic ht\n \u00b7 rw [scaledZeta_zero]\n exact one_ne_zero\n\n/-- g is nonvanishing on closedBall(0, r_c). -/\ntheorem Cf_collZeros_ne_zero {t : \u211d} (ht : 10 \u2264 |t|) {w : \u2102}\n (hw : w \u2208 Metric.closedBall 0 (rC ht)) :\n Cf (rC ht) (scaledZeta t) w \u2260 0 := by\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n by_cases h0 : scaledZeta t w = 0\n \u00b7 have hwS : w \u2208 SetOfZeros (rC ht) (scaledZeta t) := \u27e8hw, h0\u27e9\n rw [Cf_eq_zeroFactor_div ht hwS]\n apply div_ne_zero\n \u00b7 obtain \u27e8h_w, h_w_an, h_w_ne, hZF, _\u27e9 := ZeroFactorization (rC_lt_one ht)\n (scaledZeta_analytic ht) (by rw [scaledZeta_zero]; exact one_ne_zero) hwS\n rw [hZF]\n exact h_w_ne\n \u00b7 apply Finset.prod_ne_zero_iff.mpr\n intro \u03c1 h\u03c1\n have h\u03c1ne : \u03c1 \u2260 w := fun h => (Finset.mem_sdiff.mp h\u03c1).2 (Finset.mem_singleton.mpr h)\n exact pow_ne_zero _ (sub_ne_zero.mpr h\u03c1ne.symm)\n \u00b7 have hwS : w \u2209 SetOfZeros (rC ht) (scaledZeta t) := fun h => h0 h.2\n rw [Cf_eq_div_collProd ht hwS]\n apply div_ne_zero h0\n unfold collProd\n apply Finset.prod_ne_zero_iff.mpr\n intro \u03c1 h\u03c1\n have h\u03c10 : scaledZeta t \u03c1 = 0 := ((mem_collZeros ht).mp h\u03c1).2\n exact pow_ne_zero _ (sub_ne_zero.mpr (fun h => h0 (by rw [h]; exact h\u03c10)))\n\n/-- At the center, log\u2016g(0)\u2016 \u2265 0 (since g(0) = 1/\u220f(\u2212\u03c1)^{m_\u03c1} and each\n\u2016\u03c1\u2016 \u2264 r_c < 1). -/\ntheorem Cf_collZeros_log_norm_zero_nonneg {t : \u211d} (ht : 10 \u2264 |t|) :\n 0 \u2264 Real.log \u2016Cf (rC ht) (scaledZeta t) 0\u2016 := by\n have h0S : (0:\u2102) \u2209 SetOfZeros (rC ht) (scaledZeta t) := by\n intro h\n have h2 := h.2\n rw [scaledZeta_zero] at h2\n exact one_ne_zero h2\n rw [Cf_eq_div_collProd ht h0S, scaledZeta_zero]\n have hprod_norm : \u2016collProd ht 0\u2016\n = \u220f \u03c1 \u2208 collZeros ht, \u2016\u03c1\u2016 ^ analyticOrderNatAt (scaledZeta t) \u03c1 := by\n unfold collProd\n rw [norm_prod]\n apply Finset.prod_congr rfl\n intro \u03c1 h\u03c1\n rw [zero_sub, norm_neg, norm_pow]\n have hfac : \u2200 \u03c1 \u2208 collZeros ht,\n 0 < \u2016\u03c1\u2016 ^ analyticOrderNatAt (scaledZeta t) \u03c1 := by\n intro \u03c1 h\u03c1\n have h\u03c10 : scaledZeta t \u03c1 = 0 := ((mem_collZeros ht).mp h\u03c1).2\n have hne : \u03c1 \u2260 0 := by\n intro h\n rw [h, scaledZeta_zero] at h\u03c10\n exact one_ne_zero h\u03c10\n exact pow_pos (norm_pos_iff.mpr hne) _\n have hprod_pos : 0 < \u220f \u03c1 \u2208 collZeros ht, \u2016\u03c1\u2016 ^ analyticOrderNatAt (scaledZeta t) \u03c1 :=\n Finset.prod_pos hfac\n have hprod_le : \u220f \u03c1 \u2208 collZeros ht, \u2016\u03c1\u2016 ^ analyticOrderNatAt (scaledZeta t) \u03c1 \u2264 1 := by\n apply Finset.prod_le_one (fun \u03c1 h\u03c1 => (hfac \u03c1 h\u03c1).le)\n intro \u03c1 h\u03c1\n have hnorm : \u2016\u03c1\u2016 \u2264 1 :=\n (((mem_collZeros ht).mp h\u03c1).1.trans (rC_le ht)).trans (by norm_num)\n exact pow_le_one\u2080 (norm_nonneg _) hnorm\n rw [hprod_norm, norm_div, norm_one,\n Real.log_div one_ne_zero (ne_of_gt hprod_pos), Real.log_one, zero_sub]\n exact neg_nonneg.mpr (Real.log_nonpos hprod_pos.le hprod_le)\n\n/-- **The outer-circle bound**: on the sphere \u2016w\u2016 = r_c (which carries no\nzeros, by the gap), \u2016g(w)\u2016 \u2264 (9/4)|t|\u00b2 \u00b7 gapD^{\u2212M_c}. -/\ntheorem Cf_collZeros_norm_le_sphere {t : \u211d} (ht : 10 \u2264 |t|) {w : \u2102}\n (hw : \u2016w\u2016 = rC ht) :\n \u2016Cf (rC ht) (scaledZeta t) w\u2016 \u2264\n (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by\n have h\u03b4 := gapD_pos t\n have hwS : w \u2209 SetOfZeros (rC ht) (scaledZeta t) := by\n intro hmem\n have hmemZ : w \u2208 collZeros ht := (mem_collZeros ht).mpr \u27e8hmem.1, hmem.2\u27e9\n have hle := collZeros_norm_le ht hmemZ\n rw [hw] at hle\n linarith\n rw [Cf_eq_div_collProd ht hwS, norm_div]\n have hF : \u2016scaledZeta t w\u2016 \u2264 (9 / 4) * |t| ^ 2 :=\n norm_scaledZeta_le ht (by rw [hw]; exact (rC_le ht).trans (by norm_num))\n -- the product is \u2265 gapD^{M_c}\n have hP : gapD t ^ collMultSum ht \u2264 \u2016collProd ht w\u2016 := by\n have hstep : \u220f \u03c1 \u2208 collZeros ht, gapD t ^ analyticOrderNatAt (scaledZeta t) \u03c1\n \u2264 \u220f \u03c1 \u2208 collZeros ht, \u2016w - \u03c1\u2016 ^ analyticOrderNatAt (scaledZeta t) \u03c1 := by\n apply Finset.prod_le_prod (fun \u03c1 _ => pow_nonneg h\u03b4.le _)\n intro \u03c1 h\u03c1\n have h\u03c1le := collZeros_norm_le ht h\u03c1\n have hd : gapD t \u2264 \u2016w - \u03c1\u2016 := by\n have h1 : \u2016w\u2016 - \u2016\u03c1\u2016 \u2264 \u2016w - \u03c1\u2016 := norm_sub_norm_le w \u03c1\n rw [hw] at h1\n linarith\n exact pow_le_pow_left\u2080 h\u03b4.le hd _\n rw [\u2190 Finset.prod_pow_eq_pow_sum] at hstep\n calc gapD t ^ collMultSum ht\n = gapD t ^ (\u2211 \u03c1 \u2208 collZeros ht, analyticOrderNatAt (scaledZeta t) \u03c1) := rfl\n _ \u2264 \u220f \u03c1 \u2208 collZeros ht, \u2016w - \u03c1\u2016 ^ analyticOrderNatAt (scaledZeta t) \u03c1 := hstep\n _ = \u2016collProd ht w\u2016 := by\n unfold collProd\n rw [norm_prod]\n apply Finset.prod_congr rfl\n intro \u03c1 h\u03c1\n rw [norm_pow]\n have hPpos : 0 < gapD t ^ collMultSum ht := pow_pos h\u03b4 _\n calc \u2016scaledZeta t w\u2016 / \u2016collProd ht w\u2016\n \u2264 (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht :=\n div_le_div hF hP hPpos (norm_nonneg _)\n\n/-- The bound propagates to the closed ball by the maximum principle. -/\ntheorem Cf_collZeros_norm_le_ball {t : \u211d} (ht : 10 \u2264 |t|) {w : \u2102}\n (hw : w \u2208 Metric.closedBall 0 (rC ht)) :\n \u2016Cf (rC ht) (scaledZeta t) w\u2016 \u2264\n (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by\n apply AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC ht) (R := (1 + rC ht) / 2)\n \u00b7 have h1 := rC_lt_one ht\n linarith [rC_pos ht]\n \u00b7 exact (Cf_collZeros_analytic ht).analyticOn\n \u00b7 intro z hz\n rw [Metric.mem_sphere_iff_norm, sub_zero] at hz\n exact Cf_collZeros_norm_le_sphere ht hz\n \u00b7 exact hw\n\nend NguyenRH1"
}
raw content_json (database row)
[{"type":"thinking","thinking":"Now append §8 (Cf/g machinery): collProd, Cf characterizations, analyticity, nonvanishing, center log-norm, sphere bound, ball bound. Insert before `end NguyenRH1`.\n\nFor the sphere bound, statement:\n```lean\ntheorem Cf_collZeros_norm_le_sphere {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : ‖w‖ = rC ht) :\n ‖Cf (rC ht) (scaledZeta t) w‖ ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht\n```\n\nAnd ball bound:\n```lean\ntheorem Cf_collZeros_norm_le_ball {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∈ Metric.closedBall 0 (rC ht)) :\n ‖Cf (rC ht) (scaledZeta t) w‖ ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht\n```\nvia AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC) (R := (1+rC)/2).\n\nFor the max-modulus I need AnalyticOn ℂ B (closedBall 0 R) — from Cf_collZeros_analytic (AnalyticOnNhd on closedBall(0, R)) .analyticOn. Sphere membership: z ∈ Metric.sphere 0 (rC ht) ⟺ ‖z‖ = rC ht (mem_sphere_iff_norm, sub_zero). ✓\n\nThen §9 in the next chunk: J_B + BC + main theorem.\n\nLet me write §8 now. Careful details:\n\ncollProd:\n```lean\n/-- The product over the collected zeros, P(w) = ∏ (w−ρ)^{m_ρ}. -/\nnoncomputable def collProd {t : ℝ} (ht : 10 ≤ |t|) (w : ℂ) : ℂ :=\n ∏ ρ ∈ collZeros ht, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ\n```\n\nCf char lemmas as drafted. Note: in Cf_eq_div_collProd, after `unfold Cf`, the goal: Cf's body with dite — need `classical` for the dite instance? The Cf def was ELABORATED with Classical open in Zeta23 — the instance is Classical.propDecidable baked into the term. simp only [hfin, ↓reduceDIte] — hfin : the proposition — simp only [h : p] rewrites p to True; ↓reduceDIte reduces dite True ... ✓ this is the Zeta23 pattern. I don't need `classical` in MY proof (the instance is in the term already). But to be safe add it.\n\nWait — one concern: `unfold Cf` — Cf is noncomputable def with the dite inside. unfold should work.\n\nAfter simp only [hfin, ↓reduceDIte]: goal `Cf r_c F w = ...` — hmm unfold replaces `Cf (rC ht) (scaledZeta t) w` by its body — but Cf has (f) (r) (z) args — `unfold Cf` unfolds all Cf occurrences ✓. Then the body: `if finite_zeros_mono : (SetOfZeros (rC ht) (scaledZeta t)).Finite then (if w ∈ SetOfZeros (rC ht) (scaledZeta t) then ZeroFactor ... / ∏ ρ ∈ finite_zeros_mono.toFinset \\ {w}, ... else scaledZeta t w / ∏ ρ ∈ finite_zeros_mono.toFinset, ...) else 1`. simp only [hfin, ↓reduceDIte] reduces the outer (hfin matches `finite_zeros_mono`'s TYPE — simp only [hfin] uses it as rewrite p → True; ↓reduceDIte then needs a Decidable (True)... the Zeta23 proofs did exactly this and it worked (with `open Classical` in scope — the instance for the reduced dite True: `Classical.propDecidable`...). Hmm — ↓reduceDIte is a simproc: dite c a b with c replaced by True and a decidable instance... it produces `a (of_decide_eq_true ...)`-ish. The Zeta23 pattern worked there; mirror it. Then the inner: `rw [dif_neg hw]` / `rw [dif_pos hw]` — dif_neg (h : ¬c) : (if h : c then a else b) = b — for dite: `dif_neg (hnc : ¬c) : (if h : c then a h else b h) = b hnc`?? the RHS is `b hnc`?? no — dif_neg : ¬c → dite c ta ea = ea (hnc)? Signature: `dif_neg (h : ¬c) {u : c → Sort _} {v : ¬c → Sort _}??` no. Standard: `dif_neg (h : ¬c) : (if h : c then a h else b h) = b h` ✓ (b takes the proof). OK.\n\nThen the product finset: finite_zeros_mono.toFinset — with finite_zeros_mono the PROOF introduced by the dite — it's an arbitrary proof of (SetOfZeros r_c F).Finite. My hfin is MY proof — after simp only [hfin, ↓reduceDIte], the dite's branch value uses the dite-BOUND proof (finite_zeros_mono), NOT my hfin!! Hmm — when simp reduces dite c (λ h => val h) ..., the result is val (proof-of-c-from-True)... i.e. the term becomes `scaledZeta t w / ∏ ρ ∈ (hproof).toFinset, ...` where hproof is some proof of the finiteness (from of_decide or from hfin's rewrite?). When simp only [hfin] rewrites the PROPOSITION to True, then ↓reduceDIte gives `val (of_decide_eq_true (decide ...))`? or with eq_true hfin: dite True (λ h => ...) — the application needs a proof of True — the simproc supplies `of_decide_eq_true rfl` or trivial. Either way the resulting toFinset uses SOME proof — and collZeros_toFinset_eq works for ANY proof (toFinset_inj.mpr rfl) — so I rewrite with `collZeros_toFinset_eq ht ⟨the proof⟩` — but I can't name the simproc-generated proof! Hmm. Alternative: `Set.Finite.toFinset_congr`? or just convert the product via Finset.prod_congr after proving the finsets equal by ext:\n\n```lean\n have hfinset : ∀ (h1 h2 : (SetOfZeros (rC ht) (scaledZeta t)).Finite),\n h1.toFinset = collZeros ht := fun h1 h2 => Set.Finite.toFinset_inj.mpr rfl\n```\nand then in the proof after simp/rw: `rw [hfinset _ _]`? Can't reference the anonymous proof term in rw... \n\nAlternative approach: use `Set.Finite.toFinset_eq` hmm. OR: congruence: the goal after the dite reductions: `scaledZeta t w / ∏ ρ ∈ PF.toFinset, (w − ρ)^m = scaledZeta t w / collProd ht w` where PF is the anonymous proof. `congr 1` ⟹ `PF.toFinset = collZeros ht`?? congr on HDiv: f a b = f a' b' → a = a' ∧ b = b': congr 1 gives goals scaledZeta t w = scaledZeta t w (rfl-closed) and ∏ ... = collProd ht w — then unfold collProd: ∏ ρ ∈ PF.toFinset, F₁ ρ = ∏ ρ ∈ collZeros ht, F₁ ρ — congr 1 again on Finset.prod: PF.toFinset = collZeros ht ∧ (fun ρ => ...) = (fun ρ => ...) — the first: Set.Finite.toFinset_inj.mpr rfl — but congr needs to produce the subgoal: `Finset.prod_congr rfl (fun _ _ => rfl)`? Finset.prod_congr (h₁ : s₁ = s₂) (h₂ : ∀ x ∈ s₂, f x = g x) : s₁.prod f = s₂.prod g. So:\n```lean\n apply Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl)\n intro ρ hρ\n rfl\n```\nHmm but the target is `∏ ρ ∈ PF.toFinset, ... = collProd ht w` — collProd is a def: apply Finset.prod_congr needs the RHS to be a prod application syntactically — `show _ = ∏ ρ ∈ collZeros ht, (w − ρ)^analyticOrderNatAt (scaledZeta t) ρ`? collProd ht w unfolds (delta) to that — `show` with defeq ✓. Or `unfold collProd` first. OK:\n\n```lean\ntheorem Cf_eq_div_collProd {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∉ SetOfZeros (rC ht) (scaledZeta t)) :\n Cf (rC ht) (scaledZeta t) w = scaledZeta t w / collProd ht w := by\n classical\n have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=\n scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by\n obtain ⟨h1, h2⟩ := hx\n exact ⟨h1.trans (rC_lt_one ht).le, h2⟩\n unfold Cf collProd\n simp only [hfin, ↓reduceDIte]\n rw [dif_neg hw]\n apply congrArg (fun X => scaledZeta t w / X)\n exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)\n```\nHmm — `apply congrArg (fun X => scaledZeta t w / X)`: goal becomes PF.toFinset.prod f = collZeros... wait goal after rw: `scaledZeta t w / ∏ ρ ∈ PF.toFinset, (w-ρ)^m = scaledZeta t w / ∏ ρ ∈ collZeros ht, (w-ρ)^m` (after unfold collProd — the RHS is the unfolded prod). congrArg (fun X => F w / X) : a = b → F w / a = F w / b — apply: goal matches F w / a = F w / b with a := ∏..., b := ∏... — new goal a = b ✓ (apply congrArg with the lambda — unification of F w / ?a = F w / ?b ✓). Then Finset.prod_congr (h₁ : PF.toFinset = collZeros ht) (h₂ : ∀ x ∈ collZeros ht, f x = f x): Finset.prod_congr : s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g ✓. toFinset_inj.mpr rfl : PF.toFinset = collZeros ht — toFinset_inj : hs.toFinset = ht.toFinset ↔ s = t: hs := PF (the anonymous), ht := subset-derived, s = SetOfZeros (rC ht) F = t ✓ rfl ✓. But — will `Set.Finite.toFinset_inj.mpr rfl` UNIFY hs with PF? The goal a = b with a = PF.toFinset: apply/exact toFinset_inj.mpr rfl: the lemma's hs, ht metavars unified by the goal ✓.\n\nHmm — but actually will `simp only [hfin, ↓reduceDIte]` maybe produce `hfin.toFinset`?? When simp rewrites the Prop `(SetOfZeros ...).Finite` to True using hfin, the dite's motive... The dite value branch: `λ finite_zeros_mono => ...` — after the condition becomes True, the simproc must supply a True proof, and the value becomes `... (proof-of-True).toFinset ...`. So PF is anonymous ✓ my approach handles it.\n\nActually — maybe simpler: avoid the issue entirely with `Set.Finite.toFinset_congr`?? Hmm — there's `Set.Finite.toFinset_eq_toFinset` (line 78: h.toFinset = s.toFinset for [Fintype s])... Let me also prepare a fallback: prove the two prod-terms equal via `Finset.prod_congr rfl`? If the finsets are DEFINITIONALLY equal (proof irrelevance!) — PF.toFinset vs subset-derived.toFinset — both are toFinset of proofs of the same set-finiteness — proof irrelevance makes PF ≡ subset-proof definitionally (Subsingleton of Prop) ⟹ the finsets are defeq ⟹ the prods are defeq ⟹ `rfl` might just close it! Finset.prod's first arg is the finset — defeq terms ⟹ rfl works. So maybe just `rfl` after the rw [dif_neg hw] + unfold. Try rfl first, fallback congrArg+prod_congr.\n\nHmm — toFinset OF a proof: `Set.Finite.toFinset (hs : s.Finite) : Finset α` — its definition uses hs.fintype... Classical choice stuff — proof irrelevance: hs ≡ hs' (Subsingleton) ⟹ toFinset hs ≡ toFinset hs' by congruence of defeq ✓ rfl should work.\n\nFor the pos branch similarly.\n\nAlso — `hw : w ∉ SetOfZeros (rC ht) (scaledZeta t)` vs the dite's condition `w ∈ SetOfZeros (rC ht) (scaledZeta t)`: dif_neg hw ✓ types match.\n\nNow — one more important check: Cf's r argument is `rC ht` — Cf (rC ht) (scaledZeta t) w — unfold Cf gives body with r := rC ht ✓.\n\nNow §8's remaining: analyticity (as drafted), nonvanishing (as drafted), center log-norm, sphere bound, ball bound.\n\nFor the center log-norm proof I need collProd at 0: ∏ (0−ρ)^m = ∏ (−ρ)^m; norm: ∏ ‖ρ‖^m. And ρ ≠ 0 for ρ ∈ collZeros (since F 0 = 1 ≠ 0 = F ρ... wait F ρ = 0 and F 0 = 1: if ρ = 0 then F ρ = F 0 = 1 ≠ 0 contradiction with F ρ = 0 — so ρ ≠ 0 ✓).\n\nlog‖B 0‖ ≥ 0: B 0 = F 0 / collProd 0 = 1/collProd 0. ‖B 0‖ = 1/‖collProd 0‖ = 1/∏‖ρ‖^m. log(1/x) = −log x; −log x ≥ 0 ⟺ log x ≤ 0 ⟸ 0 < x ≤ 1. x = ∏‖ρ‖^m ≤ 1: each factor ≤ 1 (‖ρ‖ ≤ rC − gapD ≤ rC ≤ 24/25 ≤ 1: pow_le_one₀ (norm_nonneg) (‖ρ‖ ≤ 1)) ✓; x > 0: each factor > 0 (‖ρ‖ > 0: ρ ≠ 0; pow_pos) ✓.\n\nReal.log identities: goal 0 ≤ Real.log ‖B 0‖; ‖B 0‖ = 1/x: rw norm-div chain then Real.log_div? log(1/x) = log 1 − log x (Real.log_div (one_ne_zero) (x ≠ 0)) = −log x. 0 ≤ −log x ⟺ log x ≤ 0: Real.log_nonpos (0 ≤ x) (x ≤ 1) ✓. \n\nNow write the whole §8 block. Also keep in mind `norm_prod` name: `norm_prod : ‖∏ i ∈ s, f i‖ = ∏ i ∈ s, ‖f i‖` ✓ (norm_prod in Mathlib.Analysis.Normed... exists).\n\nAlso Finset.prod_pos : (∀ i ∈ s, 0 < f i) → 0 < ∏ i ∈ s, f i ✓.\n\nFor the sphere bound: after establishing ‖B w‖ ≤ X/δ^M, done. Note δ^M with M : ℕ and δ : ℝ: gapD t ^ collMultSum ht ✓ nat pow.\n\nOne catch — collMultSum ht = Σ orders over collZeros; the product lower bound: ∏ ‖w−ρ‖^m ≥ ∏ δ^m = δ^(Σ m) — Finset.prod_pow_eq_pow_sum : ∏ i ∈ s, a ^ f i = a ^ (∑ i ∈ s, f i) ✓. So ∏ ‖w−ρ‖^m ≥ δ^(collMultSum ht): Finset.prod_le_prod (each ≥ 0: pow_nonneg (norm... δ ≥ 0)) (each δ^m ≤ ‖w−ρ‖^m: pow_le_pow_left₀ δ≥0 (δ ≤ ‖w−ρ‖) m) — prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) : ∏ f ≤ ∏ g ✓ with f = fun ρ => δ^(order ρ), g = fun ρ => ‖w−ρ‖^(order ρ). Then = δ^(Σ order) = δ^(collMultSum ht) via Finset.prod_pow_eq_pow_sum + collMultSum def (unfold).\n\ndiv bound assembly as planned.\n\nThen ball bound:\n```lean\ntheorem Cf_collZeros_norm_le_ball {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∈ Metric.closedBall 0 (rC ht)) :\n ‖Cf (rC ht) (scaledZeta t) w‖ ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by\n apply AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC ht) (R := (1 + rC ht) / 2)\n · -- r ≤ R\n have h1 := rC_lt_one ht\n linarith [rC_pos ht]\n · exact (Cf_collZeros_analytic ht).analyticOn\n · intro z hz\n rw [Metric.mem_sphere_iff_norm, sub_zero] at hz\n exact Cf_collZeros_norm_le_sphere ht hz\n · exact hw\n```\nWait signature: AnalyticOn.norm_le_of_norm_le_on_sphere (hyp_r : r ≤ R) (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R)) (cond : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ C) (wInS : w ∈ Metric.closedBall 0 r) — with f, C, w implicit. `apply` with (r := rC ht) (R := ...) named — r, R are explicit-ish implicit? In the def: {C r R : ℝ} {f} {w} — all implicit. So provide via apply ... (r := rC ht) (R := (1+rC ht)/2) then 4 goals. ✓ mem_sphere_iff_norm : z ∈ Metric.sphere 0 r ↔ ‖z − 0‖ = r — rw [Metric.mem_sphere_iff_norm, sub_zero] at hz gives ‖z‖ = rC ht ✓.\n\nAnalyticOnNhd.analyticOn — AnalyticOnNhd ℂ f s → AnalyticOn ℂ f s: `AnalyticOnNhd.analyticOn` ✓.\n\nWrite §8 now.","signature":""},{"type":"text","text":"Now appending §8 (the Cf/g machinery) before `end NguyenRH1`."},{"type":"tool_use","id":"Edit_50","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean","old_string":"/-- The mult-weighted count over the collected zeros, as a natural. -/\nnoncomputable def collMultSum {t : ℝ} (ht : 10 ≤ |t|) : ℕ :=\n ∑ ρ ∈ collZeros ht, analyticOrderNatAt (scaledZeta t) ρ\n\nend NguyenRH1","new_string":"/-- The mult-weighted count over the collected zeros, as a natural. -/\nnoncomputable def collMultSum {t : ℝ} (ht : 10 ≤ |t|) : ℕ :=\n ∑ ρ ∈ collZeros ht, analyticOrderNatAt (scaledZeta t) ρ\n\n/-! ## 8. The Blaschke quotient g = Cf r_c F -/\n\n/-- The product over the collected zeros, P(w) = ∏ (w−ρ)^{m_ρ}. -/\nnoncomputable def collProd {t : ℝ} (ht : 10 ≤ |t|) (w : ℂ) : ℂ :=\n ∏ ρ ∈ collZeros ht, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ\n\n/-- Off the collected zero set, the Blaschke quotient Cf is F/P. -/\ntheorem Cf_eq_div_collProd {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∉ SetOfZeros (rC ht) (scaledZeta t)) :\n Cf (rC ht) (scaledZeta t) w = scaledZeta t w / collProd ht w := by\n classical\n have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=\n scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by\n obtain ⟨h1, h2⟩ := hx\n exact ⟨h1.trans (rC_lt_one ht).le, h2⟩\n unfold Cf collProd\n simp only [hfin, ↓reduceDIte]\n rw [dif_neg hw]\n apply congrArg (fun X => scaledZeta t w / X)\n exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)\n\n/-- At a collected zero, Cf is the zero-factor cofactor over the remaining\nproduct. -/\ntheorem Cf_eq_zeroFactor_div {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∈ SetOfZeros (rC ht) (scaledZeta t)) :\n Cf (rC ht) (scaledZeta t) w = ZeroFactor (scaledZeta t) w /\n ∏ ρ ∈ collZeros ht \\ {w}, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ := by\n classical\n have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=\n scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by\n obtain ⟨h1, h2⟩ := hx\n exact ⟨h1.trans (rC_lt_one ht).le, h2⟩\n unfold Cf\n simp only [hfin, ↓reduceDIte]\n rw [dif_pos hw]\n apply congrArg (fun X => ZeroFactor (scaledZeta t) w / X)\n exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)\n\n/-- g is analytic on a closed disc slightly larger than closedBall(0, r_c). -/\ntheorem Cf_collZeros_analytic {t : ℝ} (ht : 10 ≤ |t|) :\n AnalyticOnNhd ℂ (Cf (rC ht) (scaledZeta t))\n (Metric.closedBall 0 ((1 + rC ht) / 2)) := by\n apply CfAnalytic\n · have h1 := rC_lt_one ht\n linarith [rC_pos ht]\n · have h1 := rC_lt_one ht\n linarith\n · exact scaledZeta_analytic ht\n · rw [scaledZeta_zero]\n exact one_ne_zero\n\n/-- g is nonvanishing on closedBall(0, r_c). -/\ntheorem Cf_collZeros_ne_zero {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∈ Metric.closedBall 0 (rC ht)) :\n Cf (rC ht) (scaledZeta t) w ≠ 0 := by\n rw [Metric.mem_closedBall, dist_zero_right] at hw\n by_cases h0 : scaledZeta t w = 0\n · have hwS : w ∈ SetOfZeros (rC ht) (scaledZeta t) := ⟨hw, h0⟩\n rw [Cf_eq_zeroFactor_div ht hwS]\n apply div_ne_zero\n · obtain ⟨h_w, h_w_an, h_w_ne, hZF, _⟩ := ZeroFactorization (rC_lt_one ht)\n (scaledZeta_analytic ht) (by rw [scaledZeta_zero]; exact one_ne_zero) hwS\n rw [hZF]\n exact h_w_ne\n · apply Finset.prod_ne_zero_iff.mpr\n intro ρ hρ\n have hρne : ρ ≠ w := fun h => (Finset.mem_sdiff.mp hρ).2 (Finset.mem_singleton.mpr h)\n exact pow_ne_zero _ (sub_ne_zero.mpr hρne.symm)\n · have hwS : w ∉ SetOfZeros (rC ht) (scaledZeta t) := fun h => h0 h.2\n rw [Cf_eq_div_collProd ht hwS]\n apply div_ne_zero h0\n unfold collProd\n apply Finset.prod_ne_zero_iff.mpr\n intro ρ hρ\n have hρ0 : scaledZeta t ρ = 0 := ((mem_collZeros ht).mp hρ).2\n exact pow_ne_zero _ (sub_ne_zero.mpr (fun h => h0 (by rw [h]; exact hρ0)))\n\n/-- At the center, log‖g(0)‖ ≥ 0 (since g(0) = 1/∏(−ρ)^{m_ρ} and each\n‖ρ‖ ≤ r_c < 1). -/\ntheorem Cf_collZeros_log_norm_zero_nonneg {t : ℝ} (ht : 10 ≤ |t|) :\n 0 ≤ Real.log ‖Cf (rC ht) (scaledZeta t) 0‖ := by\n have h0S : (0:ℂ) ∉ SetOfZeros (rC ht) (scaledZeta t) := by\n intro h\n have h2 := h.2\n rw [scaledZeta_zero] at h2\n exact one_ne_zero h2\n rw [Cf_eq_div_collProd ht h0S, scaledZeta_zero]\n have hprod_norm : ‖collProd ht 0‖\n = ∏ ρ ∈ collZeros ht, ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := by\n unfold collProd\n rw [norm_prod]\n apply Finset.prod_congr rfl\n intro ρ hρ\n rw [zero_sub, norm_neg, norm_pow]\n have hfac : ∀ ρ ∈ collZeros ht,\n 0 < ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := by\n intro ρ hρ\n have hρ0 : scaledZeta t ρ = 0 := ((mem_collZeros ht).mp hρ).2\n have hne : ρ ≠ 0 := by\n intro h\n rw [h, scaledZeta_zero] at hρ0\n exact one_ne_zero hρ0\n exact pow_pos (norm_pos_iff.mpr hne) _\n have hprod_pos : 0 < ∏ ρ ∈ collZeros ht, ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ :=\n Finset.prod_pos hfac\n have hprod_le : ∏ ρ ∈ collZeros ht, ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ ≤ 1 := by\n apply Finset.prod_le_one (fun ρ hρ => (hfac ρ hρ).le)\n intro ρ hρ\n have hnorm : ‖ρ‖ ≤ 1 :=\n (((mem_collZeros ht).mp hρ).1.trans (rC_le ht)).trans (by norm_num)\n exact pow_le_one₀ (norm_nonneg _) hnorm\n rw [hprod_norm, norm_div, norm_one,\n Real.log_div one_ne_zero (ne_of_gt hprod_pos), Real.log_one, zero_sub]\n exact neg_nonneg.mpr (Real.log_nonpos hprod_pos.le hprod_le)\n\n/-- **The outer-circle bound**: on the sphere ‖w‖ = r_c (which carries no\nzeros, by the gap), ‖g(w)‖ ≤ (9/4)|t|² · gapD^{−M_c}. -/\ntheorem Cf_collZeros_norm_le_sphere {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : ‖w‖ = rC ht) :\n ‖Cf (rC ht) (scaledZeta t) w‖ ≤\n (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by\n have hδ := gapD_pos t\n have hwS : w ∉ SetOfZeros (rC ht) (scaledZeta t) := by\n intro hmem\n have hmemZ : w ∈ collZeros ht := (mem_collZeros ht).mpr ⟨hmem.1, hmem.2⟩\n have hle := collZeros_norm_le ht hmemZ\n rw [hw] at hle\n linarith\n rw [Cf_eq_div_collProd ht hwS, norm_div]\n have hF : ‖scaledZeta t w‖ ≤ (9 / 4) * |t| ^ 2 :=\n norm_scaledZeta_le ht (by rw [hw]; exact (rC_le ht).trans (by norm_num))\n -- the product is ≥ gapD^{M_c}\n have hP : gapD t ^ collMultSum ht ≤ ‖collProd ht w‖ := by\n have hstep : ∏ ρ ∈ collZeros ht, gapD t ^ analyticOrderNatAt (scaledZeta t) ρ\n ≤ ∏ ρ ∈ collZeros ht, ‖w - ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := by\n apply Finset.prod_le_prod (fun ρ _ => pow_nonneg hδ.le _)\n intro ρ hρ\n have hρle := collZeros_norm_le ht hρ\n have hd : gapD t ≤ ‖w - ρ‖ := by\n have h1 : ‖w‖ - ‖ρ‖ ≤ ‖w - ρ‖ := norm_sub_norm_le w ρ\n rw [hw] at h1\n linarith\n exact pow_le_pow_left₀ hδ.le hd _\n rw [← Finset.prod_pow_eq_pow_sum] at hstep\n calc gapD t ^ collMultSum ht\n = gapD t ^ (∑ ρ ∈ collZeros ht, analyticOrderNatAt (scaledZeta t) ρ) := rfl\n _ ≤ ∏ ρ ∈ collZeros ht, ‖w - ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := hstep\n _ = ‖collProd ht w‖ := by\n unfold collProd\n rw [norm_prod]\n apply Finset.prod_congr rfl\n intro ρ hρ\n rw [norm_pow]\n have hPpos : 0 < gapD t ^ collMultSum ht := pow_pos hδ _\n calc ‖scaledZeta t w‖ / ‖collProd ht w‖\n ≤ (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht :=\n div_le_div hF hP hPpos (norm_nonneg _)\n\n/-- The bound propagates to the closed ball by the maximum principle. -/\ntheorem Cf_collZeros_norm_le_ball {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n (hw : w ∈ Metric.closedBall 0 (rC ht)) :\n ‖Cf (rC ht) (scaledZeta t) w‖ ≤\n (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by\n apply AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC ht) (R := (1 + rC ht) / 2)\n · have h1 := rC_lt_one ht\n linarith [rC_pos ht]\n · exact (Cf_collZeros_analytic ht).analyticOn\n · intro z hz\n rw [Metric.mem_sphere_iff_norm, sub_zero] at hz\n exact Cf_collZeros_norm_le_sphere ht hz\n · exact hw\n\nend NguyenRH1"},"extra_content":null}]