Large deviation principle

StructureRate function#✓fully proved

Let \(X\) be a topological space. A rate function on \(X\) is a lower semicontinuous function \(I : X \to [0, \infty]\).

This is the basic regularity hypothesis used in the formulation of a large deviation principle.

structure IsRateFunction {X : Type*} [TopologicalSpace X] (I : X → ℝ≥0∞) : Prop where
  lowerSemicontinuous : LowerSemicontinuous I

Used by 9

Used byCramér rate function is a convex rate function · Convex rate function · Good rate function · The absolute value is a good rate function · Good rate functions are rate functions · Convex rate functions are rate functions · Large deviation principle for a sequence of measures · Large deviation principle for a Dirac mass · Large deviation principle from bounds on measurable sets

StructureGood rate function#✓fully proved

Let \(X\) be a topological space. A function \(I : X \to [0, \infty]\) is a good rate function if it is a rate function and, for every real number \(a \ge 0\), the sub-level set \(\{x \in X : I(x) \le a\}\) is compact.

Compactness is required only at finite levels: the sub-level set at level \(\infty\) is all of \(X\), so requiring it as well would force \(X\) itself to be compact.

structure IsGoodRateFunction {X : Type*} [TopologicalSpace X] (I : X → ℝ≥0∞) : Prop
    extends IsRateFunction I where
  isCompact_levelSet : ∀ a : ℝ, IsCompact {x | I x ≤ ENNReal.ofReal a}

Uses 1 · Used by 2

Statement usesRate function

Used byThe absolute value is a good rate function · Good rate functions are rate functions

StructureConvex rate function#✓fully proved

Let \(X\) be a real vector space carrying a topology (no compatibility between the topology and the linear structure is assumed). A function \(I : X \to [0, \infty]\) is a convex rate function if it is a rate function and \(I(ax + by) \le a I(x) + b I(y)\) for all \(x, y \in X\) and all real numbers \(a, b \ge 0\) with \(a + b = 1\).

structure IsConvexRateFunction {X : Type*} [TopologicalSpace X] [AddCommMonoid X]
    [Module ℝ X] (I : X → ℝ≥0∞) : Prop extends IsRateFunction I where
  convex : ∀ ⦃x y : X⦄, ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
    I (a • x + b • y) ≤ ENNReal.ofReal a * I x + ENNReal.ofReal b * I y

Uses 1 · Used by 2

Statement usesRate function

Used byCramér rate function is a convex rate function · Convex rate functions are rate functions

StructureLarge deviation principle for a sequence of measures#✓fully proved

Let \(X\) be a topological space with a \(\sigma\)-algebra containing every open set, let \((\mu_n)_{n \in \mathbb{N}}\) be a sequence of measures on \(X\), and let \(I : X \to [0, \infty]\). The sequence \((\mu_n)\) satisfies the large deviation principle with rate function \(I\) and speed \(n\) if \(I\) is a rate function, every open set \(U \subseteq X\) satisfies

\[\liminf_{n \to \infty} \frac{1}{n} \log \mu_n(U) \ge -\inf_{x \in U} I(x),\]

and every closed set \(F \subseteq X\) satisfies

\[\limsup_{n \to \infty} \frac{1}{n} \log \mu_n(F) \le -\inf_{x \in F} I(x).\]

Here \(\log 0 = -\infty\), an infimum over the empty set is \(\infty\), and the limits are taken in the extended reals.

structure SatisfiesLDP {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
    [OpensMeasurableSpace X] (μ : ℕ → Measure X) (I : X → ℝ≥0∞) : Prop where
  isRateFunction : IsRateFunction I
  lower_bound : ∀ U : Set X, IsOpen U →
    - (⨅ x ∈ U, (I x : EReal)) ≤
      liminf (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n U)) atTop
  upper_bound : ∀ F : Set X, IsClosed F →
    limsup (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n F)) atTop ≤
      - (⨅ x ∈ F, (I x : EReal))

Uses 1 · Used by 5

Statement usesRate function

Used byLarge deviation bounds for arbitrary sets · Large deviation lower bound for arbitrary sets · Large deviation upper bound for arbitrary sets · Large deviation principle for a Dirac mass · Large deviation principle from bounds on measurable sets

TheoremGood rate functions are rate functions#✓fully proved

Every good rate function on a topological space is a rate function.

theorem IsGoodRateFunction.isRateFunction {X : Type*} [TopologicalSpace X]
    {I : X → ℝ≥0∞} (h : IsGoodRateFunction I) : IsRateFunction I

Uses 2

Statement usesGood rate function · Rate function

TheoremConvex rate functions are rate functions#✓fully proved

Every convex rate function on a real vector space with a topology is a rate function.

theorem IsConvexRateFunction.isRateFunction {X : Type*} [TopologicalSpace X]
    [AddCommMonoid X] [Module ℝ X] {I : X → ℝ≥0∞} (h : IsConvexRateFunction I) :
    IsRateFunction I

Uses 2

Statement usesConvex rate function · Rate function

TheoremLarge deviation lower bound for arbitrary sets#✓fully proved

Let \(X\) be a topological space with a \(\sigma\)-algebra in which every open set is measurable, and let \((\mu_n)_{n \in \mathbb{N}}\) be measures on \(X\) satisfying the large deviation principle with rate function \(I : X \to [0, \infty]\). Then for every set \(\Gamma \subseteq X\), not necessarily measurable (for non-measurable \(\Gamma\), \(\mu_n(\Gamma)\) is its outer measure), with interior \(\Gamma^\circ\),

\[-\inf_{x \in \Gamma^\circ} I(x) \le \liminf_{n \to \infty} \frac{1}{n} \log \mu_n(\Gamma),\]

computed in the extended reals with \(\log 0 = -\infty\).

theorem SatisfiesLDP.borel_lower_bound [OpensMeasurableSpace X]
    {μ : ℕ → Measure X} {I : X → ℝ≥0∞}
    (h : SatisfiesLDP μ I) (Γ : Set X) :
    - (⨅ x ∈ interior Γ, (I x : EReal)) ≤
      liminf (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n Γ)) atTop

Uses 1 · Used by 1

Statement usesLarge deviation principle for a sequence of measures

Used byLarge deviation bounds for arbitrary sets

TheoremLarge deviation upper bound for arbitrary sets#✓fully proved

Let \(X\) be a topological space with a \(\sigma\)-algebra in which every open set is measurable, and let \((\mu_n)_{n \in \mathbb{N}}\) be measures on \(X\) satisfying the large deviation principle with rate function \(I : X \to [0, \infty]\). Then for every set \(\Gamma \subseteq X\), not necessarily measurable (for non-measurable \(\Gamma\), \(\mu_n(\Gamma)\) is its outer measure), with closure \(\overline{\Gamma}\),

\[\limsup_{n \to \infty} \frac{1}{n} \log \mu_n(\Gamma) \le -\inf_{x \in \overline{\Gamma}} I(x),\]

computed in the extended reals with \(\log 0 = -\infty\).

theorem SatisfiesLDP.borel_upper_bound [OpensMeasurableSpace X]
    {μ : ℕ → Measure X} {I : X → ℝ≥0∞}
    (h : SatisfiesLDP μ I) (Γ : Set X) :
    limsup (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n Γ)) atTop ≤
      - (⨅ x ∈ closure Γ, (I x : EReal))

Uses 1 · Used by 1

Statement usesLarge deviation principle for a sequence of measures

Used byLarge deviation bounds for arbitrary sets

TheoremLarge deviation bounds for arbitrary sets#✓fully proved

Let \(X\) be a topological space with a \(\sigma\)-algebra in which every open set is measurable, and let \((\mu_n)_{n \in \mathbb{N}}\) be measures on \(X\) satisfying the large deviation principle with rate function \(I : X \to [0, \infty]\). Then for every set \(\Gamma \subseteq X\), not necessarily measurable (for non-measurable \(\Gamma\), \(\mu_n(\Gamma)\) is its outer measure), with interior \(\Gamma^\circ\) and closure \(\overline{\Gamma}\), both

\[-\inf_{x \in \Gamma^\circ} I(x) \le \liminf_{n \to \infty} \frac{1}{n} \log \mu_n(\Gamma)\]

and

\[\limsup_{n \to \infty} \frac{1}{n} \log \mu_n(\Gamma) \le -\inf_{x \in \overline{\Gamma}} I(x)\]

hold, computed in the extended reals with \(\log 0 = -\infty\). In particular the bounds hold for every Borel set \(\Gamma\).

theorem SatisfiesLDP.borel_bounds [OpensMeasurableSpace X]
    {μ : ℕ → Measure X} {I : X → ℝ≥0∞}
    (h : SatisfiesLDP μ I) (Γ : Set X) :
    - (⨅ x ∈ interior Γ, (I x : EReal)) ≤
        liminf (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n Γ)) atTop ∧
      limsup (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n Γ)) atTop ≤
        - (⨅ x ∈ closure Γ, (I x : EReal))

Uses 3

Statement usesLarge deviation principle for a sequence of measures

Proof usesLarge deviation lower bound for arbitrary sets · Large deviation upper bound for arbitrary sets

TheoremLarge deviation principle from bounds on measurable sets#✓fully proved

Let \(X\) be a topological space with a \(\sigma\)-algebra containing every open set, let \((\mu_n)_{n \in \mathbb{N}}\) be a sequence of measures on \(X\), and let \(I\) be a rate function on \(X\). Suppose that every measurable set \(\Gamma \subseteq X\), with interior \(\Gamma^\circ\) and closure \(\overline{\Gamma}\), satisfies

\[\liminf_{n \to \infty} \frac{1}{n} \log \mu_n(\Gamma) \ge -\inf_{x \in \Gamma^\circ} I(x)\]

and

\[\limsup_{n \to \infty} \frac{1}{n} \log \mu_n(\Gamma) \le -\inf_{x \in \overline{\Gamma}} I(x),\]

where \(\log 0 = -\infty\), an infimum over the empty set is \(\infty\), and the limits are taken in the extended reals. Then \((\mu_n)\) satisfies the large deviation principle with rate function \(I\).

Open and closed sets are measurable and equal to their interior and closure respectively, so the hypothesis contains the open-set and closed-set bounds. On a Borel space this is the textbook Borel-set converse.

theorem satisfiesLDP_of_borel_bounds [OpensMeasurableSpace X]
    {μ : ℕ → Measure X} {I : X → ℝ≥0∞}
    (hRate : IsRateFunction I)
    (h : ∀ Γ : Set X, MeasurableSet Γ →
      - (⨅ x ∈ interior Γ, (I x : EReal)) ≤
          liminf (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n Γ)) atTop ∧
        limsup (fun n => ((n : ℕ) : EReal)⁻¹ * ENNReal.log (μ n Γ)) atTop ≤
          - (⨅ x ∈ closure Γ, (I x : EReal))) :
    SatisfiesLDP μ I

Uses 2

Statement usesRate function · Large deviation principle for a sequence of measures

DefinitionRate function of a Dirac mass#✓fully proved

For a point \(x_0\) of a set \(X\), the Dirac rate function at \(x_0\) is the function \(X \to [0, \infty]\) that equals \(0\) at \(x_0\) and \(\infty\) at every other point.

noncomputable def diracRate (x₀ : X) : X → ℝ≥0∞ :=
  Set.indicator {x₀}ᶜ (fun _ => (⊤ : ℝ≥0∞))

Used by 5

Used byThe Dirac rate function is infinite away from its center · The Dirac rate function vanishes at its center · Infimum of the Dirac rate function over a set containing the center · Infimum of the Dirac rate function over a set avoiding the center · Large deviation principle for a Dirac mass

LemmaThe Dirac rate function vanishes at its center#✓fully proved

For every point \(x_0\) of a set \(X\), the Dirac rate function at \(x_0\) takes the value \(0\) at \(x_0\).

lemma diracRate_apply_self (x₀ : X) : diracRate x₀ x₀ = 0

Uses 1 · Used by 2

Statement usesRate function of a Dirac mass

Used byInfimum of the Dirac rate function over a set containing the center · Large deviation principle for a Dirac mass

LemmaThe Dirac rate function is infinite away from its center#✓fully proved

For points \(x \ne x_0\) of a set \(X\), the Dirac rate function at \(x_0\) takes the value \(\infty\) at \(x\).

lemma diracRate_apply_of_ne {x₀ x : X} (h : x ≠ x₀) : diracRate x₀ x = ⊤

Uses 1 · Used by 2

Statement usesRate function of a Dirac mass

Used byInfimum of the Dirac rate function over a set avoiding the center · Large deviation principle for a Dirac mass

LemmaInfimum of the Dirac rate function over a set containing the center#✓fully proved

For a point \(x_0\) of a set \(X\) and a subset \(s \subseteq X\) with \(x_0 \in s\), the infimum over \(x \in s\) of the Dirac rate function at \(x_0\), evaluated at \(x\), is \(0\).

lemma iInf_diracRate_of_mem {x₀ : X} {s : Set X} (h : x₀ ∈ s) :
    (⨅ x ∈ s, ((diracRate x₀ x : ℝ≥0∞) : EReal)) = 0

Uses 2 · Used by 1

Statement usesRate function of a Dirac mass

Proof usesThe Dirac rate function vanishes at its center

Used byLarge deviation principle for a Dirac mass

LemmaInfimum of the Dirac rate function over a set avoiding the center#✓fully proved

For a point \(x_0\) of a set \(X\) and a subset \(s \subseteq X\) with \(x_0 \notin s\), the infimum over \(x \in s\) of the Dirac rate function at \(x_0\), evaluated at \(x\), is \(\infty\).

lemma iInf_diracRate_of_notMem {x₀ : X} {s : Set X} (h : x₀ ∉ s) :
    (⨅ x ∈ s, ((diracRate x₀ x : ℝ≥0∞) : EReal)) = ⊤

Uses 2 · Used by 1

Statement usesRate function of a Dirac mass

Proof usesThe Dirac rate function is infinite away from its center

Used byLarge deviation principle for a Dirac mass

LemmaLog-scaled Dirac mass of a set containing the center#✓fully proved

Let \(X\) be a measurable space, let \(\delta_{x_0}\) be the Dirac measure at a point \(x_0 \in X\), and let \(s \subseteq X\) be a set with \(x_0 \in s\). Then \(\frac{1}{n} \log \delta_{x_0}(s) = 0\) in the extended reals for every natural number \(n\), the factor \(1/n\) being read as \(0\) when \(n = 0\).

lemma dirac_ldp_term_eq_zero_of_mem {x₀ : X} {s : Set X} (h : x₀ ∈ s) (n : ℕ) :
    ((n : ℕ) : EReal)⁻¹ * ENNReal.log (Measure.dirac x₀ s) = 0

Used by 1

Used byLarge deviation principle for a Dirac mass

LemmaLog-scaled Dirac mass of a set avoiding the center#✓fully proved

Let \(X\) be a measurable space in which every singleton is measurable, let \(\delta_{x_0}\) be the Dirac measure at a point \(x_0 \in X\), and let \(s \subseteq X\) be a set with \(x_0 \notin s\). Then for every natural number \(n \ge 1\), \(\frac{1}{n} \log \delta_{x_0}(s) = -\infty\) in the extended reals, with \(\log 0 = -\infty\).

lemma dirac_ldp_term_eq_bot_of_notMem [MeasurableSingletonClass X] {x₀ : X} {s : Set X}
    (h : x₀ ∉ s) {n : ℕ}
    (hn : 1 ≤ n) : ((n : ℕ) : EReal)⁻¹ * ENNReal.log (Measure.dirac x₀ s) = ⊥

Used by 1

Used byLarge deviation principle for a Dirac mass

TheoremLarge deviation principle for a Dirac mass#✓fully proved

Let \(X\) be a \(T_1\) topological space equipped with its Borel \(\sigma\)-algebra, and let \(x_0 \in X\). The constant sequence of measures \(\mu_n = \delta_{x_0}\) satisfies the large deviation principle with the Dirac rate function of \(x_0\), which is \(0\) at \(x_0\) and \(\infty\) elsewhere.

Indeed, the mass \(1\) stays at \(x_0\), so the exponential cost of a set is \(0\) if it contains \(x_0\) and \(\infty\) otherwise.

theorem satisfiesLDP_dirac [BorelSpace X] [T1Space X] (x₀ : X) :
    SatisfiesLDP (fun _ => Measure.dirac x₀) (diracRate x₀)

Uses 9

Statement usesLarge deviation principle for a sequence of measures · Rate function of a Dirac mass

Proof usesRate function · The Dirac rate function is infinite away from its center · The Dirac rate function vanishes at its center · Log-scaled Dirac mass of a set avoiding the center · Log-scaled Dirac mass of a set containing the center · Infimum of the Dirac rate function over a set containing the center · Infimum of the Dirac rate function over a set avoiding the center

TheoremThe absolute value is a good rate function#✓fully proved

The function \(x \mapsto |x|\), viewed as a map \(\mathbb{R} \to [0, \infty]\), is a good rate function on \(\mathbb{R}\).

It is continuous, hence lower semicontinuous, and its sub-level sets at finite levels are closed intervals (or the singleton \(\{0\}\) for a negative level), hence compact.

theorem isGoodRateFunction_abs :
    IsGoodRateFunction (fun x : ℝ => ENNReal.ofReal |x|)

Uses 2

Statement usesGood rate function

Proof usesRate function

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.