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.
For a finite assignment space, the design family is a set of candidate randomization designs defined on that common assignment space.
Definition (Lean source)
For a finite assignment space, an ordered risk scale, a risk criterion for randomization designs, and two randomization designs, the assertion that the first design weakly dominates the second means that its risk is no greater than the second design's risk.
Definition (Lean source)
For a finite assignment space, an ordered risk scale, a family of candidate randomization designs, a risk criterion, and a randomization design, the assertion that the design is optimal in the family means both that it belongs to the family and that its risk is no greater than the risk of every design in the family.
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)
For a finite assignment space, an estimator specified separately for each randomization design, and a real-valued target, the mean-squared-error risk function assigns to each design the mean squared error of that design's estimator about the target, evaluated under that design.
Definition (Lean source)
5 supporting declarations (lemmas, instances)
-
refllemma — Domination is reflexive: every design dominates itself.hypothesesconclusionDominates R D DProof (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.hypothesesΩ :sharedType u_1α :Type*Preorder α𝒟 :R :FiniteDesign Ω → αD₀ :h :IsOptimalOn 𝒟 R D₀D :hD :D ∈ 𝒟conclusionDominates 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.hypothesesconclusion0 ≤ mseRisk est μ DProof (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.
For a finite set of states of nature that is nonempty, a risk criterion indexed by states and randomization designs, and a randomization design, the worst-case risk is the largest risk incurred by that design as the state ranges over the given set, provided risk values admit pairwise least upper bounds.
Definition (Lean source)
For a family of randomization designs, a finite set of states of nature that is nonempty, a risk criterion indexed by states and randomization designs, and a candidate randomization design, the minimax condition holds precisely when the candidate belongs to the family and its worst-case risk over the state set is no greater than that of every design in the family, provided risk values admit pairwise least upper bounds.
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)
For a family of randomization designs that is finite and nonempty, a risk criterion indexed by states and randomization designs, and a state of nature, the best achievable risk is the least risk at that state among designs in the family, provided risk values are linearly ordered.
Definition (Lean source)
For a family of randomization designs that is finite and nonempty, a risk criterion indexed by states and randomization designs, a state of nature, and a randomization design, the design's regret is its risk at that state minus the least risk achievable there within the family, provided risk values form a linearly ordered additive group whose order is preserved by right addition.
Definition (Lean source)
3 supporting declarations (lemmas, instances)
-
le_worstRisklemma — The worst-case risk dominates the risk at every state in the family.hypothesesΩ :sharedType u_1Y :sharedType u_2α :Type*s :Finset Yhs :s.NonemptyR :Y → FiniteDesign Ω → αD :y :Yhy :y ∈ sconclusionR 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.hypothesesΩ :sharedType u_1Y :sharedType u_2α :Type*𝒟 :hfin :𝒟.Finitehne :𝒟.NonemptyR :Y → FiniteDesign Ω → αy :YD :hD :D ∈ 𝒟conclusionbestRisk 𝒟 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.hypothesesΩ :sharedType u_1Y :sharedType u_2𝒟 :hfin :𝒟.Finitehne :𝒟.Nonemptyα :R :Y → FiniteDesign Ω → αy :YD :hD :D ∈ 𝒟conclusion0 ≤ 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).
For a first real-valued input and a second real-valued input, the Neyman allocation fraction is . When the inputs are nonnegative arm variances, this is the ratio of the treated arm's standard deviation to the sum of the two arms' standard deviations.
For a first real-valued input and a second real-valued input, the Neyman optimal-value formula is . When the inputs are nonnegative arm variances, this is the squared sum of their standard deviations.
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).hypothesesA B :ℝhA :0 < AhB :0 < BProof (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 ≤ Bx :0 < xx < 1conclusionA / neymanFraction A B + B / (1 - neymanFraction A B) ≤ A / x + B / (1 - x)Proof (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