Probabilities

This defines a type Prob, which is simply any real number in the interval O to 1. This then comes with additional statements such as its application to convex sets, and it makes useful type alias for functions that only make sense on probabilities.

A significant application is in the Mixable typeclass, also in this file, which is a general notion of convex combination that applies to types as opposed to sets; elements are Mixable.mixed using Probs.

@[reducible]

def Prob : Type

Prob is a real number in the interval [0,1]. Similar to NNReal in many definitions, but this allows other nice things more 'safely' such as convex combination.

Equations

• Prob = { p : ℝ // 0 ≤ p ∧ p ≤ 1 }

instance Prob.instCoeReal : Coe Prob ℝ

Equations

• Prob.instCoeReal = { coe := Subtype.val }

instance Prob.canLift : CanLift ℝ Prob Subtype.val fun (r : ℝ) => 0 ≤ r ∧ r ≤ 1

instance Prob.instZero : Zero Prob

Equations

• Prob.instZero = { zero := ⟨0, Prob.instZero._proof_1⟩ }

instance Prob.instOne : One Prob

Equations

• Prob.instOne = { one := ⟨1, Prob.instOne._proof_1⟩ }

instance Prob.instMul : Mul Prob

Equations

• Prob.instMul = { mul := fun (x y : Prob) => ⟨↑x * ↑y, ⋯⟩ }

@[simp]

theorem Prob.coe_zero : ↑0 = 0

@[simp]

theorem Prob.coe_one : ↑1 = 1

@[simp]

theorem Prob.coe_mul (x y : Prob) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Prob.coe_inf (x y : Prob) : ↑(min x y) = min ↑x ↑y

@[simp]

theorem Prob.coe_sup (x y : Prob) : ↑(max x y) = max ↑x ↑y

instance Prob.instCommMonoidWithZero : CommMonoidWithZero Prob

Equations

• One or more equations did not get rendered due to their size.

instance Prob.instDenselyOrdered : DenselyOrdered Prob

instance Prob.instCompleteLinearOrder : CompleteLinearOrder Prob

Equations

• Prob.instCompleteLinearOrder = instCompleteLinearOrderElemIccOfFactLe

instance Prob.instInhabited : Inhabited Prob

Equations

• Prob.instInhabited = { default := 0 }

instance Prob.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero Prob

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Prob.zero_le_coe {p : Prob} : 0 ≤ ↑p

@[simp]

theorem Prob.coe_le_one {p : Prob} : ↑p ≤ 1

@[simp]

theorem Prob.zero_le {p : Prob} : 0 ≤ p

@[simp]

theorem Prob.le_one {p : Prob} : p ≤ 1

theorem Prob.eq {n m : Prob} : ↑n = ↑m → n = m

theorem Prob.eq_iff {n m : Prob} : n = m ↔ ↑n = ↑m

theorem Prob.ne_iff {x y : Prob} : ↑x ≠ ↑y ↔ x ≠ y

@[simp]

theorem Prob.toReal_mul (x y : Prob) : ↑(x * y) = ↑x * ↑y

def Prob.toNNReal : Prob → NNReal

Coercion Prob → ℝ≥0.

Equations

• ↑p = ⟨↑p, ⋯⟩

@[simp]

theorem Prob.toNNReal_mk {x : ℝ} {hx : 0 ≤ x ∧ x ≤ 1} : ↑⟨x, hx⟩ = ⟨x, ⋯⟩

instance Prob.instCoeNNReal : Coe Prob NNReal

Equations

• Prob.instCoeNNReal = { coe := Prob.toNNReal }

instance Prob.canLiftNN : CanLift NNReal Prob toNNReal fun (r : NNReal) => r ≤ 1

theorem Prob.eq_iff_nnreal (n m : Prob) : ↑n = ↑m ↔ n = m

@[simp]

theorem Prob.toNNReal_zero : ↑0 = 0

@[simp]

theorem Prob.toNNReal_one : ↑1 = 1

theorem Prob.ofNNReal_toNNReal {p : Prob} : ↑↑p = ENNReal.ofReal ↑p

def Prob.NNReal.asProb (p : NNReal) (hp : p ≤ 1) : Prob

Equations

• Prob.NNReal.asProb p hp = ⟨↑p, ⋯⟩

def Prob.NNReal.asProb' (p : NNReal) (hp : ↑p ≤ 1) : Prob

Equations

• Prob.NNReal.asProb' p hp = ⟨↑p, ⋯⟩

theorem Prob.zero_lt_coe {p : Prob} (hp : p ≠ 0) : 0 < ↑p

instance Prob.instSub : Sub Prob

Subtract a probability from another. Truncates to zero, so this is often not great to work with, for the same reason that Nat subtraction is a pain. But, it lets you write 1 - p, which is sufficiently useful on its own that this seems worth having.

Equations

• Prob.instSub = { sub := fun (p q : Prob) => ⟨max (↑p - ↑q) 0, ⋯⟩ }

theorem Prob.coe_sub (p q : Prob) : ↑(p - q) = max (↑p - ↑q) 0

@[simp]

theorem Prob.coe_one_minus (p : Prob) : ↑(1 - p) = 1 - ↑p

theorem Prob.add_one_minus (p : Prob) : ↑p + ↑(1 - p) = 1

@[simp]

theorem Prob.one_minus_inv (p : Prob) : 1 - (1 - p) = p

instance Prob.instOrderTopology : OrderTopology Prob

@[simp]

theorem Prob.coe_iInf {ι : Type u_1} [Nonempty ι] (f : ι → Prob) : ↑(⨅ (t : ι), f t) = ⨅ (t : ι), ↑(f t)

instance Prob.instNontrivial : Nontrivial Prob

@[simp]

theorem Prob.top_eq_one : ⊤ = 1

@[simp]

theorem Prob.sub_zero (p : Prob) : p - 0 = p

theorem Prob.toNNReal_Continuous : Continuous toNNReal

class Mixable (U : outParam (Type u)) (T : Type v) [AddCommMonoid U] [Module ℝ U] : Type (max u v)

A Mixable T typeclass instance gives a compact way of talking about the action of probabilities for forming linear combinations in convex spaces. The notation p [ x₁ ↔ x₂ ] means to take a convex combination, equal to x₁ if p=1 and to x₂ if p=0.

Mixable is defined by an "underlying" data type U with addition and scalar multiplication, and a bijection between the T and a convex set of U. For instance, in Mixable (Distribution (Fin n)), U is n-element vectors (which form the probability simplex, degenerate in one dimension). For QuantumInfo.Finite.MState density matrices in quantum mechanics, which are PSD matrices of trace 1, U is the underlying matrix.

Why not just stick with existing notions of Convex? Convex requires that the type already forms an AddCommMonoid and Module ℝ. But many types, such as Distribution, are not: there is no good notion of "multiplying a probability distribution by 0.3" to get another distribution. We can coerce the distribution into, say, a vector or a function, but then we are not doing arithmetic with distributions. Accordingly, the expression 0.3 * distA + 0.7 * distB cannot represent a distribution on its own.

• to_U : T → U

  Getter for the underlying data

• to_U_inj {T₁ T₂ : T} : to_U T₁ = to_U T₂ → T₁ = T₂

  Proof that this getter is injective

• convex : Convex ℝ (Set.range to_U)

  Proof that this image is convex

• mkT {u : U} : (∃ (t : T), to_U t = u) → { t : T // to_U t = u }

  Function to get a T from a proof that U is in the set.

@[reducible]

def Mixable.mix_ab {T : Type u_1} {U : Type u_2} [AddCommMonoid U] [Module ℝ U] [inst : Mixable U T] {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x₁ x₂ : T) : T

Equations

• Mixable.mix_ab ha hb hab x₁ x₂ = ↑(Mixable.mkT ⋯)

def Mixable.mix {T : Type u_1} {U : Type u_2} [AddCommMonoid U] [Module ℝ U] [inst : Mixable U T] (p : Prob) (x₁ x₂ : T) : T

Mixable.mix represents the notion of "convex combination" on the type T, afforded by the Mixable instance. It takes a Prob, that is, a Real between 0 and 1. For working directly with a Real, use mix_ab.

Equations

• p[x₁↔x₂] = Mixable.mix_ab ⋯ ⋯ ⋯ x₁ x₂

@[simp]

theorem Mixable.to_U_of_mkT {T : Type u_1} {U : Type u_2} [AddCommMonoid U] [Module ℝ U] [inst : Mixable U T] (u : U) {h : ∃ (t : T), to_U t = u} : to_U ↑(mkT h) = u

def Mixable.«term_[_↔_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mixable.«term_[_↔_:_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Mixable.mix_zero {T : Type u_1} {U : Type u_2} [AddCommMonoid U] [Module ℝ U] [inst : Mixable U T] (x₁ x₂ : T) : 0[x₁↔x₂] = x₂

instance Mixable.instUniv {T : Type u_1} [AddCommMonoid T] [Module ℝ T] : Mixable T T

When T is the whole space, and T is a suitable vector space over ℝ, we get a Mixable instance.

Equations

• Mixable.instUniv = { to_U := id, to_U_inj := ⋯, convex := ⋯, mkT := fun {u : T} (x : ∃ (t : T), id t = u) => ⟨u, ⋯⟩ }

@[simp]

theorem Mixable.mkT_instUniv {T : Type u_1} [AddCommMonoid T] [Module ℝ T] {t : T} (h : ∃ (t' : T), to_U t' = t) : mkT h = ⟨t, ⋯⟩

@[simp]

theorem Mixable.to_U_instUniv {T : Type u_1} [AddCommMonoid T] [Module ℝ T] {t : T} : to_U t = t

theorem Mixable.instPi.lem_1 {D : Type u_3} {T : D → Type u_4} {U : D → Type u_5} [(i : D) → AddCommMonoid (U i)] [(i : D) → Module ℝ (U i)] [inst : (i : D) → Mixable (U i) (T i)] {u : (i : D) → U i} (h : ∃ (t : (i : D) → T i), (fun (d : D) => to_U (t d)) = u) (d : D) : ∃ (t : T d), to_U t = u d

instance Mixable.instPi {D : Type u_3} {T : D → Type u_4} {U : D → Type u_5} [(i : D) → AddCommMonoid (U i)] [(i : D) → Module ℝ (U i)] [inst : (i : D) → Mixable (U i) (T i)] : Mixable ((i : D) → U i) ((i : D) → T i)

Mixable instance on Pi types.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Mixable.val_mkT_instPi {T : Type u_1} {U : Type u_2} [AddCommMonoid U] [Module ℝ U] (D : Type u_3) [inst : Mixable U T] {u : D → U} (h : ∃ (t : D → T), to_U t = u) : ↑(mkT h) = fun (d : D) => ↑(mkT ⋯)

@[simp]

theorem Mixable.to_U_instPi {T : Type u_1} {U : Type u_2} [AddCommMonoid U] [Module ℝ U] (D : Type u_3) [inst : Mixable U T] {t : D → T} : to_U t = fun (d : D) => to_U (t d)

def Mixable.instSubtype {U : Type u_2} [AddCommMonoid U] [Module ℝ U] {T : Type u_3} {P : T → Prop} (inst : Mixable U T) (h : ∀ {x y : T} ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), P x → P y → P (mix_ab ha hb hab x y)) : Mixable U { t : T // P t }

Mixable instances on subtypes (of other mixable types), assuming that they have the correct closure properties.

Equations

• One or more equations did not get rendered due to their size.

instance Prob.instMixable : Mixable ℝ Prob

Probabilities Prob themselves are convex.

Equations

• Prob.instMixable = { to_U := Subtype.val, to_U_inj := ⋯, convex := Prob.instMixable._proof_1, mkT := fun {u : ℝ} (h : ∃ (t : Prob), ↑t = u) => ⟨⟨u, ⋯⟩, ⋯⟩ }

@[simp]

theorem Prob.to_U_mixable {T : Type u_1} [AddCommMonoid T] [SMul ℝ T] (t : Prob) : Mixable.to_U t = ↑t

@[simp]

theorem Prob.mkT_mixable (u : ℝ) (h : ∃ (t : Prob), Mixable.to_U t = u) : Mixable.mkT h = ⟨⟨u, ⋯⟩, ⋯⟩

@[reducible, inline]

abbrev Prob.mix {U : Type u_1} {T : Type u_2} [AddCommMonoid U] [Module ℝ U] [inst : Mixable U T] (p : Prob) (x₁ x₂ : T) : T

Prob.mix is an alias of Mixable.mix so it can be accessed from a probability with dot notation, e.g. p.mix x y.

Equations

• p.mix x₁ x₂ = p[x₁↔x₂]

noncomputable def Prob.negLog : Prob → ENNReal

Map a probability [0,1] to [0,+∞] with -log p. Special case that 0 maps to +∞ (not 0, as Real.log does). This makes it Antitone.

Equations

• p.negLog = if p = 0 then ⊤ else ↑⟨-Real.log ↑p, ⋯⟩

def Prob.«term—log» : Lean.ParserDescr

Equations

• Prob.«term—log» = Lean.ParserDescr.node `Prob.«term—log» 1024 (Lean.ParserDescr.symbol "—log ")

theorem Prob.negLog_Antitone : Antitone negLog

@[simp]

theorem Prob.negLog_zero : negLog 0 = ⊤

@[simp]

theorem Prob.negLog_one : negLog 1 = 0

@[simp]

theorem Prob.negLog_eq_top_iff {p : Prob} : p.negLog = ⊤ ↔ p = 0

theorem Prob.negLog_pos_ENNReal {p : Prob} (hp : p ≠ 0) : p.negLog = ↑⟨-Real.log ↑p, ⋯⟩

@[simp]

theorem Prob.negLog_pos_Real {p : Prob} : p.negLog.toReal = -Real.log ↑p

theorem Prob.le_negLog_of_le_exp {p : Prob} {x : ℝ} (h : ↑p ≤ Real.exp (-x)) : ENNReal.ofReal x ≤ p.negLog

theorem Prob.negLog_ne_top {p : Prob} (hp : 0 < ↑p) : p.negLog ≠ ⊤

theorem Prob.negLog_eq_neg_ENNReal_log (p : Prob) : ↑p.negLog = -(↑↑p).log

theorem Prob.negLog_eq_ofReal_neg_log {p : Prob} (hp : 0 < p) : ENNReal.ofReal (-Real.log ↑p) = p.negLog

@[simp]

theorem Prob.zero_lt_negLog {p : Prob} : 0 < p.negLog ↔ p ≠ 1

theorem Prob.Continuous_negLog : Continuous negLog