Fix some formalizations, provide few Lean rewrites.

[GeorgeTsoukalas]

No description provided.

[eric-wieser]

Separately, I worry that this expected value is incorrect, as it is not conditioning on the fact that x lies within the appropriate region

[GeorgeTsoukalas]

I think that you're right. x does not lie in the appropriate region, and although the S f should be 0 in the extra space, it should still affect the expectation. What's a good workaround? I could write out an integral for the expectation explicitly over the right region.

[ocfnash]

Yeah this is an n + 2-dimensional integral instead of an n-dimensional one. Indeed, the infoview confirms that the measure used for this expectation is (volume : Measure <| Fin (n + 2) → Icc (0 : ℝ) 1). Since S f is zero almost everywhere in this region (where we fail to have x 0 = 0 ∧ x (-1) = 1) I believe this expectation is zero.

[ocfnash]

I have some time this morning so I'll see if I can write a formalisation which avoids the issues identified.

[ocfnash]

I think the following is correct:

theorem putnam_1989_b6
    (n : ℕ) [NeZero n]
    (I : (Fin n → ℝ) → Fin (n + 2) → ℝ)
    (I_def : ∀ x i, I x i = if i = 0 then 0 else if i = - 1 then 1 else x (i : ℕ).pred)
    (X : Set (Fin n → ℝ))
    (X_def : ∀ x, x ∈ X ↔ 0 < x 0 ∧ x (-1) < 1 ∧ ∀ i, i + 1 < n → x i < x (i + 1))
    (S : (ℝ → ℝ) → (Fin (n + 2) → ℝ) → ℝ)
    (S_def : ∀ f x, S f x = ∑ i in Finset.Iic n, (x (i + 1) - x i) * f (i + 1)) :
    ∃ P : Polynomial ℝ,
      P.degree = n ∧
      (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧
      (∀ f : ℝ → ℝ, f 1 = 0 → ContinuousOn f (Icc 0 1) →
        ∫ x, S f (I x) ∂ℙ[|X] = ∫ t in (0)..1, f t * P.eval t) :=
  sorry

[GeorgeTsoukalas]

I think this looks right to me as well - I will update the PR. Thank you for providing a fix!