Update lean4/src/putnam_1989_b6.lean

Co-authored-by: Eric Wieser <[email protected]>
trishullab · Dec 6, 2024 · 2d9fd2c · 2d9fd2c
1 parent dda4b9d
commit 2d9fd2c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4/src/putnam_1989_b6.lean b/lean4/src/putnam_1989_b6.lean
@@ -15,5 +15,5 @@ theorem putnam_1989_b6
     (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧
     (∀ f : ℝ → ℝ,
       f 1 = 0 ∧ ContinuousOn f (Icc 0 1) →
-      𝔼[(↑) ∘ (S f)] = ∫ t in (0)..1, (f t) * (P.eval t)) :=
+      𝔼[fun x => S f x] = ∫ t in (0)..1, f t * P.eval t) :=
   sorry