Proof of Proposition 2, Online Appendix p. 1 — affine invariance of majorization

Proved

AgriSubsidy.Combined.prop2_proof_affine

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-vectorsmajorizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $u$ and $v$ be finite real vectors of the same length with $u\ge^m v$ . Every common affine transformation, with any real slope $c$ and intercept $d$ , preserves their majorization order:

u\ge^m v\quad\Longrightarrow\quad (cu_j+d)_j\ge^m(cv_j+d)_j.

This is the order property cited in the paper's proof of Proposition 2 and used when Cournot output is affine in the farmer ratio.

Formalization Note The slope may be negative or zero, as allowed by the paper's unrestricted planting subsidy.

Preamble

import Mathlib
import Definitions.Def_AgriSubsidy_Combined_Setting
import Definitions.Def_AgriSubsidy_Combined_Majorization

Formal statement

namespace AgriSubsidy.Combined

theorem prop2_proof_affine {N : ℕ} (u v : Fin N → ℝ)
    (h : Majorizes u v) (c d : ℝ) :
    Majorizes (fun j => c * u j + d) (fun j => c * v j + d) := by sorry

end AgriSubsidy.Combined

Source

Fan, Feng, Li, Shanthikumar, Wu, Output-Oriented Agricultural Subsidy Design, SSRN 4378693 (version of 2023-03-18), Online Appendix p. 1, Proof of Proposition 2; cites Marshall et al. (1979), Theorem A.1.f

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph