Monte Carlo and importance sampling

DefinitionMonte Carlo estimate#✓fully proved

Given a function \(f : \alpha \to \mathbb{R}\) and samples \(X_0, X_1, \ldots : \Omega \to \alpha\), the Monte Carlo estimate from the first \(n\) samples at \(\omega \in \Omega\) is \(\frac{1}{n} \sum_{i < n} f(X_i(\omega))\), which is \(0\) when \(n = 0\).

noncomputable def mcEstimate (f : α → ℝ) (X : ℕ → Ω → α) (n : ℕ) (ω : Ω) : ℝ :=
  (n : ℝ)⁻¹ * ∑ i ∈ range n, f (X i ω)

Used by 3

Used byThe Monte Carlo estimator is unbiased · Importance-sampling estimate · The Monte Carlo estimator is consistent

TheoremThe Monte Carlo estimator is unbiased#✓fully proved

Let \(\mu\) be a measure on \(\Omega\), let \(\nu\) be a measure on \(\alpha\), and let \(f : \alpha \to \mathbb{R}\) be measurable and integrable with respect to \(\nu\). If \(X_0, X_1, \ldots : \Omega \to \alpha\) are measurable and the pushforward of \(\mu\) along each \(X_i\) is \(\nu\), then for every \(n \ne 0\) the integral with respect to \(\mu\) of the Monte Carlo estimate \(\frac{1}{n} \sum_{i < n} f(X_i)\) equals \(\int f \, d\nu\).

theorem integral_mcEstimate {ν : Measure α} {f : α → ℝ}
    (hf : Measurable f) (hfi : Integrable f ν) {X : ℕ → Ω → α} (hX : ∀ i, Measurable (X i))
    (hlaw : ∀ i, μ.map (X i) = ν) {n : ℕ} (hn : n ≠ 0) :
    ∫ ω, mcEstimate f X n ω ∂μ = ∫ x, f x ∂ν

Uses 1 · Used by 1

Statement usesMonte Carlo estimate

Used byImportance sampling is unbiased

TheoremThe Monte Carlo estimator is consistent#✓fully proved

The Monte Carlo estimator is consistent (strong law of large numbers). Let \(\mu\) be a measure on \(\Omega\), let \(\nu\) be a measure on \(\alpha\), and let \(f : \alpha \to \mathbb{R}\) be measurable and integrable with respect to \(\nu\). If \(X_0, X_1, \ldots : \Omega \to \alpha\) are measurable, pairwise independent under \(\mu\), and the pushforward of \(\mu\) along each \(X_i\) is \(\nu\), then for \(\mu\)-almost every \(\omega\) the Monte Carlo estimate \(\frac{1}{n} \sum_{i < n} f(X_i(\omega))\) converges to \(\int f \, d\nu\) as \(n \to \infty\).

theorem tendsto_mcEstimate {ν : Measure α} {f : α → ℝ}
    (hf : Measurable f) (hfi : Integrable f ν) {X : ℕ → Ω → α} (hX : ∀ i, Measurable (X i))
    (hlaw : ∀ i, μ.map (X i) = ν) (hindep : Pairwise fun i j ↦ IndepFun (X i) (X j) μ) :
    ∀ᵐ ω ∂μ, Tendsto (fun n ↦ mcEstimate f X n ω) atTop (𝓝 (∫ x, f x ∂ν))

Uses 1 · Used by 3

Statement usesMonte Carlo estimate

Used byParsimony is inconsistent in the Felsenstein zone · Strong law for the p-distances · Importance sampling is consistent

DefinitionImportance-sampling estimate#✓fully proved

Given a weight \(w : \alpha \to [0, \infty]\), a function \(f : \alpha \to \mathbb{R}\) and samples \(X_0, X_1, \ldots : \Omega \to \alpha\), the importance-sampling estimate from the first \(n\) samples at \(\omega \in \Omega\) is \(\frac{1}{n} \sum_{i < n} w(X_i(\omega)) \, f(X_i(\omega))\), where an infinite weight counts as \(0\) and the estimate is \(0\) when \(n = 0\). If the samples are drawn from a proposal measure \(\rho\), it estimates \(\int f \, d\nu\) for the target measure \(\nu\) with density \(w\) with respect to \(\rho\).

noncomputable def isEstimate (w : α → ℝ≥0∞) (f : α → ℝ) (X : ℕ → Ω → α) (n : ℕ) (ω : Ω) : ℝ :=
  mcEstimate (fun x ↦ (w x).toReal * f x) X n ω

Uses 1 · Used by 2

Statement usesMonte Carlo estimate

Used byImportance sampling is unbiased · Importance sampling is consistent

TheoremChange of measure for importance weights#✓fully proved

Let \(\rho\) be a measure on \(\alpha\), let \(w : \alpha \to [0, \infty]\) be measurable with \(w < \infty\) \(\rho\)-almost everywhere, and let \(\nu\) be the measure with density \(w\) with respect to \(\rho\). Then for every function \(f : \alpha \to \mathbb{R}\), \(\int w f \, d\rho = \int f \, d\nu\).

theorem integral_weight_mul {ρ : Measure α} {w : α → ℝ≥0∞} (hw : Measurable w)
    (hwt : ∀ᵐ x ∂ρ, w x < ∞) (f : α → ℝ) :
    ∫ x, (w x).toReal * f x ∂ρ = ∫ x, f x ∂(ρ.withDensity w)

Used by 2

Used byImportance sampling is unbiased · Importance sampling is consistent

TheoremImportance sampling is unbiased#✓fully proved

Let \(\mu\) be a measure on \(\Omega\), let \(\rho\) be a measure on \(\alpha\), let \(w : \alpha \to [0, \infty]\) be measurable with \(w < \infty\) \(\rho\)-almost everywhere, and let \(\nu\) be the measure with density \(w\) with respect to \(\rho\). Let \(f : \alpha \to \mathbb{R}\) be measurable and integrable with respect to \(\nu\). If \(X_0, X_1, \ldots : \Omega \to \alpha\) are measurable and the pushforward of \(\mu\) along each \(X_i\) is \(\rho\), then for every \(n \ne 0\) the integral with respect to \(\mu\) of the importance-sampling estimate of \(f\) with weight \(w\) from the first \(n\) samples equals \(\int f \, d\nu\).

theorem integral_isEstimate {ρ : Measure α} {w : α → ℝ≥0∞}
    (hw : Measurable w) (hwt : ∀ᵐ x ∂ρ, w x < ∞) {f : α → ℝ} (hf : Measurable f)
    (hfi : Integrable f (ρ.withDensity w)) {X : ℕ → Ω → α} (hX : ∀ i, Measurable (X i))
    (hlaw : ∀ i, μ.map (X i) = ρ) {n : ℕ} (hn : n ≠ 0) :
    ∫ ω, isEstimate w f X n ω ∂μ = ∫ x, f x ∂(ρ.withDensity w)

Uses 3

Statement usesImportance-sampling estimate

Proof usesThe Monte Carlo estimator is unbiased · Change of measure for importance weights

TheoremImportance sampling is consistent#✓fully proved

Let \(\mu\) be a measure on \(\Omega\), let \(\rho\) be a measure on \(\alpha\), let \(w : \alpha \to [0, \infty]\) be measurable with \(w < \infty\) \(\rho\)-almost everywhere, and let \(\nu\) be the measure with density \(w\) with respect to \(\rho\). Let \(f : \alpha \to \mathbb{R}\) be measurable and integrable with respect to \(\nu\). If \(X_0, X_1, \ldots : \Omega \to \alpha\) are measurable, pairwise independent under \(\mu\), and the pushforward of \(\mu\) along each \(X_i\) is \(\rho\), then for \(\mu\)-almost every \(\omega\) the importance-sampling estimate of \(f\) with weight \(w\) from the first \(n\) samples at \(\omega\) converges to \(\int f \, d\nu\) as \(n \to \infty\).

theorem tendsto_isEstimate {ρ : Measure α} {w : α → ℝ≥0∞}
    (hw : Measurable w) (hwt : ∀ᵐ x ∂ρ, w x < ∞) {f : α → ℝ} (hf : Measurable f)
    (hfi : Integrable f (ρ.withDensity w)) {X : ℕ → Ω → α} (hX : ∀ i, Measurable (X i))
    (hlaw : ∀ i, μ.map (X i) = ρ) (hindep : Pairwise fun i j ↦ IndepFun (X i) (X j) μ) :
    ∀ᵐ ω ∂μ, Tendsto (fun n ↦ isEstimate w f X n ω) atTop
      (𝓝 (∫ x, f x ∂(ρ.withDensity w)))

Uses 3

Statement usesImportance-sampling estimate

Proof usesChange of measure for importance weights · The Monte Carlo estimator is consistent

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.