Maximum utility and Bernoulli distributions

Contains closed-form expressions for e-values, maximum utility, and divergences for Bernoulli distributions.

Main definitions

• Ber: Bernoulli distribution on {0, 1}.

Main statements

• isEVar_bernoulli_le_iff: Characterization of e-variables for Bernoulli distributions with mean at most δ.
• maxUtility_bernoulli_half_le: Maximum utility for Bernoulli distribution with mean at most $\frac{1}{2}$.
• maxUtility_bernoulli_half_le: Maximum utility for Bernoulli distribution with mean at most $\frac{1}{2}$.
• erenyiDiv_bernoulli: e-Rényi divergence between two Bernoulli distributions with mean at most $\frac{1}{2}$.
• echernoffDiv_bernoulli: e-Chernoff divergence between two Bernoulli distributions with mean at most $\frac{1}{2}$.

noncomputable def ProbabilityTheory.Ber (p : ENNReal) : MeasureTheory.Measure ↑{0, 1}

Bernoulli distribution on {0, 1}. Using 1 - (1 - p) ensures that we always have a probability measure.

Equations

• ProbabilityTheory.Ber p = (1 - p) • MeasureTheory.Measure.dirac ⟨0, ProbabilityTheory.Ber._proof_1⟩ + (1 - (1 - p)) • MeasureTheory.Measure.dirac ⟨1, ProbabilityTheory.Ber._proof_2⟩

@[simp]

theorem ProbabilityTheory.ber_zero : Ber 0 = MeasureTheory.Measure.dirac ⟨0, Ber._proof_1⟩

@[simp]

theorem ProbabilityTheory.ber_one : Ber 1 = MeasureTheory.Measure.dirac ⟨1, Ber._proof_2⟩

@[simp]

theorem ProbabilityTheory.ber_apply_singleton_zero {p : ENNReal} : (Ber p) {⟨0, Ber._proof_1⟩} = 1 - p

@[simp]

theorem ProbabilityTheory.ber_apply_singleton_one {p : ENNReal} : (Ber p) {⟨1, Ber._proof_2⟩} = 1 - (1 - p)

@[simp]

theorem ProbabilityTheory.lintegral_ber {p : ENNReal} {f : ↑{0, 1} → ENNReal} : ∫⁻ (x : ↑{0, 1}), f x ∂Ber p = (1 - p) * f ⟨0, Ber._proof_1⟩ + (1 - (1 - p)) * f ⟨1, Ber._proof_2⟩

instance ProbabilityTheory.instIsProbabilityMeasureElemRealInsertSetOfNatSingletonBer {p : ENNReal} : MeasureTheory.IsProbabilityMeasure (Ber p)

theorem ProbabilityTheory.apply_zero_add_apply_one_eq_one (R : MeasureTheory.Measure ↑{0, 1}) [MeasureTheory.IsProbabilityMeasure R] : R {⟨0, Ber._proof_1⟩} + R {⟨1, Ber._proof_2⟩} = 1

@[simp]

theorem ProbabilityTheory.one_sub_apply_one (R : MeasureTheory.Measure ↑{0, 1}) [MeasureTheory.IsProbabilityMeasure R] : 1 - R {⟨1, Ber._proof_2⟩} = R {⟨0, Ber._proof_1⟩}

@[simp]

theorem ProbabilityTheory.one_sub_apply_zero (R : MeasureTheory.Measure ↑{0, 1}) [MeasureTheory.IsProbabilityMeasure R] : 1 - R {⟨0, Ber._proof_1⟩} = R {⟨1, Ber._proof_2⟩}

@[simp]

theorem ProbabilityTheory.one_sub_one_sub_measure_apply (R : MeasureTheory.Measure ↑{0, 1}) [MeasureTheory.IsProbabilityMeasure R] (s : Set ↑{0, 1}) : 1 - (1 - R s) = R s

theorem ProbabilityTheory.eq_ber_lintegral (R : MeasureTheory.Measure ↑{0, 1}) [MeasureTheory.IsProbabilityMeasure R] : R = Ber (∫⁻ (x : ↑{0, 1}), ENNReal.ofReal ↑x ∂R)

theorem ProbabilityTheory.isEVar_bernoulli_le_iff {δ : ℝ} (hδ_pos : 0 < δ) (hδ : δ ≤ 1) (X : ↑{0, 1} → ENNReal) : IsEVar X {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑{0, 1}), ↑x ∂μ ≤ δ} ↔ ∃ (u : ℝ) (_ : 0 ≤ u) (_ : u ≤ δ⁻¹), ∀ (x : ↑{0, 1}), X x ≤ ENNReal.ofReal (1 + u * (↑x - δ))

The e-variables for Bernoulli measures with mean at most δ are the functions f that satisfy f x ≤ 1 + u * (x - δ) for u ∈ [0, δ⁻¹].

theorem ProbabilityTheory.quadratic_inequality {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt_one : δ < 1) (u : ℝ) : (1 - u * δ) * (1 + u * (1 - δ)) ≤ (1 - δ)⁻¹ * (δ⁻¹ * 4⁻¹)

theorem ProbabilityTheory.four_le_mul_inv {δ : ℝ} (hδ_pos : 0 < δ) (hδ_lt : δ < 1) : 4 ≤ (1 - δ)⁻¹ * δ⁻¹

noncomputable def ProbabilityTheory.klBer (p q : ENNReal) : ENNReal

Kullback-Leibler divergence between two Bernoulli distributions. Meaningful only if p, q ≤ 1.

Equations

• ProbabilityTheory.klBer p q = (↑p * (p / q).log + (1 - ↑p) * ((1 - p) / (1 - q)).log).toENNReal

theorem ProbabilityTheory.klBer_half (δ : ℝ) (hδ_pos : 0 < δ) (hδ_lt : δ < 1) : klBer 2⁻¹ (ENNReal.ofReal δ) = ENNReal.ofReal (Real.log (1 / (4 * δ * (1 - δ))))

theorem ProbabilityTheory.maxUtility_bernoulli_le {p : ENNReal} {δ : ℝ} (hδ_pos : 0 < δ) (hδ : δ ≤ 2⁻¹) (hp : ENNReal.ofReal δ ≤ p) : maxUtility (Ber p) {x : MeasureTheory.Measure ↑{0, 1} | ∃ q ≤ ENNReal.ofReal δ, Ber q = x} logUtility = 2⁻¹ * ↑(klBer p (ENNReal.ofReal δ))

theorem ProbabilityTheory.maxUtility_bernoulli_half_le {δ : ℝ} (hδ_pos : 0 < δ) (hδ : δ ≤ 2⁻¹) : maxUtility (Ber 2⁻¹) {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑{0, 1}), ↑x ∂μ ≤ δ} logUtility = 2⁻¹ * ↑(Real.log (1 / (4 * δ * (1 - δ))))

The maximum utility for Bernoulli distribution with mean at most 1/2 is 2⁻¹ * log (1 / (4 * δ * (1 - δ))).

theorem ProbabilityTheory.eq_bernoulli_half_of_map_eq {R : MeasureTheory.Measure ↑{0, 1}} [MeasureTheory.IsProbabilityMeasure R] (hRφ : MeasureTheory.Measure.map (fun (x : ↑{0, 1}) => ⟨1 - ↑x, ⋯⟩) R = R) : R = Ber 2⁻¹

theorem ProbabilityTheory.map_bernoulli_half_eq : MeasureTheory.Measure.map (fun (x : ↑{0, 1}) => ⟨1 - ↑x, ⋯⟩) (Ber 2⁻¹) = Ber 2⁻¹

theorem ProbabilityTheory.map_bernoulli_le_eq_bernoulli_ge (δ : ℝ) : {x : MeasureTheory.Measure ↑{0, 1} | ∃ μ ∈ {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑{0, 1}), ↑x ∂μ ≤ δ}, MeasureTheory.Measure.map (fun (x : ↑{0, 1}) => ⟨1 - ↑x, ⋯⟩) μ = x} = {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ 1 - δ ≤ ∫ (x : ↑{0, 1}), ↑x ∂μ}

theorem ProbabilityTheory.erenyiDiv_bernoulli {δ : ℝ} (hδ_pos : 0 < δ) (hδ : δ ≤ 2⁻¹) : erenyiDiv 2⁻¹ {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑{0, 1}), ↑x ∂μ ≤ δ} {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ 1 - δ ≤ ∫ (x : ↑{0, 1}), ↑x ∂μ} = ENNReal.ofReal (Real.log (1 / (4 * δ * (1 - δ))))

The e-Rényi divergence between two Bernoulli distributions with mean at most 1/2 is log (1 / (4 * δ * (1 - δ))).

theorem ProbabilityTheory.echernoffDiv_bernoulli {δ : ℝ} (hδ_pos : 0 < δ) (hδ : δ ≤ 2⁻¹) : echernoffDiv {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ ∫ (x : ↑{0, 1}), ↑x ∂μ ≤ δ} {μ : MeasureTheory.Measure ↑{0, 1} | MeasureTheory.IsProbabilityMeasure μ ∧ 1 - δ ≤ ∫ (x : ↑{0, 1}), ↑x ∂μ} = 2⁻¹ * ENNReal.ofReal (Real.log (1 / (4 * δ * (1 - δ))))

The e-Chernoff divergence between two Bernoulli distributions with mean at most 1/2 is 2⁻¹ * log (1 / (4 * δ * (1 - δ))).