Independence -- Lean issues

[EmilyARussell]

Here is the draft of the basic definitions and theorems for the independence and covariance sections of the Defs file. They do not work. I'm not sure what im not understanding about the notation for definitions and theorems but there are red lines for so many things. Specifically, I cannot figure out how to write the hypothesis properly using correct variables. And also it seems a different FinRV is necessary for probability and expectation. I'm at a loss. I will bring this all to class to discuss with Marek I just wanted to post to show what ive worked on without submitting a pull request full of errors.
------------------------------ Independence ---------------------------

section independence
variable {n : ℕ} {P : Findist n}
variable {X Y : FinRV n Bool}

def indpRV (X Y : FinRV n Bool) :=
ℙ[X * Y // P ] == ℙ[X//P]*ℙ[Y//P]

theorem indpCond (h: indpRV A B): ℙ[A|B//P] = ℙ[A//P] := !!! ERRORS
by sorry --unfold probability_cnd
-- ℙ[A | B // P] = ℙ[A * B // P] / ℙ[ B // P ]
-- this proof will have the dividing by 0 issue
-- with indp definition, otherwise simple

theorem indpExpectation (h: indp A B): 𝔼[AB // P] = 𝔼[A // P] * 𝔼[B // P] :=
by sorry
-- (xy) * v ℙ[XY] by defn expectation
-- (xy) * v ℙ[X] * ℙ[Y] := by hypothesis of independence
-- will need properties of dot products here

end independence

------------------------------ Covariance ---------------------------
section covariance
variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ)

def covar : ℚ := 𝔼[X*Y // P] - 𝔼[X // P] * 𝔼[Y // P]

notation "cov[" X "," Y "//" P "]" => covar P X Y

theorem indpCov0 (h: indpRV X Y) : cov[X,Y//P] = 0 :=
by sorry
-- very simple given expectation theorem works, just use defn and its good

end covariance

[EmilyARussell]

Posting my update, currently trying to get definitions for CDF so that I can define and prove for the Real valued random variables
------------------------------ Independence ---------------------------
section independence
variable {n : ℕ} {P : Findist n}
variable {A B : FinRV n Bool}
variable {X Y : FinRV n ℚ}

-- need CDF definition
def cdf (x: ℚ) : ℚ := ℙ[X ≤ᵣ x // P]

notation "F_" X "(" x "//" P")" => cdf P X x

--A B events
--X Y real valued

def Findist.indpRVBool {P : Findist n} (A : FinRV n Bool) (B : FinRV n Bool) :=
ℙ[A * B // P ] = ℙ[A//P]*ℙ[B//P]

-- TODO FIX:
def Findist.indpRVreal {P : Findist n} (X : FinRV n ℚ) (Y : FinRV n ℚ) :=
by sorry --this requires a whole different definition

-- Includes assumption that probability b isnt 0 since then conditional probability would be undefined
theorem indpCond (h: P.indpRVBool A B) (h2: ℙ[B // P] ≠ 0) : ℙ[A|B//P] = ℙ[A//P] :=
by unfold probability_cnd
unfold Findist.indpRVBool at h
rw [h]
simp_all

--Findlist. things

theorem indpExpectation (h: P.indpRVreal X Y): 𝔼[AB // P] = 𝔼[A // P] * 𝔼[B // P] :=
by sorry
-- need indp of RV defn
-- (xy) * v ℙ[XY] by defn expectation
-- (xy) * v ℙ[X] * ℙ[Y] := by hypothesis of independence
-- will need properties of dot products here

end independence

------------------------------ Covariance ---------------------------
section covariance
variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ)

def covar : ℚ := 𝔼[X*Y // P] - 𝔼[X // P] * 𝔼[Y // P]

notation "cov[" X "," Y "//" P "]" => covar P X Y

--change defn

theorem indpCov0 (h: indpRV X Y) : cov[X,Y//P] = 0 :=
by sorry
-- very simple given expectation theorem works, just use defn and its good

end covariance