Lemma 2, p. 9 — finite resolvent expansion with exact remainder

Proved

DouyinDQ.Bias.lemma_2

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

matrix-inversep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1resolvent-identity

Let $A,A'$ be real square matrices with both $I-A$ and $I-A'$ invertible. For every integer $K\ge0$ , the inverse of $I-A'$ is the sum of the first $K+1$ terms of its resolvent expansion around $A$ , plus an exact remainder:

(I-A')^{-1}=(I-A)^{-1}\sum_{k=0}^{K}[(A'-A)(I-A)^{-1}]^k+(I-A')^{-1}[(A'-A)(I-A)^{-1}]^{K+1}.

The identity supplies the finite-order expansion used in the paper's value-functional theorem.

Preamble

import Mathlib

Formal statement

namespace DouyinDQ.Bias

/-- Lemma 2, p. 9: finite resolvent expansion with its exact remainder. -/
theorem lemma_2 {ι : Type} [Fintype ι] [DecidableEq ι]
    (A A' : Matrix ι ι ℝ)
    (hA : IsUnit (1 - A).det) (hA' : IsUnit (1 - A').det) (K : ℕ) :
    (1 - A')⁻¹ = (1 - A)⁻¹ *
      (∑ k ∈ Finset.range (K + 1), ((A' - A) * (1 - A)⁻¹) ^ k) +
      (1 - A')⁻¹ * ((A' - A) * (1 - A)⁻¹) ^ (K + 1) := by sorry

end DouyinDQ.Bias

Source

Farias, Li, Peng, Ren, Zhang, Zheng, Correcting for Interference in Experiments: A Case Study at Douyin, arXiv:2305.02542v1, p. 9, Lemma 2

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph