Finitely supported distributions

Adapted for Lean Pool by changing module paths and selecting explicit imports.

Komlos.IsDist P means that P : E →₀ ℝ is nonnegative and has total mass 1. Komlos.mass is the sum of the weights; Komlos.mean is their weighted sum in a real vector space.

The mass and mean are additive. For pointwise maxima and minima, the sum of the two masses and the sum of the two means are preserved. Komlos.mean_mem_convexHull places the mean of a probability distribution in the convex hull of its support.

noncomputable def Komlos.mass {E : Type u_1} (P : E →₀ ℝ) : ℝ

Total weight of a finitely supported real-valued function.

Equations

• Komlos.mass P = P.sum fun (x : E) (r : ℝ) => r

noncomputable def Komlos.mean {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P : E →₀ ℝ) : E

The weighted sum of the support points, without dividing by the total mass.

Equations

• Komlos.mean P = P.sum fun (x : E) (r : ℝ) => r • x

structure Komlos.IsDist {E : Type u_1} (P : E →₀ ℝ) : Prop

A finitely supported probability distribution: nonnegative weights with total mass one.

• nonneg (x : E) : 0 ≤ P x
• mass_eq : mass P = 1

theorem Komlos.mass_eq_sum {E : Type u_1} {P : E →₀ ℝ} {s : Finset E} (h : P.support ⊆ s) : mass P = ∑ x ∈ s, P x

theorem Komlos.mean_eq_sum {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P : E →₀ ℝ} {s : Finset E} (h : P.support ⊆ s) : mean P = ∑ x ∈ s, P x • x

theorem Komlos.mass_add {E : Type u_1} (P Q : E →₀ ℝ) : mass (P + Q) = mass P + mass Q

theorem Komlos.mass_smul {E : Type u_1} (c : ℝ) (P : E →₀ ℝ) : mass (c • P) = c * mass P

theorem Komlos.mean_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : ℝ) (P : E →₀ ℝ) : mean (c • P) = c • mean P

theorem Komlos.mass_nonneg {E : Type u_1} {P : E →₀ ℝ} (h : ∀ (x : E), 0 ≤ P x) : 0 ≤ mass P

theorem Komlos.mass_mono {E : Type u_1} {P Q : E →₀ ℝ} (h : P ≤ Q) : mass P ≤ mass Q

theorem Komlos.support_inf_subset {E : Type u_1} {P Q : E →₀ ℝ} {s : Finset E} (hP : P.support ⊆ s) (hQ : Q.support ⊆ s) : (P ⊓ Q).support ⊆ s

theorem Komlos.support_sup_subset {E : Type u_1} {P Q : E →₀ ℝ} {s : Finset E} (hP : P.support ⊆ s) (hQ : Q.support ⊆ s) : (P ⊔ Q).support ⊆ s

theorem Komlos.mass_sup_add_mass_inf {E : Type u_1} (P Q : E →₀ ℝ) : mass (P ⊔ Q) + mass (P ⊓ Q) = mass P + mass Q

theorem Komlos.mean_sup_add_mean_inf {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P Q : E →₀ ℝ) : mean (P ⊔ Q) + mean (P ⊓ Q) = mean P + mean Q

theorem Komlos.mean_mem_convexHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] {S : E →₀ ℝ} (hS : IsDist S) {s : Finset E} (h : S.support ⊆ s) : mean S ∈ (convexHull ℝ) ↑s