structure IsRateFunction {X : Type u_1} [TopologicalSpace X] (I : X → ENNReal) : Prop

A rate function I : X → [0, ∞] is, by definition, a lower-semicontinuous function. This is the basic regularity hypothesis used in the formulation of a large deviation principle.

• lowerSemicontinuous : LowerSemicontinuous I

structure IsGoodRateFunction {X : Type u_1} [TopologicalSpace X] (I : X → ENNReal) extends IsRateFunction I : Prop

A good rate function is a rate function whose sub-level sets {x | I x ≤ a} are all compact. Goodness ensures that the variational problems inf_{x ∈ Γ} I(x) are attained.

• lowerSemicontinuous : LowerSemicontinuous I
• isCompact_levelSet (a : ENNReal) : IsCompact {x : X | I x ≤ a}

structure IsConvexRateFunction {X : Type u_1} [TopologicalSpace X] [AddCommMonoid X] [Module ℝ X] (I : X → ENNReal) extends IsRateFunction I : Prop

A convex rate function on a real vector space is a rate function I that is convex: I(ax + by) ≤ a · I(x) + b · I(y) for all x, y ∈ X and all weights a, b ≥ 0 with a + b = 1.

• lowerSemicontinuous : LowerSemicontinuous I
• 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

structure SatisfiesLDP {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ : ℕ → MeasureTheory.Measure X) (I : X → ENNReal) : Prop

A sequence of measures μ : ℕ → Measure X satisfies the large deviation principle with rate function I : X → [0, ∞] and speed n if I is a rate function and the following asymptotic bounds hold for every Borel set Γ ⊆ X: -inf_{x ∈ Γ°} I(x) ≤ liminf (1/n) log μ_n(Γ) ≤ limsup (1/n) log μ_n(Γ) ≤ -inf_{x ∈ Γ̄} I(x). Concretely, this is encoded as the standard pair of bounds: a liminf lower bound over open sets U and a limsup upper bound over closed sets F.

• isRateFunction : IsRateFunction I
• lower_bound (U : Set X) : IsOpen U → -⨅ x ∈ U, ↑(I x) ≤ Filter.liminf (fun (n : ℕ) => (↑n)⁻¹ * ((μ n) U).log) Filter.atTop
• upper_bound (F : Set X) : IsClosed F → Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * ((μ n) F).log) Filter.atTop ≤ -⨅ x ∈ F, ↑(I x)