Stat.Minimax.FiniteSquaredLoss
Finite bounded decision problems: randomized designs, dependent finite observations, conditional mixing under squared loss, and an attaining minimax procedure with a least-favorable finite prior.
Core 11 core · 13 supporting This module defines the procedure, risk, Euclidean parameterization, and prior simplex used by the finite squared-loss minimax theorem. ★ risk_nonneg
Finite bounded squared-loss decision problems
This module defines the procedure, risk, Euclidean parameterization, and prior
simplex used by the finite squared-loss minimax theorem. Procedures use the
existing FiniteDesign type and dependent bounded decision rules.
structure Procedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
A procedure consists of a finite randomized design and, for every selected design and dependent observation, an action in the prescribed closed interval.
def risk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given state-specific observation likelihoods, a real target for each state, a bounded randomized procedure, and a state, the statewise squared-loss risk is the procedure-design-weighted sum of likelihood-weighted squared differences between the selected action and that state's target.
Definition (Lean source)
parameters
Theta :
Type u_1
R :
Type u_2
R → Type u_3
l :
ℝ
u :
ℝ
P :
Theta → ∀ r, X r → ℝ
tau :
Theta → ℝ
q :
Procedure X l u
theta :
Theta
def
risk P tau q theta :
ℝ
given by
∑ r, q.design.p r * ∑ x, P theta r x * ((q.decision r x : ℝ) - tau theta) ^ 2
theorem risk_nonneg reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
When the likelihood coefficients are nonnegative, every bounded finite procedure has nonnegative squared-loss risk in each state.
Formal statement
Proof (Lean source)
theorem risk_nonneg (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ)
(hP : ∀ theta r x, 0 ≤ P theta r x) (q : Procedure X l u) (theta : Theta) :
0 ≤ risk P tau q theta := by
-- Expand both finite sums and use nonnegativity of the design mass, `P`, and squares.
unfold risk
apply sum_nonneg
intro r _
apply mul_nonneg (q.design.p_nonneg r)
apply sum_nonneg
intro x _
exact mul_nonneg (hP theta r x) (sq_nonneg _)
abbrev Ambient reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a set of design indices and an observation space for each design index, the ambient coordinate space consists of one real design-weight vector and one real action coordinate for every design-index and observation pair.
Definition (Lean source)
parameters
R :
Type*
X :
R → Type*
def
given by
(R → ℝ) × (∀ r, X r → ℝ)
def procedureSet reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a family of finite observation spaces indexed by design, a lower action bound, and an upper action bound, the feasible procedure-coordinate set contains exactly those ambient coordinates whose design weights form a probability distribution and whose action coordinates all lie in the closed interval from the lower to the upper bound.
Definition (Lean source)
parameters
R :
Type u_2
X :
R → Type*
l u :
ℝ
given by
{z | z.1 ∈ stdSimplex ℝ R ∧ ∀ r x, z.2 r x ∈ Icc l u}
def toAmbient reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Procedure
Given a bounded finite randomized procedure, its ambient Euclidean coordinates are its design probabilities together with its action at every design-index and observation pair.
def ofAmbient reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Procedure
Given an ambient coordinate point that belongs to the feasible procedure-coordinate set, the corresponding bounded finite procedure uses its design-weight coordinates as design probabilities and its action coordinates as bounded decisions.
Definition (Lean source)
parameters
R :
Type u_2
R → Type u_3
l :
ℝ
u :
ℝ
z :
Ambient R X
hz :
z ∈ procedureSet X l u
def
given by
clause 1
design := { p := z.1 p_nonneg := hz.1.1 p_sum := hz.1.2 }
clause 2
decision := fun r x ↦ ⟨z.2 r x, hz.2 r x⟩
def rawRisk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given state-specific observation likelihoods, a real target for each state, an ambient coordinate point, and a state, the raw squared-loss risk is the design-coordinate-weighted sum of likelihood-weighted squared differences between action coordinates and that state's target.
Definition (Lean source)
parameters
Theta :
Type u_1
R :
Type u_2
R → Type u_3
P :
Theta → ∀ r, X r → ℝ
tau :
Theta → ℝ
z :
Ambient R X
theta :
Theta
def
rawRisk P tau z theta :
ℝ
given by
∑ r, z.1 r * ∑ x, P theta r x * (z.2 r x - tau theta) ^ 2
def riskVector reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given state-specific observation likelihoods, a real target for each state, and an ambient coordinate point, the risk vector assigns to every state its raw squared-loss risk at that coordinate point.
def finiteDesignOfSimplex reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a vector of weights over the finite state space that belongs to the standard probability simplex, the corresponding finite design is the probability design whose mass function is that vector.
Definition (Lean source)
parameters
Theta :
Type u_1
Theta → ℝ
hw :
w ∈ stdSimplex ℝ Theta
def
given by
clause 1
p := w
clause 2
p_nonneg := hw.1
clause 3
p_sum := hw.2
def bayesPayoff reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a real-valued risk vector over states and a vector of prior weights, the finite Bayes payoff is the sum over states of each prior weight times its risk-vector value.
13 supporting declarations (lemmas, instances)
-
procedure_nonemptytheorem — A nonempty design space and a nonempty action interval have a bounded finite randomized procedure, even when some observation spaces are empty.hypothesesR :sharedType u_2R → Type u_3Nonempty Rl u :ℝhlu :l ≤ uconclusionNonempty (Procedure X l u)Proof (Lean source)
theorem procedure_nonempty [Nonempty R] {l u : ℝ} (hlu : l ≤ u) : Nonempty (Procedure X l u) := by -- Put unit mass at one chosen design point and use the constant action `l`. classical let r₀ : R := choice inferInstance refine ⟨{ design := { p := single r₀ 1 p_nonneg := fun r ↦ by simp only [Pi.single_apply]; split_ifs <;> positivity p_sum := by simp } decision := fun _ _ ↦ ⟨l, le_rfl, hlu⟩ }⟩ -
toAmbient_memtheorem — The Euclidean coordinates of every bounded finite procedure belong to the feasible coordinate set.hypothesesconclusionq.toAmbient ∈ procedureSet X l uProof (Lean source)
theorem Procedure.toAmbient_mem (q : Procedure X l u) : q.toAmbient ∈ procedureSet X l u := by -- The two obligations are exactly the proof fields of `FiniteDesign` and `Icc`. exact ⟨⟨q.design.p_nonneg, q.design.p_sum⟩, fun r x ↦ (q.decision r x).property⟩ -
toAmbient_ofAmbienttheorem — Turning a feasible coordinate point into a procedure and back recovers that coordinate point.hypothesesR :sharedType u_2R → Type u_3l :sharedℝu :sharedℝz :Ambient R Xhz :z ∈ procedureSet X l uconclusion(Procedure.ofAmbient hz).toAmbient = zProof (Lean source)
@[simp] theorem Procedure.toAmbient_ofAmbient {z : Ambient R X} (hz : z ∈ procedureSet X l u) : (Procedure.ofAmbient hz).toAmbient = z := by rfl -
rawRisk_toAmbienttheorem — For given likelihood coefficients, the ambient polynomial representation of a procedure's risk equals its public squared-loss risk.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3l :sharedℝu :sharedℝP :Theta → ∀ r, X r → ℝtau :Theta → ℝq :Procedure X l utheta :Theta -
procedureSet_nonemptytheorem — A nonempty design space and a nonempty action interval make the feasible Euclidean procedure set nonempty.hypothesesR :sharedType u_2R → Type u_3Nonempty Rl u :ℝhlu :l ≤ uconclusion(procedureSet X l u).NonemptyProof (Lean source)
theorem procedureSet_nonempty [Nonempty R] {l u : ℝ} (hlu : l ≤ u) : (procedureSet X l u).Nonempty := by -- Map the witness from `procedure_nonempty` through `Procedure.toAmbient`. let q := choice (procedure_nonempty (X := X) hlu) exact ⟨q.toAmbient, q.toAmbient_mem⟩ -
convex_procedureSettheorem — An action interval with ordered endpoints makes the feasible Euclidean procedure set convex.hypothesesR :sharedType u_2R → Type u_3l u :ℝhlu :l ≤ uconclusionConvex ℝ (procedureSet X l u)Proof (Lean source)
theorem convex_procedureSet {l u : ℝ} (hlu : l ≤ u) : Convex ℝ (procedureSet X l u) := by -- Intersect the convex standard simplex with coordinatewise convex intervals. intro z hz w hw a b ha hb hab exact ⟨(convex_stdSimplex ℝ R) hz.1 hw.1 ha hb hab, fun r x ↦ (convex_Icc l u) (hz.2 r x) (hw.2 r x) ha hb hab⟩ -
isCompact_procedureSettheorem — The feasible Euclidean procedure set is compact: it is the product of a finite probability simplex and finitely many closed action intervals.Proof (Lean source)
theorem isCompact_procedureSet (l u : ℝ) : IsCompact (procedureSet X l u) := by -- View the set as a closed subset of the product of the compact simplex and finite Icc cube. have hcube : IsCompact {f : ∀ r, X r → ℝ | ∀ r x, f r x ∈ Icc l u} := by rw [show {f : ∀ r, X r → ℝ | ∀ r x, f r x ∈ Icc l u} = Set.univ.pi (fun r ↦ Set.univ.pi (fun _ : X r ↦ Icc l u)) by ext f constructor · intro hf rw [Set.mem_pi] intro r _ rw [Set.mem_pi] intro x _ exact hf r x · intro hf r x exact hf r (Set.mem_univ r) x (Set.mem_univ x)] exact isCompact_univ_pi (fun _ : R ↦ isCompact_univ_pi (fun _ ↦ (isCompact_Icc : IsCompact (Icc l u)))) rw [show procedureSet X l u = stdSimplex ℝ R ×ˢ {f : ∀ r, X r → ℝ | ∀ r x, f r x ∈ Icc l u} by ext z simp [procedureSet]] exact (isCompact_stdSimplex ℝ R).prod hcube -
continuous_rawRisktheorem — For fixed likelihood coefficients and targets, the ambient squared-loss risk in any state varies continuously with the procedure coordinates.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝtheta :ThetaconclusionProof (Lean source)
theorem continuous_rawRisk (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (theta : Theta) : Continuous (fun z : Ambient R X ↦ rawRisk P tau z theta) := by -- `fun_prop`/finite-sum continuity reduces this polynomial to coordinate projections. unfold rawRisk fun_prop -
continuous_riskVectortheorem — For fixed likelihood coefficients, the vector collecting each state's ambient squared-loss risk varies continuously with the procedure coordinates.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝconclusionContinuous (riskVector P tau : Ambient R X → Theta → ℝ)Proof (Lean source)
theorem continuous_riskVector (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) : Continuous (riskVector P tau : Ambient R X → Theta → ℝ) := by -- Use `continuous_pi` and `continuous_rawRisk` in each state coordinate. apply continuous_pi exact fun theta ↦ continuous_rawRisk P tau theta -
isCompact_riskVector_imagetheorem — Under given likelihood coefficients, the set of risk vectors attainable by feasible finite procedures is compact.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝconclusionProof (Lean source)
theorem isCompact_riskVector_image (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (l u : ℝ) : IsCompact (riskVector P tau '' procedureSet X l u) := by -- Continuous image of `isCompact_procedureSet`. exact (isCompact_procedureSet (X := X) l u).image (continuous_riskVector P tau) -
finiteDesign_mem_stdSimplextheorem — Every finite randomized design has a mass function in the standard probability simplex.Proof (Lean source)
theorem finiteDesign_mem_stdSimplex (nu : FiniteDesign Theta) : nu.p ∈ stdSimplex ℝ Theta := by exact ⟨nu.p_nonneg, nu.p_sum⟩ -
bayesPayoff_eq_Etheorem — Pairing a risk vector with a finite prior equals that prior's existing finite-design expectation.hypothesesconclusionbayesPayoff z nu.p = nu.E zProof (Lean source)
@[simp] theorem bayesPayoff_eq_E (z : Theta → ℝ) (nu : FiniteDesign Theta) : bayesPayoff z nu.p = nu.E z := by rfl -
continuous_bayesPayofftheorem — The finite Bayes payoff varies continuously with both the risk vector and the prior weights.hypothesesTheta :sharedType u_1conclusionContinuous (fun p : (Theta → ℝ) × (Theta → ℝ) ↦ bayesPayoff p.1 p.2)Proof (Lean source)
theorem continuous_bayesPayoff : Continuous (fun p : (Theta → ℝ) × (Theta → ℝ) ↦ bayesPayoff p.1 p.2) := by -- Finite sum of products of continuous coordinate projections. unfold bayesPayoff fun_prop
Mixing 3 core · 4 supporting This module proves the conditional Jensen step that turns mixtures of finite procedures back into an ordinary randomized design with a bounded decision rule. ★ risk_mixProcedure_le
Conditional mixing and convexified finite risk sets
This module proves the conditional Jensen step that turns mixtures of finite procedures back into an ordinary randomized design with a bounded decision rule. It then packages the compact convex risk set used by Sion's theorem.
def mixProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a finite set of design points, a finite observation set at each design point, ordered action bounds, a mixing weight no smaller than zero, the same weight no larger than one, and two feasible randomized procedures, the mixed feasible randomized procedure assigns the convex combination of their design masses at each design point. At a point with positive mixed mass it averages their actions using the corresponding posterior mixture weights, and at a point with zero mixed mass it uses the lower action bound.
Definition (Lean source)
parameters
R :
Type u_2
R → Type u_3
l u t :
ℝ
hlu :
l ≤ u
ht0 :
0 ≤ t
ht1 :
t ≤ 1
q₀ q₁ :
Procedure X l u
def
given by
by let p : R → ℝ := fun r ↦ t * q₀.design.p r
+ (1 - t) * q₁.design.p r refine { design := { p := p p_nonneg := ?_ p_sum := ?_ } decision := ?_ } · intro r exact add_nonneg (mul_nonneg ht0 (q₀.design.p_nonneg r)) (mul_nonneg (sub_nonneg.mpr ht1) (q₁.design.p_nonneg r)) · simp only [p, Finset.sum_add_distrib, ← Finset.mul_sum] rw [q₀.design.p_sum, q₁.design.p_sum] ring · intro r x by_cases hp : p r
= 0 · exact ⟨l, le_rfl, hlu⟩ · let a₀ := t * q₀.design.p r / p r let a₁ := (1 - t) * q₁.design.p r / p r refine ⟨a₀ * (q₀.decision r x : ℝ)
+ a₁ * (q₁.decision r x : ℝ), ?_, ?_⟩ · have hp_nonneg : 0
≤ p r := add_nonneg (mul_nonneg ht0 (q₀.design.p_nonneg r)) (mul_nonneg (sub_nonneg.mpr ht1) (q₁.design.p_nonneg r)) have ha₀ : 0 ≤ a₀ := div_nonneg (mul_nonneg ht0 (q₀.design.p_nonneg r)) hp_nonneg have ha₁ : 0 ≤ a₁ := div_nonneg (mul_nonneg (sub_nonneg.mpr ht1) (q₁.design.p_nonneg r)) hp_nonneg have ha_sum : a₀
+ a₁ = 1 := by simp only [a₀, a₁, ← add_div] exact div_self hp calc l = a₀ * l
+ a₁ * l := by rw [← add_mul, ha_sum, one_mul] _ ≤ a₀ * (q₀.decision r x : ℝ)
+ a₁ * (q₁.decision r x : ℝ) := add_le_add (mul_le_mul_of_nonneg_left (q₀.decision r x).property.1 ha₀) (mul_le_mul_of_nonneg_left (q₁.decision r x).property.1 ha₁) · have hp_nonneg : 0
≤ p r := add_nonneg (mul_nonneg ht0 (q₀.design.p_nonneg r)) (mul_nonneg (sub_nonneg.mpr ht1) (q₁.design.p_nonneg r)) have ha₀ : 0 ≤ a₀ := div_nonneg (mul_nonneg ht0 (q₀.design.p_nonneg r)) hp_nonneg have ha₁ : 0 ≤ a₁ := div_nonneg (mul_nonneg (sub_nonneg.mpr ht1) (q₁.design.p_nonneg r)) hp_nonneg have ha_sum : a₀
+ a₁
= 1 := by simp only [a₀, a₁, ← add_div] exact div_self hp calc a₀ * (q₀.decision r x : ℝ)
+ a₁ * (q₁.decision r x : ℝ) ≤ a₀ * u
+ a₁ * u := add_le_add (mul_le_mul_of_nonneg_left (q₀.decision r x).property.2 ha₀) (mul_le_mul_of_nonneg_left (q₁.decision r x).property.2 ha₁) _
= u := by rw [← add_mul, ha_sum, one_mul]
theorem risk_mixProcedure_le reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
With nonnegative likelihood coefficients, an ordered action interval, and a mixing weight between zero and one, conditional mixing produces a procedure whose statewise squared-loss risk is no greater than the corresponding mixture of the two original risks. No normalization of the coefficients is required.
Formal statement
hypotheses
Theta :
Type u_1
R :
Type u_2
R → Type u_3
P :
Theta → ∀ r, X r → ℝ
tau :
Theta → ℝ
hP :
∀ theta r x, 0 ≤ P theta r x
l u t :
ℝ
hlu :
l ≤ u
ht0 :
0 ≤ t
ht1 :
t ≤ 1
q₀ q₁ :
Procedure X l u
theta :
Theta
conclusion
risk P tau (mixProcedure hlu ht0 ht1 q₀ q₁) theta
Proof (Lean source)
theorem risk_mixProcedure_le
(P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ)
(hP : ∀ theta r x, 0 ≤ P theta r x)
{l u t : ℝ} (hlu : l ≤ u) (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
(q₀ q₁ : Procedure X l u) (theta : Theta) :
risk P tau (mixProcedure hlu ht0 ht1 q₀ q₁) theta ≤
t * risk P tau q₀ theta + (1 - t) * risk P tau q₁ theta := by
/- Split on each mixed design mass. At positive mass, clear its denominator and
use the two-point squared-loss identity/Jensen inequality. At zero mass,
nonnegativity forces both weighted component masses to vanish. Multiply the
pointwise inequality by `P ≥ 0` and sum first over observations, then designs. -/
classical
unfold risk
rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
apply Finset.sum_le_sum
intro r _
let m₀ : ℝ := t * q₀.design.p r
let m₁ : ℝ := (1 - t) * q₁.design.p r
let p : ℝ := m₀ + m₁
have hm₀ : 0 ≤ m₀ := mul_nonneg ht0 (q₀.design.p_nonneg r)
have hm₁ : 0 ≤ m₁ := mul_nonneg (sub_nonneg.mpr ht1) (q₁.design.p_nonneg r)
have hp_nonneg : 0 ≤ p := add_nonneg hm₀ hm₁
by_cases hp_zero : p = 0
· have hm₀_zero : m₀ = 0 := by nlinarith
have hm₁_zero : m₁ = 0 := by nlinarith
change p * _ ≤
t * (q₀.design.p r * _) + (1 - t) * (q₁.design.p r * _)
rw [hp_zero, zero_mul, ← mul_assoc t, ← mul_assoc (1 - t),
show t * q₀.design.p r = 0 from hm₀_zero,
show (1 - t) * q₁.design.p r = 0 from hm₁_zero]
simp
· have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg (Ne.symm hp_zero)
have hdesign :
(mixProcedure hlu ht0 ht1 q₀ q₁).design.p r = p := by
rfl
rw [hdesign, Finset.mul_sum]
rw [← mul_assoc t, ← mul_assoc (1 - t), Finset.mul_sum, Finset.mul_sum,
← Finset.sum_add_distrib]
apply Finset.sum_le_sum
intro x _
have hdecision :
((mixProcedure hlu ht0 ht1 q₀ q₁).decision r x : ℝ) =
m₀ / p * (q₀.decision r x : ℝ) +
m₁ / p * (q₁.decision r x : ℝ) := by
simp [mixProcedure, p, m₀, m₁, hp_zero]
rw [hdecision]
have hid :
(m₀ / p * (q₀.decision r x : ℝ) +
m₁ / p * (q₁.decision r x : ℝ)) - tau theta =
(m₀ * ((q₀.decision r x : ℝ) - tau theta) +
m₁ * ((q₁.decision r x : ℝ) - tau theta)) / p := by
field_simp
simp only [p]
ring
have hjensen :
p * ((m₀ / p * (q₀.decision r x : ℝ) +
m₁ / p * (q₁.decision r x : ℝ)) - tau theta) ^ 2 ≤
m₀ * ((q₀.decision r x : ℝ) - tau theta) ^ 2 +
m₁ * ((q₁.decision r x : ℝ) - tau theta) ^ 2 := by
rw [hid, div_pow]
field_simp
simp only [p]
have hvar : 0 ≤ m₀ * m₁ *
(((q₀.decision r x : ℝ) - tau theta) -
((q₁.decision r x : ℝ) - tau theta)) ^ 2 :=
mul_nonneg (mul_nonneg hm₀ hm₁) (sq_nonneg _)
nlinarith [hvar]
calc
p * (P theta r x *
((m₀ / p * (q₀.decision r x : ℝ) +
m₁ / p * (q₁.decision r x : ℝ)) - tau theta) ^ 2) =
P theta r x * (p *
((m₀ / p * (q₀.decision r x : ℝ) +
m₁ / p * (q₁.decision r x : ℝ)) - tau theta) ^ 2) := by ring
_ ≤ P theta r x *
(m₀ * ((q₀.decision r x : ℝ) - tau theta) ^ 2 +
m₁ * ((q₁.decision r x : ℝ) - tau theta) ^ 2) :=
mul_le_mul_of_nonneg_left hjensen (hP theta r x)
_ = t * q₀.design.p r *
(P theta r x * ((q₀.decision r x : ℝ) - tau theta) ^ 2) +
(1 - t) * q₁.design.p r *
(P theta r x * ((q₁.decision r x : ℝ) - tau theta) ^ 2) := by
simp only [m₀, m₁]
ring
def dominatedRiskVectors reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a parameter space, a finite set of design points, a finite observation set at each design point, likelihood coefficients, a target value for each parameter, and two action bounds, the set of dominated risk vectors consists of exactly those real-valued functions on the parameter space for which there exists a feasible finite randomized procedure whose squared-loss risk is no greater at every parameter.
4 supporting declarations (lemmas, instances)
-
convex_dominatedRiskVectorstheorem — With nonnegative likelihood coefficients and an ordered action interval, the set of risk vectors dominated by an ordinary finite procedure is convex.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝhlu :l ≤ uconclusionConvex ℝ (dominatedRiskVectors P tau l u)Proof (Lean source)
theorem convex_dominatedRiskVectors (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (hP : ∀ theta r x, 0 ≤ P theta r x) {l u : ℝ} (hlu : l ≤ u) : Convex ℝ (dominatedRiskVectors P tau l u) := by -- Unpack two witnessing procedures and use `mixProcedure` plus `risk_mixProcedure_le`. intro z hz w hw a b ha hb hab rcases hz with ⟨q₀, hq₀⟩ rcases hw with ⟨q₁, hq₁⟩ have ha1 : a ≤ 1 := by nlinarith refine ⟨mixProcedure hlu ha ha1 q₀ q₁, ?_⟩ intro theta calc risk P tau (mixProcedure hlu ha ha1 q₀ q₁) theta ≤ a * risk P tau q₀ theta + (1 - a) * risk P tau q₁ theta := risk_mixProcedure_le P tau hP hlu ha ha1 q₀ q₁ theta _ ≤ a * z theta + (1 - a) * w theta := add_le_add (mul_le_mul_of_nonneg_left (hq₀ theta) ha) (mul_le_mul_of_nonneg_left (hq₁ theta) (sub_nonneg.mpr ha1)) _ = (a • z + b • w) theta := by have hb_eq : b = 1 - a := by linarith simp [hb_eq] -
riskVector_image_subset_dominatedtheorem — Under given likelihood coefficients, every risk vector attained by feasible ambient coordinates is dominated by the risk of the associated ordinary finite procedure.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝconclusionProof (Lean source)
theorem riskVector_image_subset_dominated (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (l u : ℝ) : riskVector P tau '' procedureSet X l u ⊆ dominatedRiskVectors P tau l u := by -- Convert the feasible preimage point with `Procedure.ofAmbient`; risks agree definitionally. rintro z ⟨y, hy, rfl⟩ refine ⟨Procedure.ofAmbient hy, ?_⟩ intro theta rw [← rawRisk_toAmbient] rw [Procedure.toAmbient_ofAmbient] rfl -
exists_procedure_risk_le_of_mem_convexHulltheorem — With nonnegative likelihood coefficients and an ordered action interval, every convex combination of attainable risk vectors is coordinatewise dominated by the risk vector of an ordinary finite procedure.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝhlu :l ≤ uz :Theta → ℝhz :Proof (Lean source)
theorem exists_procedure_risk_le_of_mem_convexHull (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (hP : ∀ theta r x, 0 ≤ P theta r x) {l u : ℝ} (hlu : l ≤ u) {z : Theta → ℝ} (hz : z ∈ convexHull ℝ (riskVector P tau '' procedureSet X l u)) : ∃ q : Procedure X l u, ∀ theta, risk P tau q theta ≤ z theta := by -- Apply `convexHull_min` to the convex dominated set and the attainable-image inclusion. exact (convexHull_min (riskVector_image_subset_dominated P tau l u) (convex_dominatedRiskVectors P tau hP hlu)) hz -
isCompact_convexHull_riskVectorstheorem — Under given likelihood coefficients, the convex hull of the attainable finite risk vectors is compact.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3P :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝconclusionProof (Lean source)
theorem isCompact_convexHull_riskVectors (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (l u : ℝ) : IsCompact (convexHull ℝ (riskVector P tau '' procedureSet X l u)) := by /- Carathéodory bounds every representation by `card Theta + 1` points. After padding shorter representations with zero-weight copies of a fixed source point, the hull is the continuous barycenter image of a compact power of the source times a standard simplex. -/ classical let s : Set (Theta → ℝ) := riskVector P tau '' procedureSet X l u have hs : IsCompact s := isCompact_riskVector_image P tau l u by_cases hs_empty : s = ∅ · simp [s, hs_empty] have hs_nonempty : s.Nonempty := Set.nonempty_iff_ne_empty.mpr hs_empty let z₀ : Theta → ℝ := hs_nonempty.some have hz₀ : z₀ ∈ s := hs_nonempty.some_mem let n := card Theta + 1 let A : Set ((Fin n → Theta → ℝ) × (Fin n → ℝ)) := {p | (∀ i, p.1 i ∈ s) ∧ p.2 ∈ stdSimplex ℝ (Fin n)} have hpoints : IsCompact {z : Fin n → Theta → ℝ | ∀ i, z i ∈ s} := by rw [show {z : Fin n → Theta → ℝ | ∀ i, z i ∈ s} = Set.univ.pi (fun _ ↦ s) by ext z; simp] exact isCompact_univ_pi (fun _ ↦ hs) have hA : IsCompact A := by rw [show A = {z : Fin n → Theta → ℝ | ∀ i, z i ∈ s} ×ˢ stdSimplex ℝ (Fin n) by ext p; simp [A]] exact hpoints.prod (isCompact_stdSimplex ℝ (Fin n)) have hbarycenter : Continuous (fun p : (Fin n → Theta → ℝ) × (Fin n → ℝ) ↦ ∑ i, p.2 i • p.1 i) := by fun_prop have himage : IsCompact ((fun p : (Fin n → Theta → ℝ) × (Fin n → ℝ) ↦ ∑ i, p.2 i • p.1 i) '' A) := hA.image hbarycenter convert himage using 1 ext x constructor · intro hx rw [convexHull_eq_union] at hx simp only [exists_prop, Set.mem_iUnion] at hx obtain ⟨t, hts, ht_ind, hxt⟩ := hx rw [Finset.mem_convexHull'] at hxt obtain ⟨w, hw_nonneg, hw_sum, hw_center⟩ := hxt have ht_card : card t ≤ n := by calc card t ≤ finrank ℝ (vectorSpan ℝ (range ((↑) : t → Theta → ℝ))) + 1 := ht_ind.card_le_finrank_succ _ ≤ finrank ℝ (Theta → ℝ) + 1 := Nat.add_le_add_right (Submodule.finrank_le _) 1 _ = n := by simp [n] let e : t ↪ Fin n := choice (Function.Embedding.nonempty_of_card_le (by simpa using ht_card)) let w' : Fin n → ℝ := Function.extend e (fun i ↦ w i) (fun _ ↦ 0) let z' : Fin n → Theta → ℝ := Function.extend e (fun i ↦ (i : Theta → ℝ)) (fun _ ↦ z₀) have hz' : ∀ i, z' i ∈ s := by intro i by_cases hi : i ∈ range e · obtain ⟨j, rfl⟩ := hi rw [show z' (e j) = (j : Theta → ℝ) by simp [z', e.injective.extend_apply]] exact hts j.property · simpa [z', Function.extend_apply' _ _ _ hi] using hz₀ have hw'_nonneg : ∀ i, 0 ≤ w' i := by intro i by_cases hi : i ∈ range e · obtain ⟨j, rfl⟩ := hi simpa [w', e.injective.extend_apply] using hw_nonneg j j.property · simp [w', Function.extend_apply' _ _ _ hi] have hw'_sum : ∑ i, w' i = 1 := by calc ∑ i, w' i = ∑ i ∈ Finset.univ.map e, w' i := by symm apply Finset.sum_subset (by simp) intro i _ hi have hi' : i ∉ range e := by simpa using hi simp [w', Function.extend_apply' _ _ _ hi'] _ = ∑ i : t, w i := by simp [w', e.injective.extend_apply] _ = 1 := by rw [← hw_sum] exact (Finset.sum_subtype t (fun _ ↦ Iff.rfl) w).symm have hcenter : ∑ i, w' i • z' i = x := by calc ∑ i, w' i • z' i = ∑ i ∈ Finset.univ.map e, w' i • z' i := by symm apply Finset.sum_subset (by simp) intro i _ hi have hi' : i ∉ range e := by simpa using hi simp [w', Function.extend_apply' _ _ _ hi'] _ = ∑ i : t, w i • (i : Theta → ℝ) := by simp [w', z', e.injective.extend_apply] _ = x := by rw [← hw_center] exact (Finset.sum_subtype t (fun _ ↦ Iff.rfl) (fun y ↦ w y • y)).symm exact ⟨(z', w'), ⟨hz', ⟨hw'_nonneg, hw'_sum⟩⟩, hcenter⟩ · rintro ⟨p, hp, rfl⟩ exact mem_convexHull_of_exists_fintype p.2 p.1 hp.2.1 hp.2.2 hp.1 rfl
PosteriorBarycenter 9 core · 16 supporting This module provides posterior-residual minimax lower bounds and conditional-barycenter minimax upper bounds for finite experiments whose observation type depends on the chosen design index. ★ sInf_posteriorResidual_le_minimaxValue★ minimaxValue_le_of_randomizedGridRisk
Posterior and barycenter bounds for dependent finite squared loss
This module provides posterior-residual minimax lower bounds and conditional-barycenter minimax upper bounds for finite experiments whose observation type depends on the chosen design index. Null predictive and design fibers are handled by guarded definitions, without full-support assumptions.
structure Model reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
A dependent finite experiment assigns, at every state and design index, a nonnegative normalized mass function on that design's observation type, together with a real target.
Definition (Lean source)
parameters
fields
The observation likelihood at a state and design index.
P :
Theta → ∀ b, X b → ℝ
Every likelihood coefficient is nonnegative.
At every state and design index, the likelihood coefficients sum to one.
The real estimand attached to each state.
tau :
Theta → ℝ
def predictiveMass reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Model
Given a dependent finite experiment, a prior probability design over states, a design index, and an observation in that design's observation space, the prior predictive mass is the sum over states of prior probability times the conditional probability of that observation.
Definition (Lean source)
parameters
Theta :
Type u_1
B :
Type u_2
B → Type u_3
M :
Model Theta B X
nu :
FiniteDesign Theta
b :
B
x :
X b
def
predictiveMass M nu b x :
ℝ
def predictiveTarget reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Model
Given a dependent finite experiment, a prior probability design over states, a design index, and an observation in that design's observation space, the predictive target numerator is the sum over states of prior probability times observation likelihood times the state's target.
def posteriorMean reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Model
Given a dependent finite experiment, a prior probability design over states, a design index, and an observation in that design's observation space, the guarded posterior mean is the predictive target numerator divided by predictive mass when that mass is nonzero, and is zero when it is zero.
Definition (Lean source)
parameters
Theta :
Type u_1
B :
Type u_2
B → Type u_3
M :
Model Theta B X
nu :
FiniteDesign Theta
b :
B
x :
X b
def
posteriorMean M nu b x :
ℝ
given by
if M.predictiveMass nu b x
= 0 then 0 else M.predictiveTarget nu b x / M.predictiveMass nu b x
def posteriorResidual reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Model
Given a dependent finite experiment, a prior probability design over states, and a design index, the posterior residual is the sum, over states and observations, of prior probability times observation likelihood times squared deviation of the guarded posterior mean from the state's target.
theorem sInf_posteriorResidual_le_minimaxValue reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Model
An ordered action interval makes the least design-specific posterior residual a lower bound on the dependent experiment's bounded squared-loss minimax value.
Formal statement
hypotheses
Theta :
Type u_1
B :
Type u_2
B → Type u_3
Nonempty Theta
Nonempty B
M :
Model Theta B X
nu :
FiniteDesign Theta
l u :
ℝ
hlu :
l ≤ u
conclusion
≤ minimaxValue (risk (l := l) (u := u) M.P M.tau)
Proof (Lean source)
theorem Model.sInf_posteriorResidual_le_minimaxValue [Nonempty Theta] [Nonempty B]
(M : Model Theta B X) (nu : FiniteDesign Theta) {l u : ℝ} (hlu : l ≤ u) :
sInf (range (M.posteriorResidual nu)) ≤
minimaxValue (risk (l := l) (u := u) M.P M.tau) := by
let _ : Nonempty (Procedure X l u) := procedure_nonempty hlu
apply le_minimaxValue
intro q
calc
sInf (range (M.posteriorResidual nu)) ≤
∑ theta, nu.p theta * risk M.P M.tau q theta :=
M.sInf_posteriorResidual_le_priorRisk nu q
_ ≤ ∑ theta, nu.p theta *
worstCaseRisk (risk M.P M.tau) q := by
apply Finset.sum_le_sum
intro theta _
exact mul_le_mul_of_nonneg_left
(le_worstCaseRisk
(Finite.bddAbove_range (risk M.P M.tau q)) theta) (nu.p_nonneg theta)
_ = worstCaseRisk (risk M.P M.tau) q := by
rw [← Finset.sum_mul, nu.p_sum, one_mul]
def conditionalBarycenter reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a probability design over design indices, grid weights for each design index, observation, and grid action, real grid actions, a default action, a design index, and an observation in that design's observation space, the guarded conditional barycenter is the weighted average of grid actions divided by that design's probability when it is positive, and is the default action when it is zero.
Definition (Lean source)
parameters
B :
Type u_5
G :
Type u_6
X :
B → Type u_7
pi :
w :
∀ b
if
X b
and
G
then
ℝ
gamma :
G → ℝ
d :
ℝ
b :
B
x :
X b
def
conditionalBarycenter pi w gamma d b x :
ℝ
given by
if pi.p b = 0 then d else (∑ g, gamma g * w b x g) / pi.p b
def barycenterProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Given a probability design over design indices, grid weights, real grid actions, a default action, nonnegative grid weights, weights that sum to the corresponding design probability, a default action in the closed interval from to , and grid actions all in that interval, the barycenter procedure is the bounded finite procedure using that design and the guarded conditional barycenter as its decision rule.
Definition (Lean source)
parameters
B :
Type u_5
G :
Type u_6
X :
B → Type u_7
pi :
∀ b, Fintype (X b)
w :
∀ b
if
X b
and
G
then
ℝ
gamma :
G → ℝ
d :
ℝ
hw :
∀ b x g, 0 ≤ w b x g
hocc :
∀ b x, ∑ g, w b x g = pi.p b
l u :
ℝ
hd :
d ∈ Icc l u
hgamma :
∀ g, gamma g ∈ Icc l u
def
given by
clause 1
design := pi
clause 2
decision b x := ⟨conditionalBarycenter pi w gamma d b x, conditionalBarycenter_mem_Icc pi w gamma d hw hocc hd hgamma b x⟩
theorem minimaxValue_le_of_randomizedGridRisk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss.Model
Nonnegative grid weights that sum to each design probability, with the null-fiber default inside the action interval, all grid actions inside that interval, and randomized grid-action risk uniformly bounded across states, imply the dependent experiment's bounded squared-loss minimax value is no greater than that bound.
Formal statement
hypotheses
Theta :
Type u_4
B :
Type u_5
G :
Type u_6
X :
B → Type u_7
Nonempty Theta
∀ b, Fintype (X b)
M :
Model Theta B X
pi :
w :
∀ b
if
X b
and
G
then
ℝ
gamma :
G → ℝ
d :
ℝ
hw :
∀ b x g, 0 ≤ w b x g
hocc :
∀ b x, ∑ g, w b x g = pi.p b
l u c :
ℝ
hd :
d ∈ Icc l u
hgamma :
∀ g, gamma g ∈ Icc l u
conclusion
minimaxValue (risk (l := l) (u := u) M.P M.tau) ≤ c
Proof (Lean source)
theorem Model.minimaxValue_le_of_randomizedGridRisk [Nonempty Theta]
[∀ b, Fintype (X b)] (M : Model Theta B X) (pi : FiniteDesign B)
(w : ∀ b, X b → G → ℝ) (gamma : G → ℝ) (d : ℝ)
(hw : ∀ b x g, 0 ≤ w b x g)
(hocc : ∀ b x, ∑ g, w b x g = pi.p b)
{l u c : ℝ} (hd : d ∈ Icc l u) (hgamma : ∀ g, gamma g ∈ Icc l u)
(hrisk : ∀ theta, ∑ b, ∑ x, ∑ g,
M.P theta b x * w b x g * (gamma g - M.tau theta) ^ 2 ≤ c) :
minimaxValue (risk (l := l) (u := u) M.P M.tau) ≤ c := by
let q : Procedure X l u :=
barycenterProcedure pi w gamma d hw hocc hd hgamma
calc
minimaxValue (risk (l := l) (u := u) M.P M.tau) ≤
worstCaseRisk (risk M.P M.tau) q :=
minimaxValue_le_worstCaseRisk_of_nonneg
(fun q' theta => risk_nonneg M.P M.tau M.P_nonneg q' theta) q
_ ≤ c := worstCaseRisk_le fun theta =>
(M.risk_barycenterProcedure_le pi w gamma d hw hocc hd hgamma theta).trans
(hrisk theta)
16 supporting declarations (lemmas, instances)
-
sum_predictiveMasstheorem — The prior predictive probabilities within a fixed design sum to one.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :Bconclusion∑ x, M.predictiveMass nu b x = 1Proof (Lean source)
theorem Model.sum_predictiveMass (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) : ∑ x, M.predictiveMass nu b x = 1 := by classical unfold Model.predictiveMass rw [Finset.sum_comm] simp_rw [← Finset.mul_sum, M.P_sum, mul_one] exact nu.p_sum -
predictiveMass_nonnegtheorem — Every prior predictive probability is nonnegative.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :Bx :X bconclusion0 ≤ M.predictiveMass nu b xProof (Lean source)
theorem Model.predictiveMass_nonneg (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) (x : X b) : 0 ≤ M.predictiveMass nu b x := by exact sum_nonneg fun theta _ => mul_nonneg (nu.p_nonneg theta) (M.P_nonneg theta b x) -
joint_eq_zero_of_predictiveMass_eq_zerotheorem — A zero-mass predictive observation has zero joint probability in every state.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :BX bhx :M.predictiveMass nu b x = 0theta :Thetaconclusionnu.p theta * M.P theta b x = 0Proof (Lean source)
theorem Model.joint_eq_zero_of_predictiveMass_eq_zero (M : Model Theta B X) (nu : FiniteDesign Theta) {b : B} {x : X b} (hx : M.predictiveMass nu b x = 0) (theta : Theta) : nu.p theta * M.P theta b x = 0 := by classical have hsum : (∑ theta', nu.p theta' * M.P theta' b x) = 0 := by simpa [Model.predictiveMass] using hx exact (Finset.sum_eq_zero_iff_of_nonneg (fun theta' _ => mul_nonneg (nu.p_nonneg theta') (M.P_nonneg theta' b x))).mp hsum theta (Finset.mem_univ theta) -
predictiveTarget_eq_zero_of_predictiveMass_eq_zerotheorem — A zero-mass predictive observation has zero target-weighted joint probability.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :BX bhx :M.predictiveMass nu b x = 0conclusionM.predictiveTarget nu b x = 0Proof (Lean source)
theorem Model.predictiveTarget_eq_zero_of_predictiveMass_eq_zero (M : Model Theta B X) (nu : FiniteDesign Theta) {b : B} {x : X b} (hx : M.predictiveMass nu b x = 0) : M.predictiveTarget nu b x = 0 := by classical unfold Model.predictiveTarget apply Finset.sum_eq_zero intro theta _ rw [M.joint_eq_zero_of_predictiveMass_eq_zero nu hx theta, zero_mul] -
predictiveMass_mul_posteriorMeantheorem — Predictive probability times the guarded posterior mean equals the target-weighted joint probability, including for null observations.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :Bx :X bconclusionM.predictiveMass nu b x * M.posteriorMean nu b x = M.predictiveTarget nu b xProof (Lean source)
theorem Model.predictiveMass_mul_posteriorMean (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) (x : X b) : M.predictiveMass nu b x * M.posteriorMean nu b x = M.predictiveTarget nu b x := by classical by_cases hx : M.predictiveMass nu b x = 0 · rw [hx, zero_mul, M.predictiveTarget_eq_zero_of_predictiveMass_eq_zero nu hx] · rw [Model.posteriorMean, if_neg hx] exact mul_div_cancel₀ _ hx -
posteriorResidual_nonnegtheorem — Every design-specific posterior residual risk is nonnegative.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :Bconclusion0 ≤ M.posteriorResidual nu bProof (Lean source)
theorem Model.posteriorResidual_nonneg (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) : 0 ≤ M.posteriorResidual nu b := by unfold Model.posteriorResidual apply sum_nonneg intro theta _ apply mul_nonneg (nu.p_nonneg theta) exact sum_nonneg fun x _ => mul_nonneg (M.P_nonneg theta b x) (sq_nonneg _) -
squaredRisk_eq_posteriorResidual_addtheorem — The prior risk of any decision rule equals posterior residual risk plus its predictive-probability-weighted squared distance from the posterior mean.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :Bdelta :X b → ℝProof (Lean source)
theorem Model.squaredRisk_eq_posteriorResidual_add (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) (delta : X b → ℝ) : (∑ theta, nu.p theta * ∑ x, M.P theta b x * (delta x - M.tau theta) ^ 2) = M.posteriorResidual nu b + ∑ x, M.predictiveMass nu b x * (delta x - M.posteriorMean nu b x) ^ 2 := by classical calc (∑ theta, nu.p theta * ∑ x, M.P theta b x * (delta x - M.tau theta) ^ 2) = ∑ x, ∑ theta, nu.p theta * M.P theta b x * (delta x - M.tau theta) ^ 2 := by simp_rw [Finset.mul_sum, ← mul_assoc] rw [Finset.sum_comm] _ = (∑ x, ∑ theta, nu.p theta * M.P theta b x * (M.posteriorMean nu b x - M.tau theta) ^ 2) + ∑ x, M.predictiveMass nu b x * (delta x - M.posteriorMean nu b x) ^ 2 := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro x _ have hcenter : (∑ theta, nu.p theta * M.P theta b x * (M.posteriorMean nu b x - M.tau theta)) = 0 := by calc (∑ theta, nu.p theta * M.P theta b x * (M.posteriorMean nu b x - M.tau theta)) = ∑ theta, (nu.p theta * M.P theta b x * M.posteriorMean nu b x - nu.p theta * M.P theta b x * M.tau theta) := by apply Finset.sum_congr rfl intro theta _ ring _ = (∑ theta, nu.p theta * M.P theta b x) * M.posteriorMean nu b x - ∑ theta, nu.p theta * M.P theta b x * M.tau theta := by rw [Finset.sum_sub_distrib, Finset.sum_mul] change M.predictiveMass nu b x * M.posteriorMean nu b x - M.predictiveTarget nu b x = 0 rw [M.predictiveMass_mul_posteriorMean] exact sub_self _ -- Complete the square on this observation fiber; `hcenter` kills the cross term. calc (∑ theta, nu.p theta * M.P theta b x * (delta x - M.tau theta) ^ 2) = ∑ theta, (nu.p theta * M.P theta b x * (M.posteriorMean nu b x - M.tau theta) ^ 2 + nu.p theta * M.P theta b x * (delta x - M.posteriorMean nu b x) ^ 2 + (2 * (delta x - M.posteriorMean nu b x)) * (nu.p theta * M.P theta b x * (M.posteriorMean nu b x - M.tau theta))) := by apply Finset.sum_congr rfl intro theta _ ring _ = (∑ theta, nu.p theta * M.P theta b x * (M.posteriorMean nu b x - M.tau theta) ^ 2) + M.predictiveMass nu b x * (delta x - M.posteriorMean nu b x) ^ 2 := by rw [Finset.sum_add_distrib, Finset.sum_add_distrib, ← Finset.sum_mul, ← Finset.mul_sum, hcenter, mul_zero] simp [Model.predictiveMass] _ = M.posteriorResidual nu b + ∑ x, M.predictiveMass nu b x * (delta x - M.posteriorMean nu b x) ^ 2 := by congr 1 unfold Model.posteriorResidual simp_rw [Finset.mul_sum, ← mul_assoc] rw [Finset.sum_comm] -
squaredRisk_posteriorMeantheorem — The guarded posterior mean attains exactly the design-specific posterior residual risk.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :B -
posteriorResidual_le_squaredRisktheorem — The posterior residual risk is no greater than the prior squared-loss risk of any real decision rule for the same design.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :Bdelta :X b → ℝProof (Lean source)
theorem Model.posteriorResidual_le_squaredRisk (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) (delta : X b → ℝ) : M.posteriorResidual nu b ≤ ∑ theta, nu.p theta * ∑ x, M.P theta b x * (delta x - M.tau theta) ^ 2 := by rw [M.squaredRisk_eq_posteriorResidual_add] exact le_add_of_nonneg_right (sum_nonneg fun x _ => mul_nonneg (M.predictiveMass_nonneg nu b x) (sq_nonneg _)) -
iInf_squaredRisk_eq_posteriorResidualtheorem — The smallest prior squared-loss risk over all real decision rules for a fixed design equals its posterior residual risk.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3M :Model Theta B Xnu :FiniteDesign Thetab :BProof (Lean source)
theorem Model.iInf_squaredRisk_eq_posteriorResidual (M : Model Theta B X) (nu : FiniteDesign Theta) (b : B) : (⨅ delta : X b → ℝ, ∑ theta, nu.p theta * ∑ x, M.P theta b x * (delta x - M.tau theta) ^ 2) = M.posteriorResidual nu b := by have hb : BddBelow (Set.range fun delta : X b → ℝ => ∑ theta, nu.p theta * ∑ x, M.P theta b x * (delta x - M.tau theta) ^ 2) := by refine ⟨M.posteriorResidual nu b, ?_⟩ rintro _ ⟨delta, rfl⟩ exact M.posteriorResidual_le_squaredRisk nu b delta -- The posterior mean attains the universal lower bound. apply le_antisymm · calc (⨅ delta : X b → ℝ, ∑ theta, nu.p theta * ∑ x, M.P theta b x * (delta x - M.tau theta) ^ 2) ≤ ∑ theta, nu.p theta * ∑ x, M.P theta b x * (M.posteriorMean nu b x - M.tau theta) ^ 2 := ciInf_le hb (M.posteriorMean nu b) _ = M.posteriorResidual nu b := M.squaredRisk_posteriorMean nu b · exact le_ciInf fun delta => M.posteriorResidual_le_squaredRisk nu b delta -
sInf_posteriorResidual_le_priorRisktheorem — The least posterior residual across designs is no greater than the prior-average risk of any bounded dependent procedure.hypothesesTheta :sharedType u_1B :sharedType u_2B → Type u_3Nonempty BM :Model Theta B Xnu :FiniteDesign Thetal u :ℝq :Procedure X l uProof (Lean source)
theorem Model.sInf_posteriorResidual_le_priorRisk [Nonempty B] (M : Model Theta B X) (nu : FiniteDesign Theta) {l u : ℝ} (q : Procedure X l u) : sInf (range (M.posteriorResidual nu)) ≤ ∑ theta, nu.p theta * risk M.P M.tau q theta := by classical have hb : BddBelow (range (M.posteriorResidual nu)) := by refine ⟨0, ?_⟩ rintro _ ⟨b, rfl⟩ exact M.posteriorResidual_nonneg nu b have hs_le (b : B) : sInf (range (M.posteriorResidual nu)) ≤ M.posteriorResidual nu b := csInf_le hb ⟨b, rfl⟩ -- Average the per-design posterior inequality using the procedure's design law. calc sInf (range (M.posteriorResidual nu)) = ∑ b, q.design.p b * sInf (range (M.posteriorResidual nu)) := by rw [← Finset.sum_mul, q.design.p_sum, one_mul] _ ≤ ∑ b, q.design.p b * (∑ theta, nu.p theta * ∑ x, M.P theta b x * ((q.decision b x : ℝ) - M.tau theta) ^ 2) := by apply Finset.sum_le_sum intro b _ exact mul_le_mul_of_nonneg_left ((hs_le b).trans (M.posteriorResidual_le_squaredRisk nu b (fun x => (q.decision b x : ℝ)))) (q.design.p_nonneg b) _ = ∑ theta, nu.p theta * risk M.P M.tau q theta := by unfold risk simp_rw [Finset.mul_sum, ← mul_assoc] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro theta _ apply Finset.sum_congr rfl intro b _ apply Finset.sum_congr rfl intro x _ ring -
weight_eq_zero_of_designMass_eq_zerotheorem — Nonnegative grid weights that sum to the design probability are zero individually whenever that design has zero probability.hypothesesB :sharedType u_5G :sharedType u_6X :sharedB → Type u_7pi :w :∀ bifX bandGthenℝhw :∀ b x g, 0 ≤ w b x ghocc :∀ b x, ∑ g, w b x g = pi.p bb :Bhb :pi.p b = 0x :X bg :Gconclusionw b x g = 0Proof (Lean source)
theorem weight_eq_zero_of_designMass_eq_zero (pi : FiniteDesign B) (w : ∀ b, X b → G → ℝ) (hw : ∀ b x g, 0 ≤ w b x g) (hocc : ∀ b x, ∑ g, w b x g = pi.p b) {b : B} (hb : pi.p b = 0) (x : X b) (g : G) : w b x g = 0 := by classical have hsum : (∑ g', w b x g') = 0 := by rw [hocc b x, hb] exact (Finset.sum_eq_zero_iff_of_nonneg (fun g' _ => hw b x g')).mp hsum g (Finset.mem_univ g) -
conditionalBarycenter_mem_Icctheorem — Nonnegative grid weights that sum to the design probability, with the null-fiber default inside a closed interval and all grid actions inside that interval, produce a guarded conditional barycenter in the same interval.hypothesesB :sharedType u_5G :sharedType u_6X :sharedB → Type u_7pi :w :∀ bifX bandGthenℝgamma :G → ℝd :ℝhw :∀ b x g, 0 ≤ w b x ghocc :∀ b x, ∑ g, w b x g = pi.p bl u :ℝhd :d ∈ Icc l uhgamma :∀ g, gamma g ∈ Icc l ub :Bx :X bconclusionconditionalBarycenter pi w gamma d b x ∈ Icc l uProof (Lean source)
theorem conditionalBarycenter_mem_Icc (pi : FiniteDesign B) (w : ∀ b, X b → G → ℝ) (gamma : G → ℝ) (d : ℝ) (hw : ∀ b x g, 0 ≤ w b x g) (hocc : ∀ b x, ∑ g, w b x g = pi.p b) {l u : ℝ} (hd : d ∈ Icc l u) (hgamma : ∀ g, gamma g ∈ Icc l u) (b : B) (x : X b) : conditionalBarycenter pi w gamma d b x ∈ Icc l u := by classical by_cases hb : pi.p b = 0 · simpa [conditionalBarycenter, hb] using hd · have hbpos : 0 < pi.p b := lt_of_le_of_ne (pi.p_nonneg b) (Ne.symm hb) rw [conditionalBarycenter, if_neg hb] constructor · rw [le_div_iff₀ hbpos, ← hocc b x, Finset.mul_sum] exact Finset.sum_le_sum fun g _ => mul_le_mul_of_nonneg_right (hgamma g).1 (hw b x g) · rw [div_le_iff₀ hbpos, ← hocc b x, Finset.mul_sum] exact Finset.sum_le_sum fun g _ => mul_le_mul_of_nonneg_right (hgamma g).2 (hw b x g) -
designMass_mul_conditionalBarycenter_sq_letheorem — Nonnegative grid weights that sum to the design probability make design probability times the guarded barycenter's squared error no greater than the corresponding weighted grid-action squared error.hypothesesB :sharedType u_5G :sharedType u_6X :sharedB → Type u_7pi :w :∀ bifX bandGthenℝgamma :G → ℝd t :ℝhw :∀ b x g, 0 ≤ w b x ghocc :∀ b x, ∑ g, w b x g = pi.p bb :Bx :X bconclusionpi.p b * (conditionalBarycenter pi w gamma d b x - t) ^ 2≤ ∑ g, w b x g * (gamma g - t) ^ 2Proof (Lean source)
theorem designMass_mul_conditionalBarycenter_sq_le (pi : FiniteDesign B) (w : ∀ b, X b → G → ℝ) (gamma : G → ℝ) (d t : ℝ) (hw : ∀ b x g, 0 ≤ w b x g) (hocc : ∀ b x, ∑ g, w b x g = pi.p b) (b : B) (x : X b) : pi.p b * (conditionalBarycenter pi w gamma d b x - t) ^ 2 ≤ ∑ g, w b x g * (gamma g - t) ^ 2 := by classical by_cases hb : pi.p b = 0 · -- On a null fiber occupancy forces every nonnegative weight to vanish. simp [hb, conditionalBarycenter, weight_eq_zero_of_designMass_eq_zero pi w hw hocc hb] · have hmass : pi.p b * conditionalBarycenter pi w gamma d b x = ∑ g, gamma g * w b x g := by rw [conditionalBarycenter, if_neg hb, mul_div_cancel₀ _ hb] have hcenter : (∑ g, w b x g * (gamma g - conditionalBarycenter pi w gamma d b x)) = 0 := by calc (∑ g, w b x g * (gamma g - conditionalBarycenter pi w gamma d b x)) = ∑ g, (gamma g * w b x g - w b x g * conditionalBarycenter pi w gamma d b x) := by apply Finset.sum_congr rfl intro g _ ring _ = (∑ g, gamma g * w b x g) - (∑ g, w b x g) * conditionalBarycenter pi w gamma d b x := by rw [Finset.sum_sub_distrib, Finset.sum_mul] _ = 0 := by rw [hocc b x, ← hmass, sub_self] -- Expand around the weighted mean; the centered cross term is zero. have hsquare : (∑ g, w b x g * (gamma g - t) ^ 2) = pi.p b * (conditionalBarycenter pi w gamma d b x - t) ^ 2 + ∑ g, w b x g * (gamma g - conditionalBarycenter pi w gamma d b x) ^ 2 := by calc (∑ g, w b x g * (gamma g - t) ^ 2) = ∑ g, (w b x g * (gamma g - conditionalBarycenter pi w gamma d b x) ^ 2 + w b x g * (conditionalBarycenter pi w gamma d b x - t) ^ 2 + (2 * (conditionalBarycenter pi w gamma d b x - t)) * (w b x g * (gamma g - conditionalBarycenter pi w gamma d b x))) := by apply Finset.sum_congr rfl intro g _ ring _ = pi.p b * (conditionalBarycenter pi w gamma d b x - t) ^ 2 + ∑ g, w b x g * (gamma g - conditionalBarycenter pi w gamma d b x) ^ 2 := by rw [Finset.sum_add_distrib, Finset.sum_add_distrib, ← Finset.sum_mul, ← Finset.mul_sum, hcenter, mul_zero, add_zero, hocc b x] ring rw [hsquare] exact le_add_of_nonneg_right (sum_nonneg fun g _ => mul_nonneg (hw b x g) (sq_nonneg _)) -
conditionalBarycenter_risk_letheorem — Nonnegative grid weights that sum to each design probability make the statewise risk of the guarded conditional barycenter no greater than the randomized grid-action risk.hypothesesTheta :sharedType u_4B :sharedType u_5G :sharedType u_6M :Model Theta B Xpi :w :∀ bifX bandGthenℝgamma :G → ℝd :ℝhw :∀ b x g, 0 ≤ w b x ghocc :∀ b x, ∑ g, w b x g = pi.p btheta :Thetaconclusion∑ b, pi.p b * ∑ x, M.P theta b x * (conditionalBarycenter pi w gamma d b x - M.tau theta) ^ 2≤ ∑ b, ∑ x, ∑ g, M.P theta b x * w b x g * (gamma g - M.tau theta) ^ 2Proof (Lean source)
theorem Model.conditionalBarycenter_risk_le [∀ b, Fintype (X b)] (M : Model Theta B X) (pi : FiniteDesign B) (w : ∀ b, X b → G → ℝ) (gamma : G → ℝ) (d : ℝ) (hw : ∀ b x g, 0 ≤ w b x g) (hocc : ∀ b x, ∑ g, w b x g = pi.p b) (theta : Theta) : ∑ b, pi.p b * ∑ x, M.P theta b x * (conditionalBarycenter pi w gamma d b x - M.tau theta) ^ 2 ≤ ∑ b, ∑ x, ∑ g, M.P theta b x * w b x g * (gamma g - M.tau theta) ^ 2 := by classical calc (∑ b, pi.p b * ∑ x, M.P theta b x * (conditionalBarycenter pi w gamma d b x - M.tau theta) ^ 2) = ∑ b, ∑ x, M.P theta b x * (pi.p b * (conditionalBarycenter pi w gamma d b x - M.tau theta) ^ 2) := by apply Finset.sum_congr rfl intro b _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro x _ ring _ ≤ ∑ b, ∑ x, M.P theta b x * (∑ g, w b x g * (gamma g - M.tau theta) ^ 2) := by apply Finset.sum_le_sum intro b _ apply Finset.sum_le_sum intro x _ exact mul_le_mul_of_nonneg_left (designMass_mul_conditionalBarycenter_sq_le pi w gamma d (M.tau theta) hw hocc b x) (M.P_nonneg theta b x) _ = ∑ b, ∑ x, ∑ g, M.P theta b x * w b x g * (gamma g - M.tau theta) ^ 2 := by simp_rw [Finset.mul_sum, mul_assoc] -
risk_barycenterProcedure_letheorem — Nonnegative grid weights that sum to each design probability, with the null-fiber default inside the action interval and all grid actions inside that interval, make the bounded barycenter procedure's statewise risk no greater than the randomized grid-action risk.hypothesesTheta :sharedType u_4B :sharedType u_5G :sharedType u_6M :Model Theta B Xpi :w :∀ bifX bandGthenℝgamma :G → ℝd :ℝhw :∀ b x g, 0 ≤ w b x ghocc :∀ b x, ∑ g, w b x g = pi.p bl u :ℝhd :d ∈ Icc l uhgamma :∀ g, gamma g ∈ Icc l utheta :Thetaconclusionrisk M.P M.tau (barycenterProcedure pi w gamma d hw hocc hd hgamma) theta≤ ∑ b, ∑ x, ∑ g, M.P theta b x * w b x g * (gamma g - M.tau theta) ^ 2Proof (Lean source)
theorem Model.risk_barycenterProcedure_le [∀ b, Fintype (X b)] (M : Model Theta B X) (pi : FiniteDesign B) (w : ∀ b, X b → G → ℝ) (gamma : G → ℝ) (d : ℝ) (hw : ∀ b x g, 0 ≤ w b x g) (hocc : ∀ b x, ∑ g, w b x g = pi.p b) {l u : ℝ} (hd : d ∈ Icc l u) (hgamma : ∀ g, gamma g ∈ Icc l u) (theta : Theta) : risk M.P M.tau (barycenterProcedure pi w gamma d hw hocc hd hgamma) theta ≤ ∑ b, ∑ x, ∑ g, M.P theta b x * w b x g * (gamma g - M.tau theta) ^ 2 := by simpa [risk, barycenterProcedure] using M.conditionalBarycenter_risk_le pi w gamma d hw hocc theta
Saddle 1 core · 2 supporting This module applies Sion's minimax theorem to convexified finite risk vectors and finite priors, recovers an ordinary procedure by conditional Jensen, and bridges the saddle value to Causalean's minimaxValue and FiniteDe ★ finite_bounded_squared_loss_has_saddle
Sion saddle point and finite squared-loss minimax attainment
This module applies Sion's minimax theorem to convexified finite risk vectors and
finite priors, recovers an ordinary procedure by conditional Jensen, and bridges
the saddle value to Causalean's minimaxValue and FiniteDesign.E APIs.
theorem finite_bounded_squared_loss_has_saddle reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSquaredLoss
Finite bounded squared-loss minimax theorem. In nonempty finite state and design spaces, an ordered real action interval and nonnegative likelihood coefficients guarantee an ordinary randomized design, bounded decision rule, and finite least-favorable prior attaining both minimax saddle inequalities. No likelihood normalization, observation-space nonemptiness, or target-in-interval assumption is required.
Formal statement
hypotheses
Theta :
Type u_1
R :
Type u_2
R → Type u_3
Nonempty Theta
Nonempty R
P :
Theta → ∀ r, X r → ℝ
tau :
Theta → ℝ
l u :
ℝ
hlu :
l ≤ u
conclusion
∃ qstar : FiniteDesign R,
∃ deltastar : ∀ r,
X r → Icc l u, ∃ nu : FiniteDesign Theta, (∀ theta, risk P tau ⟨qstar, deltastar⟩ theta ≤ minimaxValue (risk P tau : Procedure X l u → Theta → ℝ)) ∧ (∀ qprime : Procedure X l u, minimaxValue (risk P tau : Procedure X l u → Theta → ℝ) ≤ nu.E (risk P tau qprime))
Proof (Lean source)
theorem finite_bounded_squared_loss_has_saddle
[Nonempty Theta] [Nonempty R]
(P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ)
{l u : ℝ} (hlu : l ≤ u)
(hP : ∀ theta r x, 0 ≤ P theta r x) :
∃ qstar : FiniteDesign R,
∃ deltastar : ∀ r, X r → Icc l u,
∃ nu : FiniteDesign Theta,
(∀ theta,
risk P tau ⟨qstar, deltastar⟩ theta ≤
minimaxValue (risk P tau : Procedure X l u → Theta → ℝ)) ∧
(∀ qprime : Procedure X l u,
minimaxValue (risk P tau : Procedure X l u → Theta → ℝ) ≤
nu.E (risk P tau qprime)) := by
/- Obtain the Sion saddle, recover its dominated ordinary procedure, convert the
prior-simplex point to `FiniteDesign`, rewrite the saddle value with
`saddle_value_eq_minimaxValue`, and specialize the two saddle inequalities. -/
classical
obtain ⟨zstar, hz, nustar, hnu, hs⟩ :=
convexified_risk_game_has_saddle P tau hlu
obtain ⟨q, hq⟩ :=
exists_procedure_risk_le_of_mem_convexHull P tau hP hlu hz
let nu : FiniteDesign Theta := finiteDesignOfSimplex hnu
have hvalue : bayesPayoff zstar nustar =
minimaxValue (risk P tau : Procedure X l u → Theta → ℝ) :=
saddle_value_eq_minimaxValue P tau hP hlu hz hnu hs
refine ⟨q.design, q.decision, nu, ?_, ?_⟩
· intro theta
have hpoint : single theta 1 ∈ stdSimplex ℝ Theta :=
single_mem_stdSimplex ℝ theta
have hs_theta := hs zstar hz (single theta 1) hpoint
calc
risk P tau q theta ≤ zstar theta := hq theta
_ = bayesPayoff zstar (single theta 1) := by
simp [bayesPayoff, Pi.single_apply]
_ ≤ bayesPayoff zstar nustar := hs_theta
_ = minimaxValue (risk P tau : Procedure X l u → Theta → ℝ) := hvalue
· intro qprime
have hrisk_mem : riskVector P tau qprime.toAmbient ∈
convexHull ℝ (riskVector P tau '' procedureSet X l u) := by
apply subset_convexHull ℝ
exact ⟨qprime.toAmbient, qprime.toAmbient_mem, rfl⟩
have hs_q := hs (riskVector P tau qprime.toAmbient) hrisk_mem nustar hnu
calc
minimaxValue (risk P tau : Procedure X l u → Theta → ℝ) =
bayesPayoff zstar nustar := hvalue.symm
_ ≤ bayesPayoff (riskVector P tau qprime.toAmbient) nustar := hs_q
_ = nu.E (risk P tau qprime) := by
rw [← bayesPayoff_eq_E]
apply Finset.sum_congr rfl
intro theta htheta
rw [show riskVector P tau qprime.toAmbient theta =
risk P tau qprime theta by
exact rawRisk_toAmbient P tau qprime theta]
change nustar theta * risk P tau qprime theta =
nustar theta * risk P tau qprime theta
rfl
2 supporting declarations (lemmas, instances)
-
convexified_risk_game_has_saddletheorem — For nonempty finite state and design spaces, given likelihood coefficients and an ordered action interval, the convexified risk game has an attaining saddle point consisting of a risk vector and a finite prior.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3Nonempty ThetaNonempty RP :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝhlu :l ≤ uconclusion∃ nustar ∈ stdSimplex ℝ Theta,IsSaddlePointOn (convexHull ℝ (riskVector P tau '' procedureSet X l u)) (stdSimplex ℝ Theta) bayesPayoff zstar nustarProof (Lean source)
theorem convexified_risk_game_has_saddle [Nonempty Theta] [Nonempty R] (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) {l u : ℝ} (hlu : l ≤ u) : ∃ zstar ∈ convexHull ℝ (riskVector P tau '' procedureSet X l u), ∃ nustar ∈ stdSimplex ℝ Theta, IsSaddlePointOn (convexHull ℝ (riskVector P tau '' procedureSet X l u)) (stdSimplex ℝ Theta) bayesPayoff zstar nustar := by /- Apply `Sion.exists_isSaddlePointOn`. The risk hull and prior simplex are nonempty, compact, and convex. The bilinear finite-sum payoff is continuous, convex in the risk vector, and concave in the prior. -/ classical let K := convexHull ℝ (riskVector P tau '' procedureSet X l u) let S := stdSimplex ℝ Theta have hK_ne : K.Nonempty := by apply Set.Nonempty.convexHull exact (procedureSet_nonempty (X := X) hlu).image (riskVector P tau) have hS_ne : S.Nonempty := ⟨Pi.single (choice inferInstance) 1, single_mem_stdSimplex ℝ (choice inferInstance)⟩ apply Sion.exists_isSaddlePointOn hK_ne (convex_convexHull ℝ _) (isCompact_convexHull_riskVectors P tau l u) · intro nu hnu have hsec : Continuous (fun z ↦ bayesPayoff z nu) := continuous_bayesPayoff.comp (continuous_id.prodMk continuous_const) exact hsec.continuousOn.lowerSemicontinuousOn · intro nu hnu apply ConvexOn.quasiconvexOn refine ⟨convex_convexHull ℝ _, ?_⟩ intro z hz w hw a b ha hb hab simp only [bayesPayoff, Pi.add_apply, Pi.smul_apply, smul_eq_mul] rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib] apply le_of_eq apply Finset.sum_congr rfl intro theta htheta ring · exact convex_stdSimplex ℝ Theta · exact hS_ne · exact isCompact_stdSimplex ℝ Theta · intro z hz have hsec : Continuous (fun nu ↦ bayesPayoff z nu) := continuous_bayesPayoff.comp (continuous_const.prodMk continuous_id) exact hsec.continuousOn.upperSemicontinuousOn · intro z hz apply ConcaveOn.quasiconcaveOn refine ⟨convex_stdSimplex ℝ Theta, ?_⟩ intro nu hnu mu hmu a b ha hb hab simp only [bayesPayoff, Pi.add_apply, Pi.smul_apply, smul_eq_mul] rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib] apply le_of_eq apply Finset.sum_congr rfl intro theta htheta ring -
saddle_value_eq_minimaxValuetheorem — Given nonnegative likelihood coefficients, an ordered action interval, and a saddle point in the feasible convexified game, its Bayes payoff equals Causalean's minimax value over ordinary bounded finite procedures.hypothesesTheta :sharedType u_1R :sharedType u_2R → Type u_3Nonempty ThetaNonempty RP :Theta → ∀ r, X r → ℝtau :Theta → ℝl u :ℝhlu :l ≤ uzstar nustar :Theta → ℝhz :hnu :nustar ∈ stdSimplex ℝ Thetahs :IsSaddlePointOn (convexHull ℝ (riskVector P tau '' procedureSet X l u)) (stdSimplex ℝ Theta) bayesPayoff zstar nustarconclusionProof (Lean source)
theorem saddle_value_eq_minimaxValue [Nonempty Theta] [Nonempty R] (P : Theta → ∀ r, X r → ℝ) (tau : Theta → ℝ) (hP : ∀ theta r x, 0 ≤ P theta r x) {l u : ℝ} (hlu : l ≤ u) {zstar nustar : Theta → ℝ} (hz : zstar ∈ convexHull ℝ (riskVector P tau '' procedureSet X l u)) (hnu : nustar ∈ stdSimplex ℝ Theta) (hs : IsSaddlePointOn (convexHull ℝ (riskVector P tau '' procedureSet X l u)) (stdSimplex ℝ Theta) bayesPayoff zstar nustar) : bayesPayoff zstar nustar = minimaxValue (risk P tau : Procedure X l u → Theta → ℝ) := by /- Recover a procedure dominated by `zstar`. Point-mass priors show all its state risks are at most the saddle value, giving minimax ≤ saddle. Conversely, the saddle lower inequality applies to every attainable risk vector; its prior average is at most that procedure's finite worst-case risk, so `le_minimaxValue` gives saddle ≤ minimax. Finiteness supplies all `BddAbove` obligations. -/ classical let riskFn : Procedure X l u → Theta → ℝ := risk P tau obtain ⟨qz, hqz⟩ := exists_procedure_risk_le_of_mem_convexHull P tau hP hlu hz have hz_le_value (theta : Theta) : zstar theta ≤ bayesPayoff zstar nustar := by have hpoint : single theta 1 ∈ stdSimplex ℝ Theta := single_mem_stdSimplex ℝ theta have h := hs zstar hz (single theta 1) hpoint simpa [bayesPayoff, Pi.single_apply] using h have hqz_value (theta : Theta) : riskFn qz theta ≤ bayesPayoff zstar nustar := (hqz theta).trans (hz_le_value theta) have hminimax_le : minimaxValue riskFn ≤ bayesPayoff zstar nustar := by calc minimaxValue riskFn ≤ worstCaseRisk riskFn qz := minimaxValue_le_worstCaseRisk_of_nonneg (fun q theta ↦ risk_nonneg P tau hP q theta) qz _ ≤ bayesPayoff zstar nustar := worstCaseRisk_le hqz_value have hvalue_le : bayesPayoff zstar nustar ≤ minimaxValue riskFn := by apply @le_minimaxValue _ _ ⟨qz⟩ intro q have hrisk_mem : riskVector P tau q.toAmbient ∈ convexHull ℝ (riskVector P tau '' procedureSet X l u) := by apply subset_convexHull ℝ exact ⟨q.toAmbient, q.toAmbient_mem, rfl⟩ have hs_q := hs (riskVector P tau q.toAmbient) hrisk_mem nustar hnu have hcoord (theta : Theta) : riskFn q theta ≤ worstCaseRisk riskFn q := le_worstCaseRisk (Finite.bddAbove_range (riskFn q)) theta calc bayesPayoff zstar nustar ≤ bayesPayoff (riskVector P tau q.toAmbient) nustar := hs_q _ = ∑ theta, nustar theta * riskFn q theta := by apply Finset.sum_congr rfl intro theta htheta rw [show riskVector P tau q.toAmbient theta = riskFn q theta by exact rawRisk_toAmbient P tau q theta] _ ≤ ∑ theta, nustar theta * worstCaseRisk riskFn q := by apply Finset.sum_le_sum intro theta htheta exact mul_le_mul_of_nonneg_left (hcoord theta) (hnu.1 theta) _ = worstCaseRisk riskFn q := by rw [← Finset.sum_mul, hnu.2, one_mul] exact le_antisymm hvalue_le hminimax_le