From 2d9fd2ccfabb5856f60ddfab20f709c8c3806171 Mon Sep 17 00:00:00 2001 From: George Tsoukalas <99286219+GeorgeTsoukalas@users.noreply.github.com> Date: Fri, 6 Dec 2024 10:34:00 -0600 Subject: [PATCH] Update lean4/src/putnam_1989_b6.lean Co-authored-by: Eric Wieser --- lean4/src/putnam_1989_b6.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4/src/putnam_1989_b6.lean b/lean4/src/putnam_1989_b6.lean index 873cfc3..988dbbf 100644 --- 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