Experimentation.DesignBased.Optimality
This file treats a randomization design as the object being chosen from a finite family under an ordered risk criterion.
Optimality 5 core · 5 supporting This file treats a randomization design as the object being chosen from a finite family under an ordered risk criterion. ★ DesignFamily★ exists_isOptimalOn
Design-family optimality criteria
This file treats a randomization design as the object being chosen from a finite family under an ordered risk criterion.
The declarations DesignFamily, Dominates, and IsOptimalOn formalize candidate sets,
weak domination, and least-risk designs. The theorem exists_isOptimalOn shows that every
nonempty finite design family has an optimal member. The risk functional mseRisk packages the
mean squared error of a design-indexed estimator, with mseRisk_nonneg and
mseRisk_eq_var_of_unbiased connecting it to nonnegativity and variance for unbiased estimators.
A design family: a set of candidate randomization designs on a common assignment space Ω, among which the experimenter chooses.
Definition (Lean source)
D₁ weakly dominates D₂ under the risk criterion R when it carries no larger risk: R D₁ ≤ R D₂.
Definition (Lean source)
A design D₀ is optimal in the family 𝒟 under risk R when it belongs to 𝒟 and carries the least risk among all members.
Definition (Lean source)
Existence of an optimal design. For a design family 𝒟 and a risk criterion R valued in a linear order, if 𝒟 is finite and 𝒟 is nonempty, then there exists a design in 𝒟 that is optimal — it dominates every other member of the family under R.
Formal statement
Proof (Lean source)
The mean-squared-error risk of a design-indexed estimator est for target μ: the risk assigned to a design D is est D's mean squared error under D.
Definition (Lean source)
5 supporting declarations (lemmas, instances)
-
refllemma — Domination is reflexive: every design dominates itself.Proof (Lean source)
lemma Dominates.refl {α : Type*} [Preorder α] (R : FiniteDesign Ω → α) (D : FiniteDesign Ω) : Dominates R D D := le_refl _ -
translemma — Domination is transitive.hypothesesconclusionDominates R D₁ D₃Proof (Lean source)
lemma Dominates.trans {α : Type*} [Preorder α] {R : FiniteDesign Ω → α} {D₁ D₂ D₃ : FiniteDesign Ω} (h₁ : Dominates R D₁ D₂) (h₂ : Dominates R D₂ D₃) : Dominates R D₁ D₃ := le_trans h₁ h₂ -
dominateslemma — An optimal design dominates every member of its family.hypothesesconclusionDominates R D₀ DProof (Lean source)
lemma IsOptimalOn.dominates {α : Type*} [Preorder α] {𝒟 : DesignFamily Ω} {R : FiniteDesign Ω → α} {D₀ : FiniteDesign Ω} (h : IsOptimalOn 𝒟 R D₀) {D : FiniteDesign Ω} (hD : D ∈ 𝒟) : Dominates R D₀ D := h.2 D hD -
mseRisk_nonneglemma — Mean-squared-error risk is nonnegative.Proof (Lean source)
lemma mseRisk_nonneg (est : FiniteDesign Ω → Ω → ℝ) (μ : ℝ) (D : FiniteDesign Ω) : 0 ≤ mseRisk est μ D := D.mse_nonneg _ _ -
mseRisk_eq_var_of_unbiasedlemma — For an estimator that is unbiased under every design in the family, the mean-squared-error risk coincides with the variance there.hypothesesconclusionmseRisk est μ D = D.Var (est D)Proof (Lean source)
lemma mseRisk_eq_var_of_unbiased {est : FiniteDesign Ω → Ω → ℝ} {μ : ℝ} {D : FiniteDesign Ω} (h : D.Unbiased (est D) μ) : mseRisk est μ D = D.Var (est D) := D.mse_eq_var_of_unbiased h
Minimax 5 core · 3 supporting Minimax designs minimize worst-case risk over a finite family of states of nature. ★ exists_isMinimaxOn
Minimax design criteria
Minimax designs minimize worst-case risk over a finite family of states of nature.
The definition worstRisk takes the maximum of R y D over a nonempty finite state set, and
IsMinimaxOn asks a design to minimize that criterion inside a design family. The theorem
exists_isMinimaxOn inherits finite-family existence from exists_isOptimalOn. The declarations
bestRisk, regret, and regret_nonneg formalize statewise regret relative to the best design
available in the same finite family.
The worst-case risk of a design D over a nonempty finite set s of states of nature: the largest risk R y D incurred as the state y ranges over s.
Definition (Lean source)
A design is minimax in the family 𝒟 over the states s when it belongs to 𝒟 and has the least worst-case risk among all members.
Definition (Lean source)
Existence of a minimax design. For a design family 𝒟 and a risk criterion R indexed by states of nature, if the state set s is nonempty, the design family 𝒟 is finite, and 𝒟 is nonempty, then there exists a design in 𝒟 that is minimax — it minimizes the worst-case risk over s among all members of 𝒟. Immediate from exists_isOptimalOn applied to the worst-case-risk criterion.
Formal statement
Proof (Lean source)
The best achievable risk at state y over the finite design family 𝒟: the least risk R y D as D ranges over 𝒟. (Defined via a chosen minimizer, which exists by exists_isOptimalOn; bestRisk_le and le_bestRisk characterize it.)
Definition (Lean source)
The regret of a design D at state y, relative to the finite family 𝒟: how much worse its risk is than the best risk achievable in 𝒟 at that state.
Definition (Lean source)
3 supporting declarations (lemmas, instances)
-
le_worstRisklemma — The worst-case risk dominates the risk at every state in the family.hypothesesconclusionR y D ≤ worstRisk s hs R DProof (Lean source)
lemma le_worstRisk {α : Type*} [SemilatticeSup α] (s : Finset Y) (hs : s.Nonempty) (R : Y → FiniteDesign Ω → α) (D : FiniteDesign Ω) {y : Y} (hy : y ∈ s) : R y D ≤ worstRisk s hs R D := Finset.le_sup' (fun y => R y D) hy -
bestRisk_lelemma — The best achievable risk is attained, hence no larger than the risk of any family member.hypothesesconclusionbestRisk 𝒟 hfin hne R y ≤ R y DProof (Lean source)
lemma bestRisk_le {α : Type*} [LinearOrder α] (𝒟 : DesignFamily Ω) (hfin : 𝒟.Finite) (hne : 𝒟.Nonempty) (R : Y → FiniteDesign Ω → α) (y : Y) {D : FiniteDesign Ω} (hD : D ∈ 𝒟) : bestRisk 𝒟 hfin hne R y ≤ R y D := (Classical.choose_spec (exists_isOptimalOn 𝒟 (R y) hfin hne)).2 D hD -
regret_nonneglemma — Regret is nonnegative for every member of the family.hypothesesconclusion0 ≤ regret 𝒟 hfin hne R y DProof (Lean source)
lemma regret_nonneg (𝒟 : DesignFamily Ω) (hfin : 𝒟.Finite) (hne : 𝒟.Nonempty) {α : Type*} [AddGroup α] [LinearOrder α] [AddRightMono α] (R : Y → FiniteDesign Ω → α) (y : Y) {D : FiniteDesign Ω} (hD : D ∈ 𝒟) : 0 ≤ regret 𝒟 hfin hne R y D := sub_nonneg.mpr (bestRisk_le 𝒟 hfin hne R y hD)
Neyman 3 core · 3 supporting Neyman allocation minimizes the two-arm variance proxy by assigning in proportion to standard deviations. ★ neyman_allocation_eq_at_fraction
Neyman allocation
Neyman allocation minimizes the two-arm variance proxy by assigning in proportion to standard deviations.
The definitions neymanFraction and neymanOptimalValue package the optimizer
sqrt A / (sqrt A + sqrt B) and the value (sqrt A + sqrt B)^2. Theorems
neyman_allocation_lower_bound, neyman_allocation_eq_at_fraction, and
neyman_allocation_isMinimizer prove the lower bound, show equality at the Neyman
fraction, and state the resulting minimization property on the interval (0, 1).
The Neyman-fraction formula: √A / (√A + √B), the treatment fraction that minimizes the two-arm variance A/x + B/(1−x) when the arm variances are positive.
Definition (Lean source)
The Neyman optimal-value formula: (√A + √B)², the minimized two-arm variance when the arm variances are positive.
Definition (Lean source)
Neyman allocation optimum. For nonnegative treated-arm and control-arm outcome variances A and B, evaluating the two-arm variance A/x + B/(1−x) at the Neyman fraction x* = √A/(√A+√B) yields exactly its lower bound (√A + √B)²; hence the Neyman fraction minimizes the variance over (0,1).
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
neyman_allocation_lower_boundtheorem — Neyman allocation lower bound. For nonnegative arm variances A, B and any treatment fraction x ∈ (0,1), the two-arm variance is at least (√A + √B)².hypothesesA B x :ℝhA :0 ≤ AhB :0 ≤ Bhx0 :0 < xhx1 :x < 1conclusionneymanOptimalValue A B ≤ A / x + B / (1 - x)Proof (Lean source)
theorem neyman_allocation_lower_bound {A B x : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hx0 : 0 < x) (hx1 : x < 1) : neymanOptimalValue A B ≤ A / x + B / (1 - x) := by -- A/x + B/(1−x) − (√A+√B)² = (√(A(1−x)/x) − √(Bx/(1−x)))² ≥ 0 (the cross term √(AB) cancels x). unfold neymanOptimalValue have hx1' : 0 < 1 - x := sub_pos.mpr hx1 have hxne : x ≠ 0 := ne_of_gt hx0 have h1xne : 1 - x ≠ 0 := ne_of_gt hx1' have hden : 0 < x * (1 - x) := mul_pos hx0 hx1' have hcommon : A / x + B / (1 - x) = (A * (1 - x) + B * x) / (x * (1 - x)) := by field_simp [hxne, h1xne] rw [hcommon] rw [le_div_iff₀ hden] have hsqA : sqrt A ^ 2 = A := Real.sq_sqrt hA have hsqB : sqrt B ^ 2 = B := Real.sq_sqrt hB nlinarith [sq_nonneg (sqrt A - (sqrt A + sqrt B) * x)] -
neymanFraction_mem_Iootheorem — The Neyman fraction lies in (0,1).Proof (Lean source)
theorem neymanFraction_mem_Ioo {A B : ℝ} (hA : 0 < A) (hB : 0 < B) : 0 < neymanFraction A B ∧ neymanFraction A B < 1 := by unfold neymanFraction have hs : 0 < sqrt A := Real.sqrt_pos.2 hA have ht : 0 < sqrt B := Real.sqrt_pos.2 hB constructor · exact div_pos hs (add_pos hs ht) · exact (div_lt_one (add_pos hs ht)).2 (lt_add_of_pos_right (sqrt A) ht) -
neyman_allocation_isMinimizertheorem — The Neyman fraction is a minimizer: its two-arm variance is no larger than the variance at any treatment fraction in (0,1).hypothesesA B :ℝhA :0 ≤ AhB :0 ≤ Bconclusion∀ xProof (Lean source)
theorem neyman_allocation_isMinimizer {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) : ∀ x, 0 < x → x < 1 → A / neymanFraction A B + B / (1 - neymanFraction A B) ≤ A / x + B / (1 - x) := by intro x hx0 hx1 rw [neyman_allocation_eq_at_fraction hA hB] exact neyman_allocation_lower_bound hA hB hx0 hx1