some ideas

Author: marekpetrik

MDPLib/Probability/Basic.lean

@@ -501,16 +501,18 @@ theorem law_total_exp : 𝔼[𝔼[X |ᵣ L // P] // P] = 𝔼[X // P] :=
     _ =  ∑ i : Fin k, 𝔼[X * (L =ᵢ i) // P] := by apply Fintype.sum_congr; intro i; apply exp_congr; rw[indi_eq_indr] 
     _ = 𝔼[X // P]  := by rw [←exp_decompose]
 
-example : ∀x, x ∈ Finset.univ.image X ↔ x ∈ (List.ofFn X |> List.dedup) := 
-  by intro x 
-     constructor 
-     · intro h
-       refine List.mem_dedup.mpr ?_
-       rw [Fin.univ_image_def] at h
-       rw [List.mem_toFinset] at h
-       exact h 
-     · intro h
-       sorry
+--- shows that using a set and list is the same
+lemma finset_image_eq_list_map_dedup : ∀x, x ∈ Finset.univ.image X ↔ x ∈ (List.ofFn X |> List.dedup) := 
+  by intro x; constructor <;> simp [Fin.univ_image_def,List.mem_toFinset] 
+
+
+#check Finset.sum
+
+
+example (f : ℚ → ℚ) : (∑ y ∈ (Finset.univ.image X), f y) = ((List.ofFn X |> List.dedup).map f).sum :=  sorry
+
+      
+
 
 /-- Shows that our definition of expectation is correct -/ 
 theorem expect_def_correct : 𝔼[ X // P] = ∑ y ∈ (Finset.univ.image X), (ℙ[ X =ᵣ y // P] * y) := by