Contiguity and Le Cam's lemmas

DefinitionContiguity of sequences of measures#✓fully proved

The sequence of measures Q n is contiguous with respect to P n (Q ◁ P): every sequence of measurable sets whose P n-measure tends to 0 has Q n-measure tending to 0.

def IsContiguous (Q P : ℕ → Measure Ω) : Prop :=
  ∀ A : ℕ → Set Ω, (∀ n, MeasurableSet (A n)) →
    Tendsto (fun n => P n (A n)) atTop (𝓝 0) → Tendsto (fun n => Q n (A n)) atTop (𝓝 0)

Sources

• van der Vaart (1998), Definition 6.3.

Used by 3

Used byLocal power of the likelihood-ratio test · Le Cam's first lemma · Contiguity transfers convergence in probability

TheoremExponential tilting of a centered Gaussian#✓fully proved

The law N(0, v) reweighted by the density exp(h x - h² v / 2) is N(h v, v). For v = 0 both sides are the Dirac mass at 0.

theorem gaussianReal_withDensity_exp (h : ℝ) (v : ℝ≥0) :
    (gaussianReal 0 v).withDensity
        (fun x => ENNReal.ofReal (Real.exp (h * x - h ^ 2 * v / 2))) =
      gaussianReal (h * v) v

Used by 2

Used byLe Cam's first lemma · Le Cam's third lemma

TheoremLe Cam's first lemma#✓fully proved

Le Cam's first lemma (LAN case). Let Qₙ = exp(Λₙ) · P be probability measures. If Sₙ → N(0, v) in distribution under P and Λₙ - h Sₙ → -h² v / 2 in P-probability, then Qₙ is contiguous with respect to P. This is the case of Le Cam's first lemma in which Λₙ → N(-σ²/2, σ²) under P, σ² = h² v; the general form (any limit L of dQₙ/dP with E L = 1) is not stated here.

theorem isContiguous_withDensity_exp {Λ S : ℕ → Ω → ℝ} {h : ℝ} {v : ℝ≥0}
    (hΛ : ∀ n, Measurable (Λ n))
    [∀ n, IsProbabilityMeasure (P.withDensity fun ω => ENNReal.ofReal (Real.exp (Λ n ω)))]
    (hS : TendstoInDistribution S atTop id (fun _ => P) (gaussianReal 0 v))
    (hLAN : TendstoInMeasure P (fun n ω => Λ n ω - h * S n ω) atTop
      (fun _ => -(h ^ 2 * v / 2))) :
    IsContiguous (fun n => P.withDensity fun ω => ENNReal.ofReal (Real.exp (Λ n ω)))
      (fun _ => P)

Sources

• Le Cam (1960); van der Vaart (1998), Lemma 6.4 and Example 6.5.

Uses 2 · Used by 1

Statement usesContiguity of sequences of measures

Proof usesExponential tilting of a centered Gaussian

Used byLocal power of the likelihood-ratio test

TheoremLe Cam's third lemma#✓fully proved

Le Cam's third lemma (LAN case). Let Qₙ = exp(Λₙ) · P be probability measures. If Sₙ → N(0, v) in distribution under P and Λₙ - h Sₙ → -h² v / 2 in P-probability, then Sₙ → N(h v, v) in distribution under Qₙ. This is the case of Le Cam's third lemma for the central sequence itself (covariance h v with Λₙ); the general form, for an arbitrary statistic jointly asymptotically normal with Λₙ, is not stated here.

theorem tendstoInDistribution_withDensity_exp {Λ S : ℕ → Ω → ℝ} {h : ℝ} {v : ℝ≥0}
    (hΛ : ∀ n, Measurable (Λ n))
    [∀ n, IsProbabilityMeasure (P.withDensity fun ω => ENNReal.ofReal (Real.exp (Λ n ω)))]
    (hS : TendstoInDistribution S atTop id (fun _ => P) (gaussianReal 0 v))
    (hLAN : TendstoInMeasure P (fun n ω => Λ n ω - h * S n ω) atTop
      (fun _ => -(h ^ 2 * v / 2))) :
    TendstoInDistribution S atTop id
      (fun n => P.withDensity fun ω => ENNReal.ofReal (Real.exp (Λ n ω)))
      (gaussianReal (h * v) v)

Sources

• Le Cam (1960); van der Vaart (1998), Theorem 6.6.

Uses 1 · Used by 1

Proof usesExponential tilting of a centered Gaussian

Used byLocal power of the likelihood-ratio test

TheoremContiguity transfers convergence in probability#✓fully proved

If Q ◁ P (a fixed P) and the measurable functions T n converge to c in P-probability, then Q n {ω | ε ≤ |T n ω - c|} → 0 for every ε > 0.

theorem IsContiguous.tendsto_measure_abs_sub_ge {Q : ℕ → Measure Ω}
    (hQP : IsContiguous Q (fun _ => P)) {T : ℕ → Ω → ℝ} (hT : ∀ n, Measurable (T n)) {c : ℝ}
    (h : TendstoInMeasure P T atTop (fun _ => c)) {ε : ℝ} (hε : 0 < ε) :
    Tendsto (fun n => Q n {ω | ε ≤ |T n ω - c|}) atTop (𝓝 0)

Sources

• van der Vaart (1998), ch. 6.

Uses 1 · Used by 1

Statement usesContiguity of sequences of measures

Used byLocal power of the likelihood-ratio test

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.