How to represent Bayes' theorem in LEAN4

Stream: new members

[Zhu]

Hi! I'm trying to use LEAN to proof some probability theory statements like this

$$P(\bar{A_1}\cdots \bar{A_n}) = P(\bar{A_1}) \ P(\bar{A_2}|\bar{A_1}) \ P(\bar{A_3}|\bar{A_1}\bar{A_2}) \cdots P(\bar{A_n}|\bar{A_1}\cdots\bar{A_{n-1}})$$

but I don't know how to represent the  conditional probability.
here's my current code (trying to formalize Bayes' theorem):

import Mathlib

open MeasureTheory
open ProbabilityTheory
open Finset


variable
  {Ω : Type*} [MeasurableSpace Ω]
  {P : ProbabilityMeasure Ω}
  (A B : Set Ω)

#check (A ∩ B)


theorem test :
  P ⟦A | B⟧ ≤ 1 := by simp

theorem bayes_theme :
  P B ≠ 0 → P A ≠ 0 →
  P (A ∩  B) ≠ 0 →
  P (A | B) = (P (B | A) * P A) / P B := by
  sorry

Any pointers would be greatly appreciated!

[Etienne Marion]

This is docs#ProbabilityTheory.cond

[Rémy Degenne]

You should probably not be using P : ProbabilityMeasure Ω, but instead P : Measure Ω together with [IsProbabilityMeasure P]. Most of the library is built with Measure. The type ProbabilityMeasure was introduced to put a topology on probability measures, and you should not use it unless you want to work with that topology.

We should really update the docstring for ProbabilityMeasure to point that out.

[Zhu]

Thanks, that's helpful! :big_smile:

[Zhu]

Here is my current code attempt. There's an issue: the compiler prompts me to add "set_option checkBinderAnnotations false" in order for it to compile successfully. Is there a way to avoid using this setting?

import Mathlib

open MeasureTheory
open ProbabilityTheory

section

set_option checkBinderAnnotations false

variable
  {Ω : Type*} [MeasurableSpace Ω]
  {P : Measure Ω} [IsFiniteMeasure P] [IsProbabilityMeasure P]
  {A B : Set Ω} [MeasurableSet A] [MeasurableSet B]

#check A
#check P A
#check P (A ∩ B) * P B
#check cond P B
#check (cond P B) A
#check P [A|B]

#check cond_apply
#check Set.inter_comm A B
#check cond_eq_inv_mul_cond_mul

end

set_option checkBinderAnnotations false

example
  {Ω : Type*} [MeasurableSpace Ω]
  {P : Measure Ω} [IsFiniteMeasure P] [IsProbabilityMeasure P]
  {A B : Set Ω} [MeasurableSet A] [MeasurableSet B]
: A ∩ B = B ∩ A := by
  rw [Set.inter_comm A B]

example
  {Ω : Type*} [MeasurableSpace Ω]
  {P : Measure Ω} [IsFiniteMeasure P] [IsProbabilityMeasure P]
  {A B : Set Ω} [MeasurableSet A] [hb : MeasurableSet B]
: (cond P B) A = P (A ∩ B) / P B := by
  rw [div_eq_mul_inv]
  rw [cond_apply]
  simp [mul_comm]
  simp [Set.inter_comm A B]
  exact hb

12312312312312.png

[Etienne Marion]

You can't write [MeasurableSet A]. The [...] notation is meant for stuff which should be inferred automatically by a mechanism called typeclass inference. For example, if you have a theorem about fields and you want to apply it to real numbers, you do not need to specify that real numbers are a field because there exists somewhere an instance of a field structure over the reals, and Lean knows how to find it. This is a useful and powerful mechanism, but is not meant to be used with everything (otherwise it would get too messy for the algorithm I guess). Therefore the only arguments you can put in [...] are those which are defined as a class in Lean (for example docs#MeasurableSpace etc). You can find more informations here for example.

In your case MeasurableSet is a standard definition, so you should put it between parentheses.

The option checkBinderAnnotationsforces you to only put classes between square brackets, which you should always do.

[Zhu]

Thanks for your reply, I understand now.