putnam_2010_a3: Fix partial derivative formalization

[logical-ivan]

Modified partial derivative formalization to correct argument order and add missing coefficient: (H' : ∀ x, h x = a * (fderiv ℝ h (1, 0) x) + (fderiv ℝ h (0, 1) x)) →
(H' : ∀ x, h x = a * (fderiv ℝ h x (1, 0)) + b * (fderiv ℝ h x (0, 1)))

The English problem asks to prove that if h : ℝ² → ℝ satisfies the PDE h(x,y) = a·∂h/∂x(x,y) + b·∂h/∂y(x,y) and is bounded, then h ≡ 0.

The original formalization contains two errors:

1. Wrong argument order: fderiv ℝ h (1, 0) x evaluates the derivative at the constant point (1,0), not at the variable point x. This represents ∂h/∂x|(₁,₀) rather than ∂h/∂x|(ₓ,ᵧ). The corrected fderiv ℝ h x (1, 0) properly evaluates the partial derivative at each point x.

2. Missing coefficient b: The original omits the coefficient b in the second term, changing the PDE to h = a·∂h/∂x + ∂h/∂y. This fundamentally alters the mathematical problem—the original accidentally creates a homogeneity condition, while the correct formalization involves directional derivatives along (a,b).

[GeorgeTsoukalas]

Nice catch! My first thought was maybe the order switched at some point in Mathlib, but looks like it has always been this way - the other problems in PutnamBench using fderiv follow the format as in your fix. Looks good, thanks!