TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Self-normalized importance sampling ratio CLT and consistent Monte Carlo standard error

Statement

Let $(X, X, μ)$ , $\tilde{p}$ , $Z_{p}$ , $π$ , $q$ , $Q$ , $f$ , and $W_{i}$ satisfy the hypotheses and definitions of Self-normalized importance sampling is strongly consistent under finite first moments. Assume also $E_{Q} [W_{1}^{2}] < \infty, E_{Q} [(W_{1} f (X_{1}))^{2}] < \infty,$ and assume AC for the central limit conclusion. For every $n \geq 1$ , put $S_{n} = \sum_{i = 1}^{n} W_{i}$ and define the numerical extension ${\hat{θ}}_{S N, n} = \sum_{i = 1}^{n} W_{i} f (X_{i}) / S_{n}$ when $S_{n} > 0$ , and ${\hat{θ}}_{S N, n} = 0$ when $S_{n} = 0$ . This replaces the algorithm's no-estimate status by $0$ for all convergence statements below. Set $θ = \int f d π$ and $τ^{2} : = \frac{1}{Z_{p}^{2}} E_{Q} ⁣ [W_{1}^{2} (f (X_{1}) - θ)^{2}] .$ This is finite under the stated second moments. Then this numerical extension of the estimate in Self-normalized importance sampling satisfies $\sqrt{n} ({\hat{θ}}_{S N, n} - θ) \Rightarrow N (0, τ^{2}) .$ Define its plug-in variance estimate, when $S_{n} > 0$ , by ${\overset{}{Var}}_{M C} ({\hat{θ}}_{S N, n}) : = \frac{\sum_{i = 1}^{n} W_{i}^{2} (f (X_{i}) - {\hat{θ}}_{S N, n})^{2}}{S_{n}^{2}},$ and set this quantity to $0$ if $S_{n} = 0$ . Then, without using AC, $n {\overset{}{Var}}_{M C} ({\hat{θ}}_{S N, n}) ⟶ τ^{2} almost surely .$ Define ${\overset{}{se}}_{M C, n}$ to be the nonnegative square root of this plug-in variance. Then $\sqrt{n} {\overset{}{se}}_{M C, n} \to τ$ almost surely. No finite-sample unbiasedness assertion is made.

Facts & Assumptions

Given: The IID sampling and first-moment hypotheses of Self-normalized importance sampling is strongly consistent under finite first moments, the additional second moments, and AC for the CLT branch.

[F1]

Self-normalized importance sampling: The algorithm defines a measurable weight $w$ and, for $S_{n} > 0$ , returns ${\hat{θ}}_{S N, n} = \sum_{i} W_{i} f (X_{i}) / S_{n}$ ; when $S_{n} = 0$ , it returns the status no estimate: zero observed target weight.

[F2]

Change of variables for expectation: A nonnegative measurable function of an IID draw with law $Q$ has expectation given by integration against $Q$ , possibly with value $+ \infty$ ; the same identity holds as a finite integral for integrable functions.

[F3]

Multivariate iid central limit theorem: Under AC, IID $R^{d}$ -valued variables with finite second moment and covariance $Σ$ have sample-mean limit $\sqrt{n} ({\overset{ˉ}{X}}_{n} - m) \Rightarrow N_{d} (0, Σ)$ ; singular $Σ$ is allowed.

[F4]

First- and second-order delta method for random vectors: If $\sqrt{n} (T_{n} - η) \Rightarrow Z$ and $g (η + h) - g (η) = A h + o (∥ h ∥)$ , then $\sqrt{n} (g (T_{n}) - g (η)) \Rightarrow A Z$ .

[F5]

Self-normalized importance sampling is strongly consistent under finite first moments: Under its support and finite first-moment assumptions, the ratio estimate converges almost surely to $θ$ , and its denominator is eventually positive almost surely. For the convergence statement, that theorem interprets the algorithm's no-estimate status as the numeric value $0$ on any finite prefix with zero observed target weight.

[F6]

Kolmogorov iid l1 strong law: Every IID integrable real sequence has sample mean converging almost surely to its expectation.

[F7]

Measurable coordinatewise functions preserve independence: Applying one measurable function to each member of an independent family preserves independence.

[F8]

Identical distribution and IID families: A family is IID when it is mutually independent and has a common law.

[F9]

Moments, variance, and covariance on a probability space: Covariance is the expectation of the product of centered square-integrable variables, and variance is the self-covariance.

[F10]

Multivariate normal law, including singular covariance: Under AC, $Z \sim N_{d} (0, Σ)$ exactly when each linear projection $u \cdot Z$ is normal with variance $u^{T} Σ u$ ; singular covariance is allowed.

[F11]

Holder's inequality for random variables: For conjugate exponents $p = q = 2$ , square-integrable real random variables $R, S$ satisfy $E ∣ R S ∣ \leq (E ∣ R ∣^{2})^{1 / 2} (E ∣ S ∣^{2})^{1 / 2}$ , so $R S$ is integrable.

[F12]

Arithmetic and lattice operations preserve measurability whenever they are defined: Finite products and sums, and absolute values, of measurable real functions remain measurable.

[F13]

A nonnegative integral over a null set vanishes: A nonnegative measurable function has integral zero over a measurable null set.

[A1]

The Axiom of Choice: AC asserts that every family of nonempty sets has a choice function; the CLT branch inherits it through [F3] and [F10], while the strong-law standard-error branch is choice-free.

[F14]

Integrating against a density agrees with integrating the product: for a nonnegative measurable density $r$ and nonnegative measurable $h$ , $\int h d (r d μ) = \int h r d μ$ , including infinite values. Integrable real and complex functions, and their integrals: an absolutely integrable real function has integral equal to the finite difference of the integrals of its positive and negative parts.

Proof

Given: Let $Z_{i} = (W_{i}, W_{i} f (X_{i}))$ , ${\overset{ˉ}{W}}_{n} = n^{- 1} \sum_{i} W_{i}$ , and ${\overset{ˉ}{V}}_{n} = n^{- 1} \sum_{i} W_{i} f (X_{i})$ .

1.1A1F1F2F3F7F8F12F13givenF14

Use [F14] with density $r = q$ for integration against $Q$ and with $r = \tilde{p} / Z_{p}$ for integration against $π$ . By the support condition, $π ({q = 0}) = 0$ . For each $i$ , $X_{i}$ has law $Q$ , so the given finite first moment applies to $W_{i} ∣ f (X_{i}) ∣$ . The integrable case of [F2] gives $E_{Q} [W_{i} ∣ f (X_{i}) ∣] = \int_{{q > 0}} \frac{\tilde{p} (x) ∣ f (x) ∣}{q (x)} q (x) d μ (x) = \int_{{q > 0}} \tilde{p} ∣ f ∣ d μ < \infty .$ By [F13], $\int_{{q = 0}} ∣ f ∣ d π = 0$ , and hence $\int_{{q = 0}} \tilde{p} ∣ f ∣ d μ = Z_{p} \int_{{q = 0}} ∣ f ∣ d π = 0$ . Thus $\int_{X} \tilde{p} ∣ f ∣ d μ < \infty$ . For any real measurable $h$ whose absolute integral is finite against $r d μ$ , apply [F14] separately to $h^{+} = \max (h, 0)$ and $h^{-} = \max (- h, 0)$ : both product integrals are finite because $h^{\pm} \leq ∣ h ∣$ . Subtracting their finite identities yields $\int h d (r d μ) = \int h r d μ$ , since $(h r)^{\pm} = h^{\pm} r$ for $r \geq 0$ (with the density convention $0 \cdot \infty = 0$ ). The integrable case of [F2] applied to $W_{i} f (X_{i})$ yields $E_{Q} [W_{i} f (X_{i})] = \int_{{q > 0}} \tilde{p} f d μ = \int_{X} \tilde{p} f d μ = Z_{p} θ,$ because the omitted signed integral is zero by its absolute integrability on the $π$ -null set. The nonnegative case of [F2] also gives $E_{Q} W_{i} = \int_{{q > 0}} \tilde{p} d μ = Z_{p}$ , since $\int_{{q = 0}} \tilde{p} d μ = Z_{p} π ({q = 0}) = 0$ . The second-moment assumptions make $Z_{i}$ square-integrable. The map $x \mapsto (w (x), w (x) f (x))$ is measurable by [F1] and [F12]. Applying [F7] to this map proves that the pairs $Z_{i}$ are independent; their laws agree because each $X_{i}$ has law $Q$ and the same map is applied, so they are IID by [F8]. Therefore [F3] and [A1] give $\sqrt{n} (({\overset{ˉ}{W}}_{n}, {\overset{ˉ}{V}}_{n}) - (Z_{p}, Z_{p} θ)) \Rightarrow N_{2} (0, Σ)$ , where $Σ = {Cov}_{Q} (Z_{1})$ .

2.1F5F6F7F8F11F12givenstep 1.1algebra

Put $U_{i} = W_{i}^{2} (f (X_{i}) - θ)^{2}$ , $C_{i} = W_{i}^{2} (f (X_{i}) - θ)$ , and $B_{i} = W_{i}^{2}$ . Their measurability follows from [F12]. The stated second moments and $(W_{i} f (X_{i}) - θ W_{i})^{2} \leq 2 (W_{i} f (X_{i}))^{2} + 2 θ^{2} W_{i}^{2}$ give $E U_{i} < \infty$ and $E B_{i} < \infty$ ; [F11] gives $E ∣ C_{i} ∣ \leq (E U_{i})^{1 / 2} (E B_{i})^{1 / 2} < \infty$ . Each transformed sequence is IID by [F7] and [F8], so [F6] applies to all three. Also $(W_{i})$ is IID and integrable, with mean $Z_{p}$ by step 1.1; applying [F6] to this sequence gives ${\overset{ˉ}{W}}_{n} \to Z_{p} > 0$ almost surely. Separately, [F5] gives ${\hat{θ}}_{S N, n} \to θ$ almost surely.

2.2F1F4step 1.1givenalgebra

Define the Borel function $g (s, t) = t / s$ for $s > 0$ and $g (s, t) = 0$ for $s \leq 0$ ; it is Borel because the ratio is continuous on the open set $s > 0$ and the other branch is constant on its Borel complement. At $η = (Z_{p}, Z_{p} θ)$ , its derivative is $A (h_{1}, h_{2}) = (- θ h_{1} + h_{2}) / Z_{p}$ : for $h_{1}$ small enough that $Z_{p} + h_{1} > 0$ , $g (η + h) - g (η) - A h = - \frac{h_{1} (h_{2} - θ h_{1})}{Z_{p} (Z_{p} + h_{1})} = O (∥ h ∥^{2})$ . Since $Z_{p} > 0$ , this is a valid first-order expansion. Since ${\overset{ˉ}{W}}_{n} \geq 0$ , $g ({\overset{ˉ}{W}}_{n}, {\overset{ˉ}{V}}_{n})$ equals the ratio when $S_{n} > 0$ ; when $S_{n} = 0$ , it equals the numerical value $0$ prescribed by the Statement. Thus $g ({\overset{ˉ}{W}}_{n}, {\overset{ˉ}{V}}_{n}) = {\hat{θ}}_{S N, n}$ for every $n$ , including the zero-weight branch where [F1] returns a status. Apply [F4] to step 1.1 to obtain the scalar limit $A Z$ , where $Z \sim N_{2} (0, Σ)$ .

3.1F2F9F10step 1.1step 2.2algebra

By [F10], $A Z$ is centered normal with variance $A Σ A^{T}$ . The centered linear combination of $Z_{1}$ defining this variance is $Z_{p}^{- 1} (W_{1} f (X_{1}) - θ W_{1})$ , whose mean is zero by [F2]. Therefore $A Σ A^{T} = Z_{p}^{- 2} E_{Q} [W_{1}^{2} (f (X_{1}) - θ)^{2}] = τ^{2}$ , which proves the stated CLT.

4.1F5F6F7F8F11F12step 2.1givenalgebra∎

On the probability-one event from step 2.1 the denominator is eventually positive, and expansion of the squared residual gives $n {\overset{}{Var}}_{M C} = \frac{{\overset{ˉ}{U}}_{n} - 2 ({\hat{θ}}_{S N, n} - θ) {\overset{ˉ}{C}}_{n} + ({\hat{θ}}_{S N, n} - θ)^{2} {\overset{ˉ}{B}}_{n}}{{\overset{ˉ}{W}}_{n}^{2}}$ . The numerator tends to $E U_{1}$ and the denominator tends to $Z_{p}^{2}$ , so the limit is $Z_{p}^{- 2} E U_{1} = τ^{2}$ . Continuity of the nonnegative square-root map gives $\sqrt{n} {\overset{}{se}}_{M C, n} \to τ$ . This argument uses only the choice-free suppliers [F5], [F6], [F7], [F8], [F11], and [F12], not AC.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Thomas B. Schön and Fredrik Lindsten, Learning of dynamical systems: Particle filters and Markov chain methods, Chapter 4 §4.3.3, Theorem 1 (standard reference, not scraped)
Tuan Anh Le, Importance Sampling, §Asymptotic Variance (standard reference, not scraped)
Monte Carlo Methods course notes, Chapter 6 §6.2 (standard reference, not scraped)