Prove2Me

Lemma 8 — lim⁡r→0+∫Cr(z0,θ1,θ2)f(z) dz=−i(θ2−θ1)c\lim_{r\to0^+}\int_{C_r(z_0,\theta_1,\theta_2)}f(z)\,dz=-i(\theta_2-\theta_1)c

Proved
InfoShareH2.lemma_8

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

hardy-spaceinformation-sharinginventoryp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chaintime-series

Let z0,c∈Cz_0,c\in\mathbb C, θ1≤θ2≤θ1+2π\theta_1\le\theta_2\le\theta_1+2\pi, and let Cr={z0+re−iλ:λ∈[θ1,θ2]}C_r=\{z_0+re^{-i\lambda}:\lambda\in[\theta_1,\theta_2]\}. Let f:C→Cf:\mathbb C\to\mathbb C satisfy: for every ε>0\varepsilon>0 there is δ>0\delta>0 such that ∣(z−z0)f(z)−c∣<ε|(z-z_0)f(z)-c|<\varepsilon for all 0<r<δ0<r<\delta and all z∈Crz\in C_r. Suppose the arc integrals ∫Crf(z) dz\int_{C_r}f(z)\,dz exist for small r>0r>0. Then

lim⁡r→0+∫Crf(z) dz=−i(θ2−θ1) c.\lim_{r\to0^+}\int_{C_r}f(z)\,dz=-i(\theta_2-\theta_1)\,c.

The arc is traversed through the parametrization z=z0+re−iλz=z_0+re^{-i\lambda}, λ\lambda from θ1\theta_1 to θ2\theta_2, so dz=−ire−iλdλdz=-ire^{-i\lambda}d\lambda.

The lemma evaluates the contribution of the boundary pole z=1z=1 in the contour arguments of Lemma 3 and Theorem 2.

Differences from the source:

  • reading: ∫_{C_r} f(z)dz (taken as existing) → for all small r > 0 the parametrized integrand is interval integrable on [θ₁, θ₂]; reason: the source writes the integrals as existing; in Lean a non-integrable integrand integrates to 0
  • encoding: contour integral over C_r(z₀, θ₁, θ₂) → ∫_{θ₁}^{θ₂} f(z₀ + re^{−iλ})·(−i r e^{−iλ}) dλ; reason: the parametrization of the proof
Preamble
import Mathlib
import Definitions.Def_InfoShareH2_Model

open Filter Topology MeasureTheory Complex

set_option autoImplicit false
Formal statement
namespace InfoShareH2

/-- **Lemma 8 (arc integral around a simple pole).**
SSRN 4319721 (v. 2024-01-20), Lemma 8, p.51. "Define
`C_r(z_0, θ_1, θ_2) = {z_0 + re^{−iλ} : λ ∈ [θ_1, θ_2]}` where `0 ≤ θ_2 − θ_1 ≤ 2π`. Let `f(z)` be a
function such that for any `ε > 0`, there exists some `δ > 0` such that for all `0 < r < δ`,
`|(z − z_0)f(z) − c| < ε` for all `z ∈ C_r(z_0, θ_1, θ_2)`. Then
`lim_{r→0+} ∫_{C_r(z_0,θ_1,θ_2)} f(z)dz = −i(θ_2 − θ_1)c`."

**Formalization Note** The arc integral is written through the parametrization of the proof,
`z = z_0 + re^{−iλ}`, `dz = −i r e^{−iλ} dλ`. The source takes the arc integrals as existing; the
hypothesis `hint` says so for all small `r` (otherwise Lean's integral of a non-integrable function
is `0`). -/
theorem lemma_8 (f : ℂ → ℂ) (z0 c : ℂ) (θ1 θ2 : ℝ) (h12 : 0 ≤ θ2 - θ1)
    (h12' : θ2 - θ1 ≤ 2 * Real.pi)
    (hf : ∀ e > (0 : ℝ), ∃ δ > (0 : ℝ), ∀ r : ℝ, 0 < r → r < δ → ∀ lam ∈ Set.Icc θ1 θ2,
      ‖((z0 + (r : ℂ) * exp (-(lam : ℂ) * I)) - z0) * f (z0 + (r : ℂ) * exp (-(lam : ℂ) * I)) - c‖ < e)
    (hint : ∀ᶠ r : ℝ in 𝓝[>] (0 : ℝ), IntervalIntegrable
      (fun lam : ℝ => f (z0 + (r : ℂ) * exp (-(lam : ℂ) * I)) * (-I * (r : ℂ) * exp (-(lam : ℂ) * I)))
      volume θ1 θ2) :
    Tendsto (fun r : ℝ => ∫ lam in θ1..θ2,
        f (z0 + (r : ℂ) * exp (-(lam : ℂ) * I)) * (-I * (r : ℂ) * exp (-(lam : ℂ) * I)))
      (𝓝[>] (0 : ℝ)) (𝓝 (-I * ((θ2 - θ1 : ℝ) : ℂ) * c)) := by sorry

end InfoShareH2
Source
Caldentey–Giloni–Hurvich–Zhang, Information Design and Sharing in Supply Chains, SSRN 4319721 (v. 2024-01-20), https://ssrn.com/abstract=4319721, Lemma 8, p.51
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph