Stat.Minimax.FiniteSideInformation
Finite side-information minimax convergence: compact probability-simplex coordinates, finite empirical concentration, exact-side comparison, and convergence from iid side samples to observing the side-law vector.
Coordinates 3 core · 6 supporting This module packages probability mass functions on a finite alphabet as the standard real simplex. ★ isCompact_finitePmf
Finite probability coordinates
This module packages probability mass functions on a finite alphabet as the standard real simplex. It also records the coordinate and finite-product continuity facts used by finite side-information experiments.
abbrev FinitePmf reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
A finite alphabet has as its coordinate probability simplex the subtype of real vectors with nonnegative coordinates summing to one.
Definition (Lean source)
theorem isCompact_finitePmf reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
The finite probability simplex is compact in its coordinate topology.
def productProbability reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a finite probability vector and a finite sample, the product probability is the product of the sampled atom masses.
6 supporting declarations (lemmas, instances)
-
continuous_atomtheorem — Evaluation at an atom is a continuous coordinate on the finite probability simplex.Proof (Lean source)
theorem continuous_atom (c : C) : Continuous (fun w : FinitePmf C ↦ (w.1 c : ℝ)) := by exact (continuous_apply c).comp continuous_subtype_val -
continuous_productProbabilitytheorem — For a fixed finite sample, its product probability varies continuously with the underlying probability vector.hypothesesconclusionProof (Lean source)
theorem continuous_productProbability {m : ℕ} (z : Fin m → C) : Continuous (fun w : FinitePmf C ↦ productProbability C w z) := by apply continuous_finsetProd intro i _ exact (continuous_apply (z i)).comp continuous_subtype_val -
productProbability_nonnegtheorem — Every finite product probability is nonnegative.hypothesesconclusion0 ≤ productProbability C w zProof (Lean source)
theorem productProbability_nonneg {m : ℕ} (w : FinitePmf C) (z : Fin m → C) : 0 ≤ productProbability C w z := by exact Finset.prod_nonneg fun i _ ↦ FinitePmf.nonneg C w (z i) -
sum_productProbabilitytheorem — The product probabilities of all length-m samples sum to one.hypothesesconclusion∑ z : Fin m → C, productProbability C w z = 1Proof (Lean source)
theorem sum_productProbability {m : ℕ} (w : FinitePmf C) : ∑ z : Fin m → C, productProbability C w z = 1 := by calc ∑ z : Fin m → C, productProbability C w z = ∏ _i : Fin m, ∑ c, w.1 c := by symm exact Fintype.prod_sum fun _i : Fin m ↦ fun c : C ↦ w.1 c _ = 1 := by simp [w.sum_eq_one]
Experiments 8 core · 2 supporting This module defines the two decision problems compared by the convergence theorem: exact observation of a finite side-law vector, and observation of a finite iid side sample. ★ empiricalSideRisk_le
Exact and empirical finite side-information experiments
This module defines the two decision problems compared by the convergence theorem: exact observation of a finite side-law vector, and observation of a finite iid side sample.
abbrev ExactSideProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a labeled alphabet, a side alphabet, and action bounds, an exact-side procedure assigns a bounded action after observing a label and its exact finite side-law vector.
abbrev EmpiricalSideProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a labeled alphabet, a side alphabet, a sample size, and action bounds, an empirical-side procedure assigns a bounded action after observing a label and ordered side draws.
def sidePmf reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given side-probability coordinates that are simplex-valid, the side law at a parameter is the corresponding finite probability vector.
Definition (Lean source)
parameters
Theta :
Type u_1
C :
Type u_3
q :
Theta → C → ℝ
hq :
∀ theta, q theta ∈ stdSimplex ℝ C
theta :
Theta
def
given by
⟨q theta, hq theta⟩
def exactSideRisk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label and side probabilities, a target, an exact-side procedure, and a parameter, the exact-side squared risk averages only over the labeled outcome because the side-law vector is observed without noise.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
q :
Theta → C → ℝ
hq :
∀ theta, q theta ∈ stdSimplex ℝ C
tau :
Theta → ℝ
d :
ExactSideProcedure X C l u
theta :
Theta
def
exactSideRisk p q hq tau d theta :
ℝ
def empiricalSideRisk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label and side probabilities, a target, an empirical-side procedure, a sample size, and a parameter, the empirical-side squared risk averages squared loss over the label and all ordered iid side samples.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
q :
Theta → C → ℝ
hq :
∀ theta, q theta ∈ stdSimplex ℝ C
tau :
Theta → ℝ
m :
ℕ
d :
EmpiricalSideProcedure X C m l u
theta :
Theta
def
empiricalSideRisk p q hq tau m d theta :
ℝ
given by
∑ x, p theta x * ∑ z : Fin m → C, productProbability C (sidePmf q hq theta) z * ((d x z : ℝ) - tau theta) ^ 2
def exactSideMinimaxValue reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label probabilities, side probabilities, a target, and action bounds, the exact-side minimax value is the infimum over bounded exact-law procedures of their worst-case squared risk over the parameter space.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
p :
Theta → X → ℝ
q :
Theta → C → ℝ
hq :
tau :
Theta → ℝ
l u :
ℝ
def
exactSideMinimaxValue p q hq tau l u :
ℝ
given by
minimaxValue (exactSideRisk p q hq tau : ExactSideProcedure X C l u → Theta → ℝ)
def empiricalSideMinimaxValue reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label probabilities, side probabilities, a target, action bounds, and a sample size, the empirical-side minimax value is the infimum over bounded sample procedures of their worst-case squared risk over the parameter space.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
p :
Theta → X → ℝ
q :
Theta → C → ℝ
hq :
tau :
Theta → ℝ
l u :
ℝ
m :
ℕ
def
empiricalSideMinimaxValue p q hq tau l u m :
ℝ
given by
minimaxValue (empiricalSideRisk p q hq tau m : EmpiricalSideProcedure X C m l u → Theta → ℝ)
theorem empiricalSideRisk_le reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Under probability-simplex label and side coordinates, with ordered action bounds containing the target, empirical-side squared risk is at most the squared action width.
Formal statement
hypotheses
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
q :
Theta → C → ℝ
hp :
∀ theta, p theta ∈ stdSimplex ℝ X
hq :
∀ theta, q theta ∈ stdSimplex ℝ C
tau :
Theta → ℝ
hlu :
l ≤ u
htau :
∀ theta, tau theta ∈ Icc l u
m :
ℕ
d :
EmpiricalSideProcedure X C m l u
theta :
Theta
conclusion
empiricalSideRisk p q hq tau m d theta ≤ (u - l) ^ 2
Proof (Lean source)
theorem empiricalSideRisk_le (p : Theta → X → ℝ) (q : Theta → C → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (tau : Theta → ℝ)
(hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) (m : ℕ)
(d : EmpiricalSideProcedure X C m l u) (theta : Theta) :
empiricalSideRisk p q hq tau m d theta ≤ (u - l) ^ 2 := by
unfold empiricalSideRisk
calc
∑ x, p theta x * ∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z * ((d x z : ℝ) - tau theta) ^ 2 ≤
∑ x, p theta x * (u - l) ^ 2 := by
apply Finset.sum_le_sum
intro x _
apply mul_le_mul_of_nonneg_left _ ((hp theta).1 x)
calc
∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z * ((d x z : ℝ) - tau theta) ^ 2 ≤
∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z * (u - l) ^ 2 := by
apply Finset.sum_le_sum
intro z _
apply mul_le_mul_of_nonneg_left _
(productProbability_nonneg C (sidePmf q hq theta) z)
have hd := (d x z).2
have ht := htau theta
have hdiff_le : (d x z : ℝ) - tau theta ≤ u - l :=
sub_le_sub hd.2 ht.1
have hneg_diff_le : -(u - l) ≤ (d x z : ℝ) - tau theta := by
linarith [hd.1, ht.2]
nlinarith [hlu, mul_nonneg (sub_nonneg.mpr hdiff_le)
(by linarith : 0 ≤ (u - l) + ((d x z : ℝ) - tau theta))]
_ = (u - l) ^ 2 := by
rw [← Finset.sum_mul, sum_productProbability]
exact one_mul _
_ = (u - l) ^ 2 := by
rw [← Finset.sum_mul, (hp theta).2]
exact one_mul _
2 supporting declarations (lemmas, instances)
-
continuous_sidePmftheorem — When side-probability coordinates are simplex-valid and continuous, the simplex-valued side law is continuous.hypothesesconclusionContinuous (sidePmf q hq)Proof (Lean source)
theorem continuous_sidePmf [TopologicalSpace Theta] (q : Theta → C → ℝ) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) : Continuous (sidePmf q hq) := by exact continuous_induced_rng.2 (continuous_pi hqcont) -
empiricalSideRisk_nonnegtheorem — Under probability-simplex label and side coordinates, empirical-side squared risk is nonnegative.hypothesesTheta :sharedType u_1X :sharedType u_2C :sharedType u_3l :sharedℝu :sharedℝp :Theta → X → ℝq :Theta → C → ℝhp :∀ theta, p theta ∈ stdSimplex ℝ Xhq :∀ theta, q theta ∈ stdSimplex ℝ Ctau :Theta → ℝm :ℕd :EmpiricalSideProcedure X C m l utheta :Thetaconclusion0 ≤ empiricalSideRisk p q hq tau m d thetaProof (Lean source)
theorem empiricalSideRisk_nonneg (p : Theta → X → ℝ) (q : Theta → C → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (tau : Theta → ℝ) (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (theta : Theta) : 0 ≤ empiricalSideRisk p q hq tau m d theta := by unfold empiricalSideRisk apply sum_nonneg intro x _ apply mul_nonneg ((hp theta).1 x) apply sum_nonneg intro z _ exact mul_nonneg (productProbability_nonneg C (sidePmf q hq theta) z) (sq_nonneg _)
Fiber 3 core · 0 supporting This module isolates the compactness argument saying that minimax values over shrinking neighborhoods of an observed side law converge to the minimax value over its exact fiber. ★ localMinimaxValue_tendsto_fiber
Compact shrinking-fiber minimax values
This module isolates the compactness argument saying that minimax values over shrinking neighborhoods of an observed side law converge to the minimax value over its exact fiber.
def fiberMinimaxValue reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
For label probabilities, a target, side coordinates, action bounds, and a center parameter, the exact-fiber local minimax value minimizes finite squared risk over decisions and maximizes over parameters with the same side law as the center.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
p :
Theta → X → ℝ
tau :
Theta → ℝ
q :
Theta → C → ℝ
hq :
∀ theta, q theta ∈ stdSimplex ℝ C
l u :
ℝ
theta0 :
Theta
def
fiberMinimaxValue p tau q hq l u theta0 :
ℝ
given by
minimaxValue (fun (d : BoundedDecision X l u) (theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦ finiteSquaredRisk p tau d theta.1)
def localMinimaxValue reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
For label probabilities, a target, side coordinates, action bounds, a radius, and a center parameter, the local minimax value minimizes finite squared risk over decisions and maximizes over parameters whose side law is within that radius of the center law.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
p :
Theta → X → ℝ
tau :
Theta → ℝ
q :
Theta → C → ℝ
hq :
∀ theta, q theta ∈ stdSimplex ℝ C
l u r :
ℝ
theta0 :
Theta
def
localMinimaxValue p tau q hq l u r theta0 :
ℝ
given by
minimaxValue (fun (d : BoundedDecision X l u) (theta : {theta : Theta // dist (sidePmf q hq theta) (sidePmf q hq theta0) ≤ r}) ↦ finiteSquaredRisk p tau d theta.1)
theorem localMinimaxValue_tendsto_fiber reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
On a compact parameter space, if label and side coordinates and the target are continuous, probabilities are simplex-valid, and the action interval contains the target, then local minimax values over radii 1/(n+1) converge to the exact-fiber minimax value.
Formal statement
hypotheses
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
hp :
hq :
hpcont :
hqcont :
htau :
Continuous tau
hlu :
l ≤ u
theta0 :
Theta
conclusion
Tendsto (fun n : ℕ ↦ localMinimaxValue p tau q hq l u (1 / (n + 1 : ℝ)) theta0) atTop (nhds (fiberMinimaxValue p tau q hq l u theta0))
Proof (Lean source)
theorem localMinimaxValue_tendsto_fiber (p : Theta → X → ℝ)
(q : Theta → C → ℝ) (tau : Theta → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C)
(hpcont : ∀ x, Continuous (fun theta ↦ p theta x))
(hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) (htau : Continuous tau)
(hlu : l ≤ u) (htau_mem : ∀ theta, tau theta ∈ Icc l u) (theta0 : Theta) :
Tendsto (fun n : ℕ ↦ localMinimaxValue p tau q hq l u (1 / (n + 1 : ℝ)) theta0)
atTop (nhds (fiberMinimaxValue p tau q hq l u theta0)) := by
-- Proof plan: compactness gives convergent subsequences of near-optimal bounded decisions and
-- parameters; continuity identifies every zero-radius cluster point with the exact fiber.
-- A direct epsilon proof is also available and avoids choosing exact minimizers: restriction
-- gives `fiberMinimaxValue ≤ localMinimaxValue`; choose a decision whose exact-fiber
-- worst-case risk is within `ε / 2` of the infimum. The strict sublevel set of its continuous
-- risk contains the compact exact fiber. Compactness of the complementary parameter set and
-- continuity of `sidePmf` then give a positive side-law radius whose inverse image lies in that
-- sublevel set. Eventually `1 / (n + 1)` is below this radius, yielding the reverse epsilon
-- bound. `finiteSquaredRisk_bounds` supplies every conditional-completeness side condition.
letI : Nonempty (BoundedDecision X l u) :=
⟨fun _ ↦ ⟨l, le_rfl, hlu⟩⟩
have hrisk (d : BoundedDecision X l u) (theta : Theta) :
0 ≤ finiteSquaredRisk p tau d theta ∧
finiteSquaredRisk p tau d theta ≤ (u - l) ^ 2 :=
finiteSquaredRisk_bounds p tau (fun theta x ↦ (hp theta).1 x)
(fun theta ↦ (hp theta).2) hlu htau_mem d theta
have hfiber_le_local (r : ℝ) (hr : 0 ≤ r) :
fiberMinimaxValue p tau q hq l u theta0 ≤
localMinimaxValue p tau q hq l u r theta0 := by
unfold fiberMinimaxValue localMinimaxValue
refine minimaxValue_mono_class_of_nonneg
(fun theta ↦ ⟨theta.1, ?_⟩) ?_ ?_ ?_ ?_
· simpa [theta.property] using hr
· exact fun d theta ↦ (hrisk d theta.1).1
· exact fun d theta ↦ (hrisk d theta.1).1
· intro d
refine ⟨(u - l) ^ 2, ?_⟩
rintro _ ⟨theta, rfl⟩
exact (hrisk d theta.1).2
· exact fun _ _ ↦ le_rfl
apply tendsto_order.2
constructor
· intro a ha
filter_upwards [] with n
exact ha.trans_le (hfiber_le_local _ (by positivity))
· intro b hb
let c := (fiberMinimaxValue p tau q hq l u theta0 + b) / 2
have hvalue_lt_c : fiberMinimaxValue p tau q hq l u theta0 < c := by
dsimp [c]
linarith
have hc_lt_b : c < b := by
dsimp [c]
linarith
let fiberRisk := fun (d : BoundedDecision X l u)
(theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦
finiteSquaredRisk p tau d theta.1
have hnonnegFiber : ∀ d theta, 0 ≤ fiberRisk d theta :=
fun d theta ↦ (hrisk d theta.1).1
have hbddBelow : BddBelow (range (worstCaseRisk fiberRisk)) :=
bddBelow_range_worstCaseRisk hnonnegFiber
have hvalue : (⨅ d, worstCaseRisk fiberRisk d) < c := by
simpa [fiberMinimaxValue, minimaxValue, fiberRisk] using hvalue_lt_c
obtain ⟨d, hd⟩ := (ciInf_lt_iff hbddBelow).1 hvalue
have hbddFiber : BddAbove (range (fiberRisk d)) := by
refine ⟨(u - l) ^ 2, ?_⟩
rintro _ ⟨theta, rfl⟩
exact (hrisk d theta.1).2
have hfiberRisk_lt (theta : Theta)
(htheta : sidePmf q hq theta = sidePmf q hq theta0) :
finiteSquaredRisk p tau d theta < c := by
exact (le_worstCaseRisk hbddFiber ⟨theta, htheta⟩).trans_lt hd
let bad : Set Theta := {theta | c ≤ finiteSquaredRisk p tau d theta}
have hbadClosed : IsClosed bad := by
change IsClosed ((fun theta ↦ finiteSquaredRisk p tau d theta) ⁻¹' Ici c)
exact isClosed_Ici.preimage (continuous_finiteSquaredRisk p tau hpcont htau d)
have hbadCompact : IsCompact bad := hbadClosed.isCompact
have hsideCont : Continuous (sidePmf q hq) := continuous_sidePmf q hq hqcont
have himageClosed : IsClosed (sidePmf q hq '' bad) :=
(hbadCompact.image hsideCont).isClosed
have hcenterNotImage : sidePmf q hq theta0 ∉ sidePmf q hq '' bad := by
rintro ⟨theta, hthetaBad, hthetaSide⟩
exact (not_lt_of_ge hthetaBad) (hfiberRisk_lt theta hthetaSide)
have himageComplNhds : (sidePmf q hq '' bad)ᶜ ∈ nhds (sidePmf q hq theta0) :=
himageClosed.isOpen_compl.mem_nhds hcenterNotImage
obtain ⟨δ, hδ, hball⟩ := Metric.mem_nhds_iff.1 himageComplNhds
have hnear (theta : Theta)
(htheta : dist (sidePmf q hq theta) (sidePmf q hq theta0) < δ) :
finiteSquaredRisk p tau d theta < c := by
by_contra hnot
have hthetaBad : theta ∈ bad := by
simpa [bad] using le_of_not_gt hnot
have hthetaImage : sidePmf q hq theta ∈ sidePmf q hq '' bad :=
⟨theta, hthetaBad, rfl⟩
have hthetaBall : sidePmf q hq theta ∈ ball (sidePmf q hq theta0) δ := by
simpa [Metric.mem_ball, dist_comm] using htheta
exact (hball hthetaBall) hthetaImage
have hradius : ∀ᶠ n : ℕ in atTop, 1 / (n + 1 : ℝ) < δ :=
(tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ)).eventually_lt_const hδ
filter_upwards [hradius] with n hn
haveI : Nonempty {theta : Theta //
dist (sidePmf q hq theta) (sidePmf q hq theta0) ≤ 1 / (n + 1 : ℝ)} :=
⟨⟨theta0, by simp only [dist_self]; positivity⟩⟩
let localRisk : BoundedDecision X l u →
{theta : Theta //
dist (sidePmf q hq theta) (sidePmf q hq theta0) ≤ 1 / (n + 1 : ℝ)} → ℝ :=
fun d theta ↦ finiteSquaredRisk p tau d theta.1
change minimaxValue localRisk < b
have hlocalNonneg : ∀ d theta, 0 ≤ localRisk d theta := by
intro d theta
exact (hrisk d theta.1).1
calc
minimaxValue localRisk ≤ worstCaseRisk localRisk d :=
minimaxValue_le_worstCaseRisk_of_nonneg hlocalNonneg d
_ < b := (worstCaseRisk_le fun theta ↦
(hnear theta.1 (theta.2.trans_lt hn)).le).trans_lt hc_lt_b
Comparison 2 core · 2 supporting This module constructs the exact-law conditional average of an empirical procedure and applies convexity of squared loss to obtain the lower minimax comparison. ★ exactSideMinimaxValue_eq_iSup_fiber
Comparison with the exact side-law experiment
This module constructs the exact-law conditional average of an empirical procedure and applies convexity of squared loss to obtain the lower minimax comparison. It also identifies exact-law minimax risk with the supremum of fiberwise minimax values.
def conditionalAverageProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given action bounds, a sample size, and an empirical-side procedure, the conditional-average exact-side procedure averages the action over an iid sample drawn from the supplied exact side law.
Definition (Lean source)
parameters
def
given by
by intro x w refine ⟨∑ z : Fin m → C, productProbability C w z * (d x z : ℝ), ?_, ?_⟩ · calc l
= ∑ z : Fin m → C, productProbability C w z * l := by rw [← Finset.sum_mul, sum_productProbability, one_mul] _ ≤ ∑ z : Fin m → C, productProbability C w z * (d x z : ℝ) := by exact Finset.sum_le_sum fun z _ ↦ mul_le_mul_of_nonneg_left (d x z).2.1 (productProbability_nonneg C w z) · calc ∑ z : Fin m → C, productProbability C w z * (d x z : ℝ) ≤ ∑ z : Fin m → C, productProbability C w z * u := by exact Finset.sum_le_sum fun z _ ↦ mul_le_mul_of_nonneg_left (d x z).2.2 (productProbability_nonneg C w z) _ = u := by rw [← Finset.sum_mul, sum_productProbability, one_mul]
theorem exactSideMinimaxValue_eq_iSup_fiber reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
On a compact parameter space, under continuous simplex-valid label and side coordinates and a continuous bounded target, the exact-side minimax value equals the supremum of its fiberwise minimax values.
Formal statement
hypotheses
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
TopologicalSpace Theta
CompactSpace Theta
Nonempty Theta
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
hp :
hq :
hpcont :
hqcont :
htau :
Continuous tau
hlu :
l ≤ u
conclusion
exactSideMinimaxValue p q hq tau l u
= ⨆ theta0 : Theta, fiberMinimaxValue p tau q hq l u theta0
Proof (Lean source)
theorem exactSideMinimaxValue_eq_iSup_fiber
[TopologicalSpace Theta] [CompactSpace Theta] [Nonempty Theta]
(p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C)
(hpcont : ∀ x, Continuous (fun theta ↦ p theta x))
(hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) (htau : Continuous tau)
(hlu : l ≤ u) (htau_mem : ∀ theta, tau theta ∈ Icc l u) :
exactSideMinimaxValue p q hq tau l u =
⨆ theta0 : Theta, fiberMinimaxValue p tau q hq l u theta0 := by
classical
letI : Nonempty (BoundedDecision X l u) :=
⟨fun _ ↦ ⟨l, le_rfl, hlu⟩⟩
letI : Nonempty (ExactSideProcedure X C l u) :=
⟨fun _ _ ↦ ⟨l, le_rfl, hlu⟩⟩
have hrisk (d : BoundedDecision X l u) (theta : Theta) :
0 ≤ finiteSquaredRisk p tau d theta ∧
finiteSquaredRisk p tau d theta ≤ (u - l) ^ 2 :=
finiteSquaredRisk_bounds p tau (fun theta x ↦ (hp theta).1 x)
(fun theta ↦ (hp theta).2) hlu htau_mem d theta
have hexact_nonneg (d : ExactSideProcedure X C l u) (theta : Theta) :
0 ≤ exactSideRisk p q hq tau d theta := by
simpa [exactSideRisk, finiteSquaredRisk] using
(hrisk (fun x ↦ d x (sidePmf q hq theta)) theta).1
have hexact_le (d : ExactSideProcedure X C l u) (theta : Theta) :
exactSideRisk p q hq tau d theta ≤ (u - l) ^ 2 := by
simpa [exactSideRisk, finiteSquaredRisk] using
(hrisk (fun x ↦ d x (sidePmf q hq theta)) theta).2
have hfiber_le_exact (theta0 : Theta) :
fiberMinimaxValue p tau q hq l u theta0 ≤
exactSideMinimaxValue p q hq tau l u := by
let fiberRisk := fun (d : BoundedDecision X l u)
(theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦
finiteSquaredRisk p tau d theta.1
let exactRisk : ExactSideProcedure X C l u → Theta → ℝ :=
exactSideRisk p q hq tau
have hfiber_nonneg : ∀ d theta, 0 ≤ fiberRisk d theta :=
fun d theta ↦ (hrisk d theta.1).1
unfold fiberMinimaxValue exactSideMinimaxValue
refine minimaxValue_le_minimaxValue
(bddBelow_range_worstCaseRisk hfiber_nonneg) ?_
intro d
refine ⟨fun x ↦ d x (sidePmf q hq theta0), ?_⟩
letI : Nonempty {theta : Theta //
sidePmf q hq theta = sidePmf q hq theta0} := ⟨⟨theta0, rfl⟩⟩
apply Causalean.Stat.worstCaseRisk_le
intro theta
have hbddExact : BddAbove (range (exactRisk d)) := by
refine ⟨(u - l) ^ 2, ?_⟩
rintro _ ⟨theta', rfl⟩
exact hexact_le d theta'
simpa [fiberRisk, exactRisk, exactSideRisk, finiteSquaredRisk, theta.property] using
(le_worstCaseRisk hbddExact theta.1)
have hexactValue_le : exactSideMinimaxValue p q hq tau l u ≤ (u - l) ^ 2 := by
let d0 : ExactSideProcedure X C l u := fun _ _ ↦ ⟨l, le_rfl, hlu⟩
unfold exactSideMinimaxValue
calc
minimaxValue (exactSideRisk p q hq tau) ≤
worstCaseRisk (exactSideRisk p q hq tau) d0 :=
minimaxValue_le_worstCaseRisk_of_nonneg hexact_nonneg d0
_ ≤ (u - l) ^ 2 := Causalean.Stat.worstCaseRisk_le (hexact_le d0)
have hfiber_bdd : BddAbove
(range (fun theta0 : Theta ↦ fiberMinimaxValue p tau q hq l u theta0)) := by
refine ⟨(u - l) ^ 2, ?_⟩
rintro _ ⟨theta0, rfl⟩
exact (hfiber_le_exact theta0).trans hexactValue_le
apply le_antisymm
· apply le_of_forall_gt_imp_ge_of_dense
intro a ha
have hfiber_lt (theta0 : Theta) :
fiberMinimaxValue p tau q hq l u theta0 < a :=
(le_ciSup hfiber_bdd theta0).trans_lt ha
have hdecision (theta0 : Theta) : ∃ d : BoundedDecision X l u,
worstCaseRisk
(fun (d : BoundedDecision X l u)
(theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦
finiteSquaredRisk p tau d theta.1) d < a := by
let fiberRisk := fun (d : BoundedDecision X l u)
(theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦
finiteSquaredRisk p tau d theta.1
have hbddBelow : BddBelow
(range (worstCaseRisk fiberRisk)) :=
bddBelow_range_worstCaseRisk
(fun d theta ↦ (hrisk d theta.1).1)
exact (ciInf_lt_iff hbddBelow).1 (by
simpa [fiberMinimaxValue, minimaxValue, fiberRisk] using
hfiber_lt theta0)
let chosen : Theta → BoundedDecision X l u :=
fun theta0 ↦ choose (hdecision theta0)
have hchosen (theta0 : Theta) :
worstCaseRisk
(fun (d : BoundedDecision X l u)
(theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦
finiteSquaredRisk p tau d theta.1) (chosen theta0) < a :=
Classical.choose_spec (hdecision theta0)
let rep : FinitePmf C → Theta := fun w ↦
if h : ∃ theta, sidePmf q hq theta = w then choose h
else choice inferInstance
have hrep (w : FinitePmf C) (h : ∃ theta, sidePmf q hq theta = w) :
sidePmf q hq (rep w) = w := by
simp only [rep, dif_pos h]
exact Classical.choose_spec h
let assembled : ExactSideProcedure X C l u :=
fun x w ↦ chosen (rep w) x
have hassembled_lt (theta : Theta) :
exactSideRisk p q hq tau assembled theta < a := by
have hs : sidePmf q hq (rep (sidePmf q hq theta)) = sidePmf q hq theta :=
hrep _ ⟨theta, rfl⟩
let thetaFiber : {theta' : Theta //
sidePmf q hq theta' = sidePmf q hq (rep (sidePmf q hq theta))} :=
⟨theta, hs.symm⟩
have hbddFiber : BddAbove (range
((fun (d : BoundedDecision X l u)
(theta' : {theta' : Theta //
sidePmf q hq theta' = sidePmf q hq (rep (sidePmf q hq theta))}) ↦
finiteSquaredRisk p tau d theta'.1) (chosen (rep (sidePmf q hq theta))))) := by
refine ⟨(u - l) ^ 2, ?_⟩
rintro _ ⟨theta', rfl⟩
exact (hrisk _ theta'.1).2
have hpoint := le_worstCaseRisk
(risk := fun (d : BoundedDecision X l u)
(theta' : {theta' : Theta //
sidePmf q hq theta' = sidePmf q hq (rep (sidePmf q hq theta))}) ↦
finiteSquaredRisk p tau d theta'.1)
(e := chosen (rep (sidePmf q hq theta))) hbddFiber thetaFiber
calc
exactSideRisk p q hq tau assembled theta =
finiteSquaredRisk p tau (chosen (rep (sidePmf q hq theta))) theta := by
rfl
_ ≤ worstCaseRisk
(fun (d : BoundedDecision X l u)
(theta' : {theta' : Theta //
sidePmf q hq theta' = sidePmf q hq (rep (sidePmf q hq theta))}) ↦
finiteSquaredRisk p tau d theta'.1)
(chosen (rep (sidePmf q hq theta))) := by
simpa [thetaFiber] using hpoint
_ < a := hchosen (rep (sidePmf q hq theta))
unfold exactSideMinimaxValue
calc
minimaxValue (exactSideRisk p q hq tau) ≤
worstCaseRisk (exactSideRisk p q hq tau) assembled :=
minimaxValue_le_worstCaseRisk_of_nonneg hexact_nonneg assembled
_ ≤ a := Causalean.Stat.worstCaseRisk_le fun theta ↦ (hassembled_lt theta).le
· exact ciSup_le hfiber_le_exact
2 supporting declarations (lemmas, instances)
-
exactSideRisk_conditionalAverage_letheorem — Under simplex-valid label and side coordinates and ordered action bounds, conditional averaging of an empirical procedure cannot increase squared risk at any parameter.hypothesesTheta :sharedType u_1X :sharedType u_2C :sharedType u_3l :sharedℝu :sharedℝp :Theta → X → ℝq :Theta → C → ℝtau :Theta → ℝhp :∀ theta, p theta ∈ stdSimplex ℝ Xhq :∀ theta, q theta ∈ stdSimplex ℝ Chlu :l ≤ um :ℕd :EmpiricalSideProcedure X C m l utheta :ThetaconclusionexactSideRisk p q hq tau (conditionalAverageProcedure l u m d) theta≤ empiricalSideRisk p q hq tau m d thetaProof (Lean source)
theorem exactSideRisk_conditionalAverage_le (p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hlu : l ≤ u) (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (theta : Theta) : exactSideRisk p q hq tau (conditionalAverageProcedure l u m d) theta ≤ empiricalSideRisk p q hq tau m d theta := by have hconvex : ConvexOn ℝ univ (fun a : ℝ ↦ (a - tau theta) ^ 2) := by refine ⟨convex_univ, ?_⟩ intro x _ y _ a b ha hb hab dsimp apply sub_nonneg.mp calc a * (x - tau theta) ^ 2 + b * (y - tau theta) ^ 2 - (a * x + b * y - tau theta) ^ 2 = a * b * (x - y) ^ 2 := by have hb' : b = 1 - a := by linarith rw [hb'] ring _ ≥ 0 := mul_nonneg (mul_nonneg ha hb) (sq_nonneg (x - y)) unfold exactSideRisk empiricalSideRisk apply Finset.sum_le_sum intro x _ apply mul_le_mul_of_nonneg_left _ ((hp theta).1 x) simpa [conditionalAverageProcedure, smul_eq_mul] using (hconvex.map_sum_le (t := univ) (w := fun z : Fin m → C ↦ productProbability C (sidePmf q hq theta) z) (p := fun z : Fin m → C ↦ (d x z : ℝ)) (fun z _ ↦ productProbability_nonneg C (sidePmf q hq theta) z) (by simpa using sum_productProbability C (sidePmf q hq theta)) (fun _ _ ↦ Set.mem_univ _)) -
exactSideMinimaxValue_le_empiricalSideMinimaxValuetheorem — Under simplex-valid probabilities, ordered action bounds, and a bounded target, the exact-side minimax value is no larger than every empirical-side minimax value.hypothesesTheta :sharedType u_1X :sharedType u_2C :sharedType u_3l :sharedℝu :sharedℝNonempty Thetap :Theta → X → ℝq :Theta → C → ℝtau :Theta → ℝhp :hq :hlu :l ≤ um :ℕconclusionexactSideMinimaxValue p q hq tau l u ≤ empiricalSideMinimaxValue p q hq tau l u mProof (Lean source)
theorem exactSideMinimaxValue_le_empiricalSideMinimaxValue [Nonempty Theta] (p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) (m : ℕ) : exactSideMinimaxValue p q hq tau l u ≤ empiricalSideMinimaxValue p q hq tau l u m := by letI : Nonempty (EmpiricalSideProcedure X C m l u) := ⟨fun _ _ ↦ ⟨l, le_rfl, hlu⟩⟩ have hexact_nonneg (d : ExactSideProcedure X C l u) (theta : Theta) : 0 ≤ exactSideRisk p q hq tau d theta := by unfold exactSideRisk exact sum_nonneg fun x _ ↦ mul_nonneg ((hp theta).1 x) (sq_nonneg _) unfold exactSideMinimaxValue empiricalSideMinimaxValue refine minimaxValue_le_minimaxValue (bddBelow_range_worstCaseRisk hexact_nonneg) ?_ intro d refine ⟨conditionalAverageProcedure l u m d, ?_⟩ apply worstCaseRisk_le intro theta refine (exactSideRisk_conditionalAverage_le p q tau hp hq hlu m d theta).trans ?_ apply le_worstCaseRisk refine ⟨(u - l) ^ 2, ?_⟩ rintro _ ⟨theta', rfl⟩ exact empiricalSideRisk_le p q hp hq tau hlu htau m d theta'
Risk 3 core · 4 supporting This module defines bounded decision rules for a finite labeled observation, their finite squared risks, and the continuity and uniform bounds needed by compact minimax arguments. ★ continuous_finiteSquaredRisk_joint
Finite squared risks
This module defines bounded decision rules for a finite labeled observation, their finite squared risks, and the continuity and uniform bounds needed by compact minimax arguments.
abbrev BoundedDecision reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
For a finite labeled alphabet and action bounds, a bounded decision assigns an action in the closed interval to every label.
Definition (Lean source)
def finiteSquaredRisk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label probabilities, a target, a bounded decision, and a parameter, the finite squared risk is the probability-weighted sum of squared errors over the labeled alphabet.
Definition (Lean source)
parameters
Theta :
Type u_1
X :
Type u_2
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
tau :
Theta → ℝ
d :
BoundedDecision X l u
theta :
Theta
def
finiteSquaredRisk p tau d theta :
ℝ
given by
∑ x, p theta x * (((d x : Icc l u) : ℝ) - tau theta) ^ 2
theorem continuous_finiteSquaredRisk_joint reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
When every label coordinate and the target are continuous, the finite squared risk is jointly continuous in the bounded decision and parameter.
Formal statement
hypotheses
Theta :
Type u_1
X :
Type u_2
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
tau :
Theta → ℝ
hp :
htau :
Continuous tau
conclusion
Proof (Lean source)
theorem continuous_finiteSquaredRisk_joint (p : Theta → X → ℝ) (tau : Theta → ℝ)
(hp : ∀ x, Continuous (fun theta ↦ p theta x)) (htau : Continuous tau) :
Continuous (fun z : BoundedDecision X l u × Theta ↦
finiteSquaredRisk p tau z.1 z.2) := by
unfold finiteSquaredRisk
fun_prop
4 supporting declarations (lemmas, instances)
-
finiteSquaredRisk_nonnegtheorem — If the label coordinates are nonnegative, every finite squared risk is nonnegative.hypothesesTheta :sharedType u_1X :sharedType u_2l :sharedℝu :sharedℝp :Theta → X → ℝtau :Theta → ℝhp :∀ theta x, 0 ≤ p theta xd :BoundedDecision X l utheta :Thetaconclusion0 ≤ finiteSquaredRisk p tau d thetaProof (Lean source)
theorem finiteSquaredRisk_nonneg (p : Theta → X → ℝ) (tau : Theta → ℝ) (hp : ∀ theta x, 0 ≤ p theta x) (d : BoundedDecision X l u) (theta : Theta) : 0 ≤ finiteSquaredRisk p tau d theta := by exact sum_nonneg fun x _ ↦ mul_nonneg (hp theta x) (sq_nonneg _) -
finiteSquaredRisk_boundstheorem — If label probabilities are nonnegative and sum to one, and actions and targets lie in the same ordered interval, then the finite squared risk is bounded between zero and the squared interval width.hypothesesTheta :sharedType u_1X :sharedType u_2l :sharedℝu :sharedℝp :Theta → X → ℝtau :Theta → ℝhp :∀ theta x, 0 ≤ p theta xhsum :∀ theta, ∑ x, p theta x = 1hlu :l ≤ uhtau :∀ theta, tau theta ∈ Icc l ud :BoundedDecision X l utheta :Thetaconclusionconclusion 10 ≤ finiteSquaredRisk p tau d thetaconclusion 2finiteSquaredRisk p tau d theta ≤ (u - l) ^ 2Proof (Lean source)
theorem finiteSquaredRisk_bounds (p : Theta → X → ℝ) (tau : Theta → ℝ) (hp : ∀ theta x, 0 ≤ p theta x) (hsum : ∀ theta, ∑ x, p theta x = 1) (hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) (d : BoundedDecision X l u) (theta : Theta) : 0 ≤ finiteSquaredRisk p tau d theta ∧ finiteSquaredRisk p tau d theta ≤ (u - l) ^ 2 := by refine ⟨finiteSquaredRisk_nonneg p tau hp d theta, ?_⟩ calc finiteSquaredRisk p tau d theta ≤ ∑ x, p theta x * (u - l) ^ 2 := by apply Finset.sum_le_sum intro x _ apply mul_le_mul_of_nonneg_left _ (hp theta x) have hd := (d x).2 have ht := htau theta have hdiff_le : (d x : ℝ) - tau theta ≤ u - l := sub_le_sub hd.2 ht.1 have hneg_diff_le : -(u - l) ≤ (d x : ℝ) - tau theta := by linarith [hd.1, ht.2] nlinarith [mul_nonneg (sub_nonneg.mpr hdiff_le) (by linarith : 0 ≤ (u - l) + ((d x : ℝ) - tau theta))] _ = (u - l) ^ 2 := by rw [← Finset.sum_mul, hsum theta, one_mul] -
continuous_finiteSquaredRisktheorem — When every label coordinate and the target are continuous, the finite squared risk of a fixed decision is continuous in the parameter.hypothesesTheta :sharedType u_1X :sharedType u_2l :sharedℝu :sharedℝp :Theta → X → ℝtau :Theta → ℝhp :htau :Continuous taud :BoundedDecision X l uconclusionProof (Lean source)
theorem continuous_finiteSquaredRisk (p : Theta → X → ℝ) (tau : Theta → ℝ) (hp : ∀ x, Continuous (fun theta ↦ p theta x)) (htau : Continuous tau) (d : BoundedDecision X l u) : Continuous (fun theta ↦ finiteSquaredRisk p tau d theta) := by unfold finiteSquaredRisk fun_prop -
isCompact_boundedDecisiontheorem — A finite labeled alphabet and ordered action bounds make the space of bounded decisions compact.hypothesesX :sharedType u_2l :sharedℝu :sharedℝhlu :l ≤ uconclusionProof (Lean source)
theorem isCompact_boundedDecision (hlu : l ≤ u) : IsCompact (Set.univ : Set (BoundedDecision X l u)) := by exact isCompact_univ
Approximation 1 core · 1 supporting This module packages the compact finite-cover selection argument and combines it with empirical finite-category concentration to prove the upper asymptotic comparison. ★ empiricalSideMinimax_limsup_le_exact
Finite-cover achievability
This module packages the compact finite-cover selection argument and combines it with empirical finite-category concentration to prove the upper asymptotic comparison.
theorem empiricalSideMinimax_limsup_le_exact reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Under the compact continuous finite-model assumptions, the limsup of empirical-side minimax values is at most the exact-side minimax value. The proof uses a measurable finite-cover selector and the uniform empirical L1 Hoeffding tail.
Formal statement
hypotheses
Theta :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
hp :
hq :
hpcont :
hqcont :
htau :
Continuous tau
hlu :
l ≤ u
conclusion
≤ exactSideMinimaxValue p q hq tau l u
Proof (Lean source)
theorem empiricalSideMinimax_limsup_le_exact
(p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C)
(hpcont : ∀ x, Continuous (fun theta ↦ p theta x))
(hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) (htau : Continuous tau)
(hlu : l ≤ u) (htau_mem : ∀ theta, tau theta ∈ Icc l u) :
limsup (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop ≤
exactSideMinimaxValue p q hq tau l u := by
-- Proof plan: for a cover with margin η, run `exists_measurable_finiteCoverSelector` with radii
-- `radius i - η / 2`, and select from `empiricalPmf C hm z`. On `empiricalL1 < η / 2`, the cover
-- margin makes the empirical law belong to a selector ball and the triangle inequality puts the
-- true law in the selected larger ball. Rewrite the empirical risk as a sum over samples of
-- `finiteSquaredRisk`; bound good samples by the local guarantee, bad samples by `(u-l)^2`, and
-- apply `empiricalL1_tail`. The resulting uniform bound is the benchmark plus ε plus the squared
-- width times `empiricalL1_tail_bound_tendsto_zero`; use `limsup_le_iff'` and the global risk bounds.
classical
let value := exactSideMinimaxValue p q hq tau l u
let widthSq := (u - l) ^ 2
have hwidthSq : 0 ≤ widthSq := by
dsimp [widthSq]
positivity
have hemp_nonneg (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (theta : Theta) :
0 ≤ empiricalSideRisk p q hq tau m d theta :=
empiricalSideRisk_nonneg p q hp hq tau m d theta
have hminimax_nonneg (m : ℕ) :
0 ≤ empiricalSideMinimaxValue p q hq tau l u m := by
unfold empiricalSideMinimaxValue
exact minimaxValue_nonneg (hemp_nonneg m)
have hminimax_le (m : ℕ) :
empiricalSideMinimaxValue p q hq tau l u m ≤ widthSq := by
let d0 : EmpiricalSideProcedure X C m l u := fun _ _ ↦ ⟨l, le_rfl, hlu⟩
unfold empiricalSideMinimaxValue
calc
minimaxValue (empiricalSideRisk p q hq tau m) ≤
worstCaseRisk (empiricalSideRisk p q hq tau m) d0 :=
minimaxValue_le_worstCaseRisk_of_nonneg (hemp_nonneg m) d0
_ ≤ widthSq := Causalean.Stat.worstCaseRisk_le fun theta ↦ by
exact empiricalSideRisk_le p q hp hq tau hlu htau_mem m d0 theta
have hcobounded : Filter.IsCoboundedUnder (fun x y : ℝ ↦ x ≤ y) atTop
(fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) :=
Filter.isCoboundedUnder_le_of_le atTop hminimax_nonneg
have hbounded : Filter.IsBoundedUnder (fun x y : ℝ ↦ x ≤ y) atTop
(fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) :=
Filter.isBoundedUnder_of_eventually_le (Filter.Eventually.of_forall hminimax_le)
apply (Filter.limsup_le_iff' hcobounded hbounded).2
intro y hy
let ε := (y - value) / 2
have hε : 0 < ε := by
dsimp [ε, value]
linarith
obtain ⟨k, hk, center, decision, radius, η, hη, hradius, hcover, hrisk⟩ :=
finiteCover_approximateDecision p q tau hp hq hpcont hqcont htau hlu htau_mem hε
have hselectorRadius (i : Fin k) : 0 < radius i - η / 2 := by
linarith [hradius i]
obtain ⟨select, _hselect_meas, hselect⟩ :=
exists_measurable_finiteCoverSelector k hk
(fun i ↦ sidePmf q hq (center i)) (fun i ↦ radius i - η / 2)
hselectorRadius
let tail : ℕ → ℝ := fun m ↦
2 * card C * exp (-2 * m * ((η / 2) / card C) ^ 2)
have htail_zero : Tendsto (fun m ↦ widthSq * tail m) atTop (nhds 0) := by
simpa [tail] using
(empiricalL1_tail_bound_tendsto_zero C (half_pos hη)).const_mul widthSq
have htail_small : ∀ᶠ m : ℕ in atTop, widthSq * tail m < ε :=
htail_zero.eventually_lt_const hε
filter_upwards [htail_small, eventually_atTop.2 ⟨1, fun m hm ↦ by omega⟩] with m htail_m hm
let d : EmpiricalSideProcedure X C m l u := fun x z ↦
decision (select (empiricalPmf C hm z)) x
have hrisk_pointwise (theta : Theta) (z : Fin m → C) :
finiteSquaredRisk p tau
(decision (select (empiricalPmf C hm z))) theta ≤
value + ε +
(if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then widthSq else 0) := by
by_cases hbad : η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta)
· rw [if_pos hbad]
have hlocalUpper := finiteSquaredRisk_bounds p tau
(fun theta x ↦ (hp theta).1 x) (fun theta ↦ (hp theta).2)
hlu htau_mem (decision (select (empiricalPmf C hm z))) theta |>.2
have hvalue_nonneg : 0 ≤ value := by
dsimp [value]
unfold exactSideMinimaxValue
apply minimaxValue_nonneg
intro d' theta'
unfold exactSideRisk
exact sum_nonneg fun x _ ↦ mul_nonneg ((hp theta').1 x) (sq_nonneg _)
linarith
· rw [if_neg hbad, add_zero]
have hgood : empiricalL1 C hm z (sidePmf q hq theta) < η / 2 :=
lt_of_not_ge hbad
obtain ⟨i, hi⟩ := hcover theta
have hemp_center :
dist (empiricalPmf C hm z) (sidePmf q hq (center i)) < radius i - η / 2 := by
calc
dist (empiricalPmf C hm z) (sidePmf q hq (center i)) ≤
dist (empiricalPmf C hm z) (sidePmf q hq theta) +
dist (sidePmf q hq theta) (sidePmf q hq (center i)) := dist_triangle _ _ _
_ < η / 2 + (radius i - η) :=
add_lt_add
((dist_empiricalPmf_le_empiricalL1 C hm z
(sidePmf q hq theta)).trans_lt hgood) hi
_ = radius i - η / 2 := by ring
have hselected := hselect (empiricalPmf C hm z) ⟨i, hemp_center⟩
have htrue_selected :
dist (sidePmf q hq theta)
(sidePmf q hq (center (select (empiricalPmf C hm z)))) <
radius (select (empiricalPmf C hm z)) := by
calc
dist (sidePmf q hq theta)
(sidePmf q hq (center (select (empiricalPmf C hm z)))) ≤
dist (sidePmf q hq theta) (empiricalPmf C hm z) +
dist (empiricalPmf C hm z)
(sidePmf q hq (center (select (empiricalPmf C hm z)))) := dist_triangle _ _ _
_ < η / 2 + (radius (select (empiricalPmf C hm z)) - η / 2) := by
apply add_lt_add
· simpa [dist_comm] using
(dist_empiricalPmf_le_empiricalL1 C hm z
(sidePmf q hq theta)).trans_lt hgood
· exact hselected
_ = radius (select (empiricalPmf C hm z)) := by ring
simpa [value] using hrisk (select (empiricalPmf C hm z)) theta htrue_selected
have hrisk_d (theta : Theta) :
empiricalSideRisk p q hq tau m d theta ≤ value + ε + widthSq * tail m := by
have hrearrange :
empiricalSideRisk p q hq tau m d theta =
∑ z : Fin m → C, productProbability C (sidePmf q hq theta) z *
finiteSquaredRisk p tau
(decision (select (empiricalPmf C hm z))) theta := by
unfold empiricalSideRisk finiteSquaredRisk
simp only [d]
simp_rw [Finset.mul_sum]
rw [Finset.sum_comm]
apply Finset.sum_congr rfl
intro z _
apply Finset.sum_congr rfl
intro x _
ring
rw [hrearrange]
calc
(∑ z : Fin m → C, productProbability C (sidePmf q hq theta) z *
finiteSquaredRisk p tau
(decision (select (empiricalPmf C hm z))) theta) ≤
∑ z : Fin m → C, productProbability C (sidePmf q hq theta) z *
(value + ε +
if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then widthSq else 0) := by
apply Finset.sum_le_sum
intro z _
exact mul_le_mul_of_nonneg_left (hrisk_pointwise theta z)
(productProbability_nonneg C (sidePmf q hq theta) z)
_ = value + ε + widthSq *
(∑ z : Fin m → C,
if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then
productProbability C (sidePmf q hq theta) z else 0) := by
have hconst :
(∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z * (value + ε)) =
value + ε := by
rw [← Finset.sum_mul, sum_productProbability, one_mul]
have hbadfactor :
(∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z *
(if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then
widthSq else 0)) =
widthSq * (∑ z : Fin m → C,
if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then
productProbability C (sidePmf q hq theta) z else 0) := by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro z _
by_cases hz : η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) <;>
simp [hz, mul_comm]
rw [show (∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z *
(value + ε +
if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then
widthSq else 0)) =
(∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z * (value + ε)) +
∑ z : Fin m → C,
productProbability C (sidePmf q hq theta) z *
(if η / 2 ≤ empiricalL1 C hm z (sidePmf q hq theta) then
widthSq else 0) by
simp_rw [mul_add]
exact Finset.sum_add_distrib]
rw [hconst, hbadfactor]
_ ≤ value + ε + widthSq * tail m := by
simpa [tail, add_comm] using
(add_le_add_left
(mul_le_mul_of_nonneg_left
(empiricalL1_tail C hm (sidePmf q hq theta) (half_pos hη)) hwidthSq)
(value + ε))
unfold empiricalSideMinimaxValue
calc
minimaxValue (empiricalSideRisk p q hq tau m) ≤
worstCaseRisk (empiricalSideRisk p q hq tau m) d :=
minimaxValue_le_worstCaseRisk_of_nonneg (hemp_nonneg m) d
_ ≤ value + ε + widthSq * tail m := Causalean.Stat.worstCaseRisk_le hrisk_d
_ ≤ y := by
dsimp [ε, value] at htail_m ⊢
linarith
1 supporting declaration (lemmas, instances)
-
finiteCover_approximateDecisiontheorem — On a compact parameter space, under continuous simplex-valid label and side coordinates and a continuous bounded target, every positive tolerance admits a finite family of local decisions: smaller side-law balls cover the model with a uniform positive margin, and each decision has risk within the tolerance of the exact-side minimax value throughout its larger ball.hypothesesTheta :sharedType u_1X :sharedType u_2C :sharedType u_3l :sharedℝu :sharedℝp :Theta → X → ℝq :Theta → C → ℝtau :Theta → ℝhp :∀ theta, p theta ∈ stdSimplex ℝ Xhq :∀ theta, q theta ∈ stdSimplex ℝ Chpcont :∀ x, Continuous (fun theta ↦ p theta x)hqcont :∀ c, Continuous (fun theta ↦ q theta c)htau :Continuous tauhlu :l ≤ uhtau_mem :∀ theta, tau theta ∈ Icc l uε :ℝhε :0 < εconclusion∃ (k : ℕ) (hk : 0 < k) (center : Fin k → Theta) (decision : Fin k → BoundedDecision X l u) (radius : Fin k → ℝ) (η : ℝ),0 < ηconclusion 1i :η < radius iconclusion 3finiteSquaredRisk p tau (decision i) theta ≤ exactSideMinimaxValue p q hq tau l u + εProof (Lean source)
theorem finiteCover_approximateDecision (p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hpcont : ∀ x, Continuous (fun theta ↦ p theta x)) (hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) (htau : Continuous tau) (hlu : l ≤ u) (htau_mem : ∀ theta, tau theta ∈ Icc l u) {ε : ℝ} (hε : 0 < ε) : ∃ (k : ℕ) (hk : 0 < k) (center : Fin k → Theta) (decision : Fin k → BoundedDecision X l u) (radius : Fin k → ℝ) (η : ℝ), 0 < η ∧ (∀ i, η < radius i) ∧ (∀ theta, ∃ i, dist (sidePmf q hq theta) (sidePmf q hq (center i)) < radius i - η) ∧ (∀ i theta, dist (sidePmf q hq theta) (sidePmf q hq (center i)) < radius i → finiteSquaredRisk p tau (decision i) theta ≤ exactSideMinimaxValue p q hq tau l u + ε) := by -- Proof plan: shrinking-fiber convergence yields one good radius and decision at each center; -- `exactSideMinimaxValue_eq_iSup_fiber` bounds every fiber value by the exact benchmark. -- For each center, apply `localMinimaxValue_tendsto_fiber` and then `ciInf_lt_iff` to choose -- a positive reciprocal radius and a decision whose worst-case risk on the corresponding closed -- side-law ball is strictly below the benchmark plus ε. The open balls of half those radii cover -- `univ`; use `IsCompact.elim_finite_subcover` to obtain a nonempty `Finset` of centers, enumerate -- it by `Fin k`, and take η to be the minimum of their positive half-radii. This gives both the -- strict cover margin and the larger-ball risk guarantee. The risk bounds in `Risk.lean` discharge -- all conditional-completeness hypotheses for `worstCaseRisk` and `minimaxValue`. classical letI : Nonempty (BoundedDecision X l u) := ⟨fun _ ↦ ⟨l, le_rfl, hlu⟩⟩ have hrisk (d : BoundedDecision X l u) (theta : Theta) : 0 ≤ finiteSquaredRisk p tau d theta ∧ finiteSquaredRisk p tau d theta ≤ (u - l) ^ 2 := finiteSquaredRisk_bounds p tau (fun theta x ↦ (hp theta).1 x) (fun theta ↦ (hp theta).2) hlu htau_mem d theta let d0 : BoundedDecision X l u := fun _ ↦ ⟨l, le_rfl, hlu⟩ have hfiber_bdd : BddAbove (range (fun theta0 : Theta ↦ fiberMinimaxValue p tau q hq l u theta0)) := by refine ⟨(u - l) ^ 2, ?_⟩ rintro _ ⟨theta0, rfl⟩ let fiberRisk := fun (d : BoundedDecision X l u) (theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}) ↦ finiteSquaredRisk p tau d theta.1 letI : Nonempty {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0} := ⟨⟨theta0, rfl⟩⟩ have hnonneg : ∀ (d : BoundedDecision X l u) (theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}), 0 ≤ fiberRisk d theta := fun d theta ↦ (hrisk d theta.1).1 have hupper : ∀ theta : {theta : Theta // sidePmf q hq theta = sidePmf q hq theta0}, fiberRisk d0 theta ≤ (u - l) ^ 2 := fun theta ↦ (hrisk d0 theta.1).2 unfold fiberMinimaxValue calc minimaxValue fiberRisk ≤ worstCaseRisk fiberRisk d0 := minimaxValue_le_worstCaseRisk_of_nonneg (risk := fiberRisk) hnonneg d0 _ ≤ (u - l) ^ 2 := worstCaseRisk_le hupper have hfiber_le_exact (theta0 : Theta) : fiberMinimaxValue p tau q hq l u theta0 ≤ exactSideMinimaxValue p q hq tau l u := by rw [exactSideMinimaxValue_eq_iSup_fiber p q tau hp hq hpcont hqcont htau hlu htau_mem] exact le_ciSup hfiber_bdd theta0 have hlocal (theta0 : Theta) : ∃ (d : BoundedDecision X l u) (r : ℝ), 0 < r ∧ ∀ theta, dist (sidePmf q hq theta) (sidePmf q hq theta0) < r → finiteSquaredRisk p tau d theta ≤ exactSideMinimaxValue p q hq tau l u + ε := by have hconv := localMinimaxValue_tendsto_fiber p q tau hp hq hpcont hqcont htau hlu htau_mem theta0 have heventually : ∀ᶠ n : ℕ in atTop, localMinimaxValue p tau q hq l u (1 / (n + 1 : ℝ)) theta0 < fiberMinimaxValue p tau q hq l u theta0 + ε / 2 := hconv.eventually_lt_const (by linarith) obtain ⟨n, hn⟩ := heventually.exists let r : ℝ := 1 / (n + 1 : ℝ) have hr : 0 < r := by dsimp [r] positivity let localRisk := fun (d : BoundedDecision X l u) (theta : {theta : Theta // dist (sidePmf q hq theta) (sidePmf q hq theta0) ≤ r}) ↦ finiteSquaredRisk p tau d theta.1 letI : Nonempty {theta : Theta // dist (sidePmf q hq theta) (sidePmf q hq theta0) ≤ r} := ⟨⟨theta0, by simp [hr.le]⟩⟩ have hbddBelow : BddBelow (range (worstCaseRisk localRisk)) := bddBelow_range_worstCaseRisk (fun d theta ↦ (hrisk d theta.1).1) have hvalue : (⨅ d, worstCaseRisk localRisk d) < exactSideMinimaxValue p q hq tau l u + ε := by have hn' : localMinimaxValue p tau q hq l u r theta0 < fiberMinimaxValue p tau q hq l u theta0 + ε / 2 := by simpa [r] using hn have hlocal_lt : localMinimaxValue p tau q hq l u r theta0 < exactSideMinimaxValue p q hq tau l u + ε := by linarith [hfiber_le_exact theta0] simpa [localMinimaxValue, minimaxValue, localRisk] using hlocal_lt obtain ⟨d, hd⟩ := (ciInf_lt_iff hbddBelow).1 hvalue refine ⟨d, r, hr, ?_⟩ intro theta htheta have hbddAbove : BddAbove (range (localRisk d)) := by refine ⟨(u - l) ^ 2, ?_⟩ rintro _ ⟨theta', rfl⟩ exact (hrisk d theta'.1).2 have hpoint := le_worstCaseRisk hbddAbove (⟨theta, htheta.le⟩ : {theta : Theta // dist (sidePmf q hq theta) (sidePmf q hq theta0) ≤ r}) exact (hpoint.trans_lt hd).le let chosenDecision : Theta → BoundedDecision X l u := fun theta ↦ choose (hlocal theta) let chosenRadius : Theta → ℝ := fun theta ↦ choose (Classical.choose_spec (hlocal theta)) have hchosen (theta0 : Theta) : 0 < chosenRadius theta0 ∧ ∀ theta, dist (sidePmf q hq theta) (sidePmf q hq theta0) < chosenRadius theta0 → finiteSquaredRisk p tau (chosenDecision theta0) theta ≤ exactSideMinimaxValue p q hq tau l u + ε := Classical.choose_spec (Classical.choose_spec (hlocal theta0)) let U : Theta → Set Theta := fun theta0 ↦ (sidePmf q hq) ⁻¹' ball (sidePmf q hq theta0) (chosenRadius theta0 / 2) have hsideCont : Continuous (sidePmf q hq) := continuous_sidePmf q hq hqcont have hUopen (theta0 : Theta) : IsOpen (U theta0) := Metric.isOpen_ball.preimage hsideCont have hUcover (theta : Theta) : theta ∈ U theta := by simp [U, hchosen theta |>.1] obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover U hUopen (fun theta _ ↦ Set.mem_iUnion.mpr ⟨theta, hUcover theta⟩) have ht_nonempty : t.Nonempty := by let theta : Theta := choice inferInstance obtain ⟨theta0, htheta0t, _⟩ := Set.mem_iUnion₂.mp (ht (Set.mem_univ theta)) exact ⟨theta0, htheta0t⟩ let halfRadius : Theta → ℝ := fun theta ↦ chosenRadius theta / 2 obtain ⟨thetaMin, hthetaMin, hmin⟩ := Finset.exists_min_image t halfRadius ht_nonempty refine ⟨t.card, Finset.card_pos.mpr ht_nonempty, fun i ↦ (t.equivFin.symm i).1, fun i ↦ chosenDecision (t.equivFin.symm i).1, fun i ↦ chosenRadius (t.equivFin.symm i).1, halfRadius thetaMin, ?_, ?_, ?_, ?_⟩ · exact half_pos (hchosen thetaMin).1 · intro i have hhalf_le := hmin (t.equivFin.symm i).1 (t.equivFin.symm i).2 dsimp [halfRadius] at hhalf_le ⊢ linarith [(hchosen (t.equivFin.symm i).1).1] · intro theta obtain ⟨theta0, htheta0t, hthetaU⟩ := Set.mem_iUnion₂.mp (ht (Set.mem_univ theta)) let i : Fin t.card := t.equivFin ⟨theta0, htheta0t⟩ refine ⟨i, ?_⟩ have hi : (t.equivFin.symm i).1 = theta0 := by exact congrArg val (t.equivFin.symm_apply_apply ⟨theta0, htheta0t⟩) have hdist : dist (sidePmf q hq theta) (sidePmf q hq theta0) < chosenRadius theta0 / 2 := by simpa [U, Metric.mem_ball] using hthetaU have heta_le : halfRadius thetaMin ≤ chosenRadius theta0 / 2 := by exact hmin theta0 htheta0t dsimp [i] rw [hi] dsimp [halfRadius] at heta_le ⊢ linarith · intro i theta htheta exact (hchosen (t.equivFin.symm i).1).2 theta htheta
Concentration 4 core · 5 supporting This module defines empirical atom frequencies and proves a uniform L1 tail bound from coordinatewise Hoeffding inequalities and a finite union bound. ★ empiricalL1_tail
Finite-category empirical concentration
This module defines empirical atom frequencies and proves a uniform L1 tail bound from coordinatewise Hoeffding inequalities and a finite union bound.
def empiricalFrequency reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a positive sample size, an ordered finite sample, and an atom, the empirical atom frequency is its sample count divided by the sample size.
Definition (Lean source)
parameters
def
empiricalFrequency C hm z c :
ℝ
given by
(∑ i, if z i = c then (1 : ℝ) else 0) / m
def empiricalL1 reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a positive sample size, a sample, and a side law, the empirical L1 error is the sum of the absolute atom-frequency errors.
Definition (Lean source)
def empiricalPmf reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
A positive finite sample determines the probability-simplex point whose coordinates are its empirical atom frequencies.
Definition (Lean source)
parameters
def
given by
⟨empiricalFrequency C hm z, ⟨empiricalFrequency_nonneg C hm z, sum_empiricalFrequency C hm z⟩⟩
theorem empiricalL1_tail reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
For a finite nonempty alphabet, a probability vector, a positive sample size, and a positive tolerance, the total product probability of samples whose empirical L1 error is at least the tolerance is at most the finite-union Hoeffding bound 2 |C| exp (-2 m (ε/|C|)^2).
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem empiricalL1_tail [Nonempty C] {m : ℕ} (hm : 0 < m) (w : FinitePmf C)
{ε : ℝ} (hε : 0 < ε) :
(∑ z : Fin m → C,
if ε ≤ empiricalL1 C hm z w then productProbability C w z else 0)
≤ 2 * card C * exp (-2 * m * (ε / card C) ^ 2) := by
open Causalean.Stat in
letI : MeasurableSpace C := ⊤
have hw : ∑ c, ofReal (w.1 c) = 1 := by
rw [← ENNReal.ofReal_sum_of_nonneg
(fun c _ ↦ FinitePmf.nonneg C w c),
FinitePmf.sum_eq_one C w]
norm_num
let p : PMF C := PMF.ofFintype (fun c ↦ ofReal (w.1 c)) hw
let P : Measure C := p.toMeasure
haveI : IsProbabilityMeasure P := inferInstance
have hP (c : C) : P.real {c} = w.1 c := by
change toReal (p.toMeasure {c}) = w.1 c
rw [PMF.toMeasure_apply_fintype]
simp [p, FinitePmf.nonneg C w c]
have hint (c : C) :
(∫ x, (if x = c then (1 : ℝ) else 0) ∂P) = w.1 c := by
rw [show (fun x ↦ if x = c then (1 : ℝ) else 0) =
indicator {c} (1 : C → ℝ) by
funext x
by_cases h : x = c <;> simp [h]]
rw [MeasureTheory.integral_indicator_one (measurableSet_singleton c)]
exact hP c
let S := iidSample_infinitePi P
let μ : Measure (ℕ → C) := Measure.infinitePi (fun _ : ℕ ↦ P)
let Φ : (ℕ → C) → (Fin m → C) := fun ω i ↦ ω i
have hmean (c : C) (ω : ℕ → C) :
S.sampleMean (fun x ↦ if x = c then (1 : ℝ) else 0) m ω =
empiricalFrequency C hm (Φ ω) c := by
rw [IIDSample.sampleMean, empiricalFrequency,
Fin.sum_univ_eq_sum_range (fun i ↦ if ω i = c then (1 : ℝ) else 0) m]
simp only [S, Φ, iidSample_infinitePi]
ring
let A : C → Set (ℕ → C) := fun c ↦
{ω | ε / card C ≤
|empiricalFrequency C hm (Φ ω) c - w.1 c|}
have hcoord (c : C) :
μ.real (A c) ≤ 2 * exp (-2 * m * (ε / card C) ^ 2) := by
have hb : ∀ᵐ x ∂P, (if x = c then (1 : ℝ) else 0) ∈ Icc 0 1 := by
filter_upwards with x
by_cases hx : x = c <;> simp [hx]
have hh := hoeffding_abs_ge S
(f := fun x ↦ if x = c then (1 : ℝ) else 0)
(by fun_prop) (a := 0) (b := 1) zero_lt_one hb m hm
(div_nonneg (le_of_lt hε)
(by positivity : (0 : ℝ) ≤ card C))
rw [hint c] at hh
simpa only [μ, hmean, sub_zero, one_pow, div_one, A] using hh
let B : Set (ℕ → C) := {ω | ε ≤ empiricalL1 C hm (Φ ω) w}
have hsub : B ⊆ ⋃ c, A c := by
intro ω hω
rcases exists_large_empirical_coordinate C hm (Φ ω) w hω with ⟨c, hc⟩
exact Set.mem_iUnion.2 ⟨c, hc⟩
have hB : μ.real B ≤
2 * card C * exp (-2 * m * (ε / card C) ^ 2) := by
calc
μ.real B ≤ μ.real (⋃ c, A c) := measureReal_mono hsub
_ ≤ ∑ c, μ.real (A c) := measureReal_iUnion_fintype_le μ A
_ ≤ ∑ _c : C, 2 * exp
(-2 * m * (ε / card C) ^ 2) :=
Finset.sum_le_sum fun c _ ↦ hcoord c
_ = 2 * card C * exp
(-2 * m * (ε / card C) ^ 2) := by
rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
ring
let E : Finset (Fin m → C) :=
Finset.univ.filter (fun z ↦ ε ≤ empiricalL1 C hm z w)
have hmap : μ.map Φ = Measure.pi (fun _ : Fin m ↦ P) := by
simpa only [μ, Φ, S, iidSample_infinitePi] using iidSample_finN_pushforward S m
have hBE : B = Φ ⁻¹' (E : Set (Fin m → C)) := by
ext ω
simp only [B, E, Φ, Set.mem_ofPred_eq, Set.mem_preimage, Finset.mem_coe,
mem_filter, Finset.mem_univ, true_and]
have htransport :
μ.real B = (Measure.pi (fun _ : Fin m ↦ P)).real (E : Set (Fin m → C)) := by
simp only [Measure.real]
congr 1
rw [hBE, ← Measure.map_apply (by fun_prop) (by measurability), hmap]
have hsingleton (z : Fin m → C) :
(Measure.pi (fun _ : Fin m ↦ P)).real {z} = productProbability C w z := by
simp only [Measure.real, Measure.pi_singleton]
rw [ENNReal.toReal_prod]
change (∏ i, P.real {z i}) = _
simp_rw [hP]
rfl
have hsumE :
(∑ z : Fin m → C,
if ε ≤ empiricalL1 C hm z w then productProbability C w z else 0) =
(Measure.pi (fun _ : Fin m ↦ P)).real (E : Set (Fin m → C)) := by
rw [← Finset.sum_filter]
calc
∑ z ∈ E, productProbability C w z =
∑ z ∈ E, (Measure.pi (fun _ : Fin m ↦ P)).real {z} := by
apply Finset.sum_congr rfl
intro z _
exact (hsingleton z).symm
_ = (Measure.pi (fun _ : Fin m ↦ P)).real (E : Set (Fin m → C)) :=
MeasureTheory.sum_measureReal_singleton E
rw [hsumE, ← htransport]
exact hB
5 supporting declarations (lemmas, instances)
-
empiricalFrequency_nonnegtheorem — Every empirical atom frequency is nonnegative.hypothesesconclusion0 ≤ empiricalFrequency C hm z cProof (Lean source)
theorem empiricalFrequency_nonneg {m : ℕ} (hm : 0 < m) (z : Fin m → C) (c : C) : 0 ≤ empiricalFrequency C hm z c := by unfold empiricalFrequency exact div_nonneg (sum_nonneg fun _ _ ↦ by positivity) (Nat.cast_nonneg _) -
sum_empiricalFrequencytheorem — Over a finite nonempty alphabet, the empirical atom frequencies of a positive sample sum to one.hypothesesconclusion∑ c, empiricalFrequency C hm z c = 1Proof (Lean source)
theorem sum_empiricalFrequency [Nonempty C] {m : ℕ} (hm : 0 < m) (z : Fin m → C) : ∑ c, empiricalFrequency C hm z c = 1 := by unfold empiricalFrequency rw [← Finset.sum_div, Finset.sum_comm] simp [Finset.sum_ite_eq, Nat.ne_of_gt hm] -
empiricalPmf_applytheorem — Given a positive sample size, a sample, and an atom, the corresponding empirical probability-vector coordinate equals the empirical frequency.hypothesesconclusion(empiricalPmf C hm z).1 c = empiricalFrequency C hm z cProof (Lean source)
@[simp] theorem empiricalPmf_apply [Nonempty C] {m : ℕ} (hm : 0 < m) (z : Fin m → C) (c : C) : (empiricalPmf C hm z).1 c = empiricalFrequency C hm z c := rfl -
dist_empiricalPmf_le_empiricalL1theorem — For a finite nonempty alphabet, a positive sample, and a probability vector, the distance from the empirical simplex point to the vector is at most their coordinatewise L1 error.hypothesesconclusionProof (Lean source)
theorem dist_empiricalPmf_le_empiricalL1 [Nonempty C] {m : ℕ} (hm : 0 < m) (z : Fin m → C) (w : FinitePmf C) : dist (empiricalPmf C hm z) w ≤ empiricalL1 C hm z w := by change dist (empiricalFrequency C hm z) w.1 ≤ ∑ c, |empiricalFrequency C hm z c - w.1 c| rw [dist_pi_le_iff'] intro c rw [Real.dist_eq] exact Finset.single_le_sum (s := univ) (f := fun c ↦ |empiricalFrequency C hm z c - w.1 c|) (fun c _ ↦ abs_nonneg _) (Finset.mem_univ c) -
empiricalL1_tail_bound_tendsto_zerotheorem — For every positive tolerance, the uniform finite-category empirical L1 tail bound tends to zero as the sample size tends to infinity.hypothesesC :sharedType u_1Nonempty Cε :ℝhε :0 < εProof (Lean source)
theorem empiricalL1_tail_bound_tendsto_zero [Nonempty C] {ε : ℝ} (hε : 0 < ε) : Tendsto (fun m : ℕ ↦ 2 * Fintype.card C * exp (-2 * m * (ε / Fintype.card C) ^ 2)) atTop (nhds 0) := by have hcard : (0 : ℝ) < Fintype.card C := by exact_mod_cast Fintype.card_pos have ha : 0 < 2 * (ε / (Fintype.card C : ℝ)) ^ 2 := by positivity have harg : Tendsto (fun m : ℕ ↦ (m : ℝ) * (2 * (ε / (Fintype.card C : ℝ)) ^ 2)) atTop atTop := (tendsto_natCast_atTop_atTop (R := ℝ)).atTop_mul_const ha have hexp : Tendsto (fun m : ℕ ↦ exp (-((m : ℝ) * (2 * (ε / (Fintype.card C : ℝ)) ^ 2)))) atTop (nhds 0) := Real.tendsto_exp_neg_atTop_nhds_zero.comp harg have hmul := hexp.const_mul (2 * (Fintype.card C : ℝ)) convert hmul using 1 · funext m congr 2 ring · simp
Main 1 core · 0 supporting This module proves that bounded squared-loss minimax values based on finitely many iid observations from a finite side law converge to the minimax value in the experiment that reveals that side-law vector exactly. ★ finiteSideInfo_minimax_tendsto
Finite side-information minimax convergence
This module proves that bounded squared-loss minimax values based on finitely many iid observations from a finite side law converge to the minimax value in the experiment that reveals that side-law vector exactly.
theorem finiteSideInfo_minimax_tendsto reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
For a compact parameter space, finite labeled and finite nonempty side alphabets, continuous simplex-valid label and side probabilities, and a continuous target contained in an ordered bounded action interval, the bounded squared-loss empirical-side minimax values converge to the exact-side minimax benchmark as the iid side sample size tends to infinity.
Formal statement
hypotheses
l :
ℝ
u :
ℝ
Theta X C :
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
hp :
hq :
hpcont :
hqcont :
htau :
Continuous tau
hlu :
l ≤ u
conclusion
Tendsto (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop (nhds (exactSideMinimaxValue p q hq tau l u))
Proof (Lean source)
theorem finiteSideInfo_minimax_tendsto
{Theta X C : Type*} [TopologicalSpace Theta] [CompactSpace Theta] [Nonempty Theta]
[Fintype X] [Fintype C] [DecidableEq C] [Nonempty C]
(p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C)
(hpcont : ∀ x, Continuous (fun theta ↦ p theta x))
(hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) (htau : Continuous tau)
(hlu : l ≤ u) (htau_mem : ∀ theta, tau theta ∈ Icc l u) :
Tendsto (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop
(nhds (exactSideMinimaxValue p q hq tau l u)) := by
apply tendsto_order.2
constructor
· intro a ha
exact Filter.Eventually.of_forall fun m ↦
ha.trans_le
(exactSideMinimaxValue_le_empiricalSideMinimaxValue
p q tau hp hq hlu htau_mem m)
· intro b hb
have hemp_nonneg (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (theta : Theta) :
0 ≤ empiricalSideRisk p q hq tau m d theta :=
empiricalSideRisk_nonneg p q hp hq tau m d theta
have hminimax_le (m : ℕ) :
empiricalSideMinimaxValue p q hq tau l u m ≤ (u - l) ^ 2 := by
let d0 : EmpiricalSideProcedure X C m l u := fun _ _ ↦ ⟨l, le_rfl, hlu⟩
unfold empiricalSideMinimaxValue
calc
minimaxValue (empiricalSideRisk p q hq tau m) ≤
worstCaseRisk (empiricalSideRisk p q hq tau m) d0 :=
minimaxValue_le_worstCaseRisk_of_nonneg (hemp_nonneg m) d0
_ ≤ (u - l) ^ 2 := Causalean.Stat.worstCaseRisk_le fun theta ↦
empiricalSideRisk_le p q hp hq tau hlu htau_mem m d0 theta
have hbounded : Filter.IsBoundedUnder (fun x y : ℝ ↦ x ≤ y) atTop
(fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) :=
Filter.isBoundedUnder_of_eventually_le (Filter.Eventually.of_forall hminimax_le)
exact Filter.eventually_lt_of_limsup_lt
((empiricalSideMinimax_limsup_le_exact
p q tau hp hq hpcont hqcont htau hlu htau_mem).trans_lt hb) hbounded
Measurable 10 core · 21 supporting This module connects finite-sample side-information procedures with globally measurable bounded procedures on ambient probability-coordinate tables. ★ measurableExactTableMinimax_squeeze
Measurable finite-side-information minimax bridge
This module connects finite-sample side-information procedures with globally measurable bounded procedures on ambient probability-coordinate tables. It proves polynomial continuity of conditional averaging, clipped measurable extension from the finite simplex, finite-product integral identities, and the minimax comparison that is stable under surjective reparameterization.
def conditionalAveragePolynomial reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a side-sample size, an empirical procedure, and a label, the conditional-average polynomial is the finite sum of action-weighted sample monomials.
Definition (Lean source)
parameters
X :
Type u_1
C :
Type u_2
l :
ℝ
u :
ℝ
m :
ℕ
d :
EmpiricalSideProcedure X C m l u
x :
X
def
abbrev AmbientExactSideProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a label alphabet, a side alphabet, and action bounds, an ambient exact-table procedure is the function assigning a bounded action to each label and arbitrary real side-coordinate table.
def IsContinuousAmbientExactSideProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given an ambient exact-table procedure, the continuity property requires every fixed-label section to vary continuously with its real coordinate table.
Definition (Lean source)
parameters
X :
Type u_1
C :
Type u_2
l :
ℝ
u :
ℝ
d :
AmbientExactSideProcedure X C l u
x :
def
IsContinuousAmbientExactSideProcedure d :
Prop
given by
Continuous (d x)
def IsMeasurableAmbientExactSideProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given an ambient exact-table procedure, the measurability property requires every fixed-label section to be Borel measurable in its real coordinate table.
Definition (Lean source)
parameters
X :
Type u_1
C :
Type u_2
l :
ℝ
u :
ℝ
d :
AmbientExactSideProcedure X C l u
x :
def
IsMeasurableAmbientExactSideProcedure d :
Prop
given by
Measurable (d x)
def finitePmfDesign reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a finite probability vector, the corresponding finite randomization design is the design with exactly those atom probabilities.
Definition (Lean source)
parameters
C :
Type u_2
w :
def
given by
clause 1
p := w.1
clause 2
p_nonneg := w.nonneg
clause 3
p_sum := w.sum_eq_one
def finitePmfMeasure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a finite probability vector, the finite-PMF measure is the atomic probability measure with those atom masses.
Definition (Lean source)
parameters
w :
def
given by
abbrev MeasurableAmbientExactSideProcedure reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a label alphabet, a finite side alphabet, and action bounds, a measurable ambient exact-table procedure is an ambient bounded rule equipped with Borel measurability of every label section.
Definition (Lean source)
parameters
X C :
Type*
Fintype C
l u :
ℝ
def
given by
{d : AmbientExactSideProcedure X C l u // IsMeasurableAmbientExactSideProcedure d}
def measurableExactTableRisk reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label probabilities, side-coordinate probabilities, a target, a measurable ambient procedure, and a parameter, the measurable exact-table risk is the label-probability-weighted squared loss after evaluating the procedure at that parameter's raw side-coordinate table.
Definition (Lean source)
parameters
Theta :
Type u_4
X :
Type u_5
C :
Type u_6
l :
ℝ
u :
ℝ
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
d :
theta :
Theta
def
measurableExactTableRisk p q tau d theta :
ℝ
given by
∑ x, p theta x * ((d.1 x (q theta) : ℝ) - tau theta) ^ 2
def measurableExactTableMinimaxValue reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given label probabilities, side-coordinate probabilities, a target, and action bounds, the measurable exact-table minimax value is the infimum of worst-case squared risks over globally Borel-measurable bounded ambient procedures.
Definition (Lean source)
parameters
Theta :
Type u_4
X :
Type u_5
C :
Type u_6
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
l u :
ℝ
def
measurableExactTableMinimaxValue p q tau l u :
ℝ
given by
minimaxValue (measurableExactTableRisk p q tau : MeasurableAmbientExactSideProcedure X C l u → Theta → ℝ)
theorem measurableExactTableMinimax_squeeze reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given simplex-valid label and side probabilities, a target, ordered action bounds, and target containment in those bounds, the measurable exact-table minimax value lies between the exact-side value and every empirical-side value.
Formal statement
hypotheses
Theta :
Type u_4
X :
Type u_5
C :
Type u_6
l :
ℝ
u :
ℝ
Nonempty Theta
p :
Theta → X → ℝ
q :
Theta → C → ℝ
tau :
Theta → ℝ
hp :
hq :
hlu :
l ≤ u
conclusion
conclusion 1
exactSideMinimaxValue p q hq tau l u ≤ measurableExactTableMinimaxValue p q tau l u
conclusion 2
m :
measurableExactTableMinimaxValue p q tau l u ≤ empiricalSideMinimaxValue p q hq tau l u m
Proof (Lean source)
theorem measurableExactTableMinimax_squeeze [Nonempty Theta]
(p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C)
(hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) :
exactSideMinimaxValue p q hq tau l u ≤
measurableExactTableMinimaxValue p q tau l u ∧
∀ m, measurableExactTableMinimaxValue p q tau l u ≤
empiricalSideMinimaxValue p q hq tau l u m := by
exact ⟨exactSideMinimaxValue_le_measurableExactTableMinimaxValue
p q tau hp hq hlu htau,
fun m ↦ measurableExactTableMinimaxValue_le_empiricalSideMinimaxValue
p q tau hp hq hlu htau m⟩
21 supporting declarations (lemmas, instances)
-
eval_conditionalAveragePolynomialtheorem — For a side-sample size, empirical procedure, label, and real coordinate table, evaluating the conditional-average polynomial gives the corresponding product-weighted finite sum.hypothesesX :sharedType u_1C :sharedType u_2l :sharedℝu :sharedℝm :ℕd :EmpiricalSideProcedure X C m l ux :Xw :C → ℝconclusioneval w (conditionalAveragePolynomial m d x)= ∑ z : Fin m → C, (∏ i, w (z i)) * (d x z : ℝ)Proof (Lean source)
theorem eval_conditionalAveragePolynomial (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (x : X) (w : C → ℝ) : eval w (conditionalAveragePolynomial m d x) = ∑ z : Fin m → C, (∏ i, w (z i)) * (d x z : ℝ) := by simp [conditionalAveragePolynomial, mul_comm] -
continuous_conditionalAverageProceduretheorem — Given action bounds, a side-sample size, an empirical procedure, and a label, the conditional-average procedure varies continuously with the finite side-law vector.hypothesesconclusionContinuous (conditionalAverageProcedure l u m d x)Proof (Lean source)
theorem continuous_conditionalAverageProcedure (l u : ℝ) (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (x : X) : Continuous (conditionalAverageProcedure l u m d x) := by unfold conditionalAverageProcedure apply Continuous.subtype_mk apply continuous_finsetSum intro z _ have hc : Continuous (fun _ : FinitePmf C ↦ (d x z : ℝ)) := continuous_const exact (continuous_productProbability C z).mul hc -
measurable_conditionalAverageProceduretheorem — Given action bounds, a side-sample size, an empirical procedure, and a label, the conditional-average procedure is Borel measurable in the finite side-law vector.hypothesesconclusionMeasurable (conditionalAverageProcedure l u m d x)Proof (Lean source)
theorem measurable_conditionalAverageProcedure (l u : ℝ) (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (x : X) : Measurable (conditionalAverageProcedure l u m d x) := by exact (continuous_conditionalAverageProcedure l u m d x).measurable -
exists_continuous_clippedExtensiontheorem — Given ordered action bounds, an interval-valued simplex rule, and its continuity, a continuous interval-valued ambient extension agreeing on the simplex exists.hypothesesC :sharedType u_2l :sharedℝu :sharedℝhlu :l ≤ uhf :Proof (Lean source)
theorem exists_continuous_clippedExtension (hlu : l ≤ u) (f : FinitePmf C → Icc l u) (hf : Continuous f) : ∃ g : (C → ℝ) → Icc l u, Continuous g ∧ ∀ w : FinitePmf C, g w.1 = f w := by let fb : BoundedContinuousFunction (FinitePmf C) ℝ := BoundedContinuousFunction.mkOfCompact ⟨fun w ↦ (f w : ℝ), hf.subtype_val⟩ have hfb : ∀ w, fb w ∈ Icc l u := by intro w exact (f w).2 have he : Topology.IsClosedEmbedding ((↑) : FinitePmf C → C → ℝ) := Topology.IsClosedEmbedding.subtypeVal (isClosed_stdSimplex ℝ C) rcases BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_isClosedEmbedding fb hfb hlu he with ⟨g, hg, hgf⟩ let g' : (C → ℝ) → Icc l u := fun w ↦ ⟨g w, hg w⟩ refine ⟨g', g.continuous.subtype_mk _, ?_⟩ intro w apply Subtype.ext exact congrFun hgf w -
exists_continuous_ambientExactSideProceduretheorem — Given ordered action bounds, an exact-side procedure, and continuous label sections, an ambient procedure with continuous sections that agrees on simplex tables exists.hypothesesX :sharedType u_1C :sharedType u_2l :sharedℝu :sharedℝhlu :l ≤ ud :ExactSideProcedure X C l uhd :∀ x, Continuous (d x)conclusion∃ g : AmbientExactSideProcedure X C l u,conclusion 1x (w : FinitePmf C) :g x w.1 = d x wProof (Lean source)
theorem exists_continuous_ambientExactSideProcedure (hlu : l ≤ u) (d : ExactSideProcedure X C l u) (hd : ∀ x, Continuous (d x)) : ∃ g : AmbientExactSideProcedure X C l u, IsContinuousAmbientExactSideProcedure g ∧ ∀ x (w : FinitePmf C), g x w.1 = d x w := by choose g hg_cont hg_eq using fun x ↦ exists_continuous_clippedExtension hlu (d x) (hd x) exact ⟨g, hg_cont, hg_eq⟩ -
exists_measurable_clippedAmbientExactSideProceduretheorem — Given ordered action bounds, an exact-side procedure, and continuous label sections, a Borel-measurable ambient procedure that agrees on simplex tables exists.hypothesesX :sharedType u_1C :sharedType u_2l :sharedℝu :sharedℝhlu :l ≤ ud :ExactSideProcedure X C l uhd :∀ x, Continuous (d x)conclusion∃ g : AmbientExactSideProcedure X C l u,conclusion 1x (w : FinitePmf C) :g x w.1 = d x wProof (Lean source)
theorem exists_measurable_clippedAmbientExactSideProcedure (hlu : l ≤ u) (d : ExactSideProcedure X C l u) (hd : ∀ x, Continuous (d x)) : ∃ g : AmbientExactSideProcedure X C l u, IsMeasurableAmbientExactSideProcedure g ∧ ∀ x (w : FinitePmf C), g x w.1 = d x w := by rcases exists_continuous_ambientExactSideProcedure hlu d hd with ⟨g, hg, hgeq⟩ exact ⟨g, fun x ↦ (hg x).measurable, hgeq⟩ -
integral_finitePmfMeasure_eq_sumtheorem — Given a finite probability vector and a real-valued function, integration against its atomic measure equals the probability-weighted finite sum.hypothesesconclusion∫ c, f c ∂finitePmfMeasure w = ∑ c, w.1 c * f cProof (Lean source)
theorem integral_finitePmfMeasure_eq_sum [MeasurableSpace C] [MeasurableSingletonClass C] (w : FinitePmf C) (f : C → ℝ) : ∫ c, f c ∂finitePmfMeasure w = ∑ c, w.1 c * f c := by simpa [finitePmfMeasure, FiniteDesign.E, finitePmfDesign] using (FiniteDesign.integral_toMeasure (finitePmfDesign w) f) -
pi_finitePmfMeasure_eq_productDesignMeasuretheorem — Given a finite probability vector and sample size, the finite product of its atomic measures equals the product-design measure.hypothesesconclusionMeasure.pi (fun _ : Fin m ↦ finitePmfMeasure w)Proof (Lean source)
theorem pi_finitePmfMeasure_eq_productDesignMeasure [MeasurableSpace C] [MeasurableSingletonClass C] (w : FinitePmf C) (m : ℕ) : Measure.pi (fun _ : Fin m ↦ finitePmfMeasure w) = (prodDesign (fun _ : Fin m ↦ finitePmfDesign w)).toMeasure := by simpa [finitePmfMeasure] using (prodDesign_toMeasure_eq_pi (fun _ : Fin m ↦ finitePmfDesign w)).symm -
integral_pi_finitePmfMeasure_eq_sum_productProbabilitytheorem — Given a finite probability vector, sample size, and real-valued sample function, integration against the iid product measure equals the exact product-probability sum.hypothesesconclusion∫ z, f z ∂Measure.pi (fun _ : Fin m ↦ finitePmfMeasure w)= ∑ z : Fin m → C, productProbability C w z * f zProof (Lean source)
theorem integral_pi_finitePmfMeasure_eq_sum_productProbability [MeasurableSpace C] [MeasurableSingletonClass C] (w : FinitePmf C) (m : ℕ) (f : (Fin m → C) → ℝ) : ∫ z, f z ∂Measure.pi (fun _ : Fin m ↦ finitePmfMeasure w) = ∑ z : Fin m → C, productProbability C w z * f z := by rw [pi_finitePmfMeasure_eq_productDesignMeasure] rw [FiniteDesign.integral_toMeasure] rfl -
exactSideRisk_eq_integraltheorem — Given label probabilities, side probabilities, simplex validity, a target, an exact-side procedure, and a parameter, the exact-side finite-sum risk equals its finite-measure integral representation.hypothesesX :sharedType u_1C :sharedType u_2Theta :sharedType u_3l :sharedℝu :sharedℝp :Theta → X → ℝq :Theta → C → ℝhp :∀ theta, p theta ∈ stdSimplex ℝ Xhq :∀ theta, q theta ∈ stdSimplex ℝ Ctau :Theta → ℝd :ExactSideProcedure X C l utheta :ThetaconclusionexactSideRisk p q hq tau d thetaProof (Lean source)
theorem exactSideRisk_eq_integral (p : Theta → X → ℝ) (q : Theta → C → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (tau : Theta → ℝ) (d : ExactSideProcedure X C l u) (theta : Theta) : exactSideRisk p q hq tau d theta = ∫ x, (((d x (sidePmf q hq theta) : Icc l u) : ℝ) - tau theta) ^ 2 ∂finitePmfMeasure (sidePmf p hp theta) := by rw [integral_finitePmfMeasure_eq_sum] rfl -
empiricalSideRisk_eq_integraltheorem — Given label probabilities, side probabilities, simplex validity, a target, sample size, an empirical procedure, and a parameter, the empirical finite-sum risk equals its iterated product-measure integral representation.hypothesesX :sharedType u_1C :sharedType u_2Theta :sharedType u_3l :sharedℝu :sharedℝp :Theta → X → ℝq :Theta → C → ℝhp :∀ theta, p theta ∈ stdSimplex ℝ Xhq :∀ theta, q theta ∈ stdSimplex ℝ Ctau :Theta → ℝm :ℕd :EmpiricalSideProcedure X C m l utheta :ThetaconclusionempiricalSideRisk p q hq tau m d theta= ∫ x, ∫ z, ((d x z : ℝ) - tau theta) ^ 2 ∂Measure.pi (fun _ : Fin m ↦ finitePmfMeasure (sidePmf q hq theta)) ∂finitePmfMeasure (sidePmf p hp theta)Proof (Lean source)
theorem empiricalSideRisk_eq_integral (p : Theta → X → ℝ) (q : Theta → C → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (tau : Theta → ℝ) (m : ℕ) (d : EmpiricalSideProcedure X C m l u) (theta : Theta) : empiricalSideRisk p q hq tau m d theta = ∫ x, ∫ z, ((d x z : ℝ) - tau theta) ^ 2 ∂Measure.pi (fun _ : Fin m ↦ finitePmfMeasure (sidePmf q hq theta)) ∂finitePmfMeasure (sidePmf p hp theta) := by rw [integral_finitePmfMeasure_eq_sum] simp_rw [integral_pi_finitePmfMeasure_eq_sum_productProbability] rfl -
worstCaseRisk_comp_surjectivetheorem — Given a risk, a fixed procedure, a parameter map, and surjectivity of that map, reindexing leaves the worst-case risk unchanged.hypothesesconclusionworstCaseRisk (fun e a ↦ risk e (phi a)) e = worstCaseRisk risk eProof (Lean source)
theorem worstCaseRisk_comp_surjective {E A B : Type*} (risk : E → B → ℝ) (e : E) (phi : A → B) (hphi : Surjective phi) : worstCaseRisk (fun e a ↦ risk e (phi a)) e = worstCaseRisk risk e := by rw [worstCaseRisk, iSup] congr 1 ext r simp only [Set.mem_range] constructor · rintro ⟨a, rfl⟩ exact ⟨phi a, rfl⟩ · rintro ⟨b, rfl⟩ obtain ⟨a, rfl⟩ := hphi b exact ⟨a, rfl⟩ -
minimaxValue_comp_surjectivetheorem — Given a risk, a parameter map, and surjectivity of that map, reindexing leaves the minimax value unchanged.hypothesesconclusionminimaxValue (fun e a ↦ risk e (phi a)) = minimaxValue riskProof (Lean source)
theorem minimaxValue_comp_surjective {E A B : Type*} (risk : E → B → ℝ) (phi : A → B) (hphi : Surjective phi) : minimaxValue (fun e a ↦ risk e (phi a)) = minimaxValue risk := by unfold minimaxValue congr 1 funext e exact worstCaseRisk_comp_surjective risk e phi hphi -
continuous_coordinateFamily_comptheorem — Given a parameter map, its continuity, a real coordinate family, and continuity of every coordinate, the pulled-back coordinate family is continuous.hypothesesconclusionContinuous (fun a ↦ f (phi a) i)Proof (Lean source)
theorem continuous_coordinateFamily_comp {A B I : Type*} [TopologicalSpace A] [TopologicalSpace B] (phi : A → B) (hphi : Continuous phi) (f : B → I → ℝ) (hf : ∀ i, Continuous (fun b ↦ f b i)) : ∀ i, Continuous (fun a ↦ f (phi a) i) := by intro i exact (hf i).comp hphi -
measurableExactTableMinimaxValue_comp_surjectivetheorem — Given label probabilities, side-coordinate probabilities, a target, action bounds, a surjective parameter map, pulling all model coordinates back leaves the measurable exact-table minimax value unchanged.hypothesesX :sharedType u_5C :sharedType u_6A B :Type*p :B → X → ℝq :B → C → ℝtau :B → ℝl u :ℝphi :A → Bhphi :Surjective phiconclusionmeasurableExactTableMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ tau (phi a)) l u= measurableExactTableMinimaxValue p q tau l uProof (Lean source)
theorem measurableExactTableMinimaxValue_comp_surjective {A B : Type*} (p : B → X → ℝ) (q : B → C → ℝ) (tau : B → ℝ) (l u : ℝ) (phi : A → B) (hphi : Surjective phi) : measurableExactTableMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ tau (phi a)) l u = measurableExactTableMinimaxValue p q tau l u := by unfold measurableExactTableMinimaxValue exact minimaxValue_comp_surjective (measurableExactTableRisk p q tau) phi hphi -
exactSideMinimaxValue_comp_surjectivetheorem — Given label probabilities, side-coordinate probabilities, simplex validity, a target, action bounds, and a surjective parameter map, pulling all model coordinates back leaves the exact-side minimax value unchanged.hypothesesX :sharedType u_5C :sharedType u_6A B :Type*p :B → X → ℝq :B → C → ℝhq :∀ b, q b ∈ stdSimplex ℝ Ctau :B → ℝl u :ℝphi :A → Bhphi :Surjective phiconclusionexactSideMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ hq (phi a)) (fun a ↦ tau (phi a)) l u= exactSideMinimaxValue p q hq tau l uProof (Lean source)
theorem exactSideMinimaxValue_comp_surjective {A B : Type*} (p : B → X → ℝ) (q : B → C → ℝ) (hq : ∀ b, q b ∈ stdSimplex ℝ C) (tau : B → ℝ) (l u : ℝ) (phi : A → B) (hphi : Surjective phi) : exactSideMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ hq (phi a)) (fun a ↦ tau (phi a)) l u = exactSideMinimaxValue p q hq tau l u := by unfold exactSideMinimaxValue exact minimaxValue_comp_surjective (exactSideRisk p q hq tau) phi hphi -
empiricalSideMinimaxValue_comp_surjectivetheorem — Given label probabilities, side-coordinate probabilities, simplex validity, a target, action bounds, a sample size, and a surjective parameter map, pulling all model coordinates back leaves the empirical-side minimax value unchanged.hypothesesX :sharedType u_5C :sharedType u_6A B :Type*p :B → X → ℝq :B → C → ℝhq :∀ b, q b ∈ stdSimplex ℝ Ctau :B → ℝl u :ℝm :ℕphi :A → Bhphi :Surjective phiconclusionempiricalSideMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ hq (phi a)) (fun a ↦ tau (phi a)) l u m= empiricalSideMinimaxValue p q hq tau l u mProof (Lean source)
theorem empiricalSideMinimaxValue_comp_surjective {A B : Type*} (p : B → X → ℝ) (q : B → C → ℝ) (hq : ∀ b, q b ∈ stdSimplex ℝ C) (tau : B → ℝ) (l u : ℝ) (m : ℕ) (phi : A → B) (hphi : Surjective phi) : empiricalSideMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ hq (phi a)) (fun a ↦ tau (phi a)) l u m = empiricalSideMinimaxValue p q hq tau l u m := by unfold empiricalSideMinimaxValue exact minimaxValue_comp_surjective (empiricalSideRisk p q hq tau m) phi hphi -
exactSideMinimaxValue_le_measurableExactTableMinimaxValuetheorem — Given simplex-valid label and side probabilities, a target, ordered action bounds, and target containment in those bounds, the unrestricted exact-side minimax value is at most the measurable ambient exact-table value.hypothesesTheta :sharedType u_4X :sharedType u_5C :sharedType u_6l :sharedℝu :sharedℝNonempty Thetap :Theta → X → ℝq :Theta → C → ℝtau :Theta → ℝhp :hq :hlu :l ≤ uconclusionexactSideMinimaxValue p q hq tau l u ≤ measurableExactTableMinimaxValue p q tau l uProof (Lean source)
theorem exactSideMinimaxValue_le_measurableExactTableMinimaxValue [Nonempty Theta] (p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) : exactSideMinimaxValue p q hq tau l u ≤ measurableExactTableMinimaxValue p q tau l u := by letI : Nonempty (MeasurableAmbientExactSideProcedure X C l u) := ⟨⟨fun _ _ ↦ ⟨l, le_rfl, hlu⟩, fun _ ↦ measurable_const⟩⟩ have hexact_nonneg (d : ExactSideProcedure X C l u) (theta : Theta) : 0 ≤ exactSideRisk p q hq tau d theta := by unfold exactSideRisk exact sum_nonneg fun x _ ↦ mul_nonneg ((hp theta).1 x) (sq_nonneg _) unfold exactSideMinimaxValue measurableExactTableMinimaxValue refine minimaxValue_le_minimaxValue (bddBelow_range_worstCaseRisk hexact_nonneg) ?_ intro d refine ⟨fun x w ↦ d.1 x w.1, ?_⟩ rfl -
measurableExactTableMinimaxValue_le_empiricalSideMinimaxValuetheorem — Given simplex-valid label and side probabilities, a target, ordered action bounds, target containment in those bounds, and a sample size, the measurable ambient exact-table minimax value is at most the empirical-side minimax value.hypothesesTheta :sharedType u_4X :sharedType u_5C :sharedType u_6l :sharedℝu :sharedℝNonempty Thetap :Theta → X → ℝq :Theta → C → ℝtau :Theta → ℝhp :hq :hlu :l ≤ um :ℕconclusionmeasurableExactTableMinimaxValue p q tau l u ≤ empiricalSideMinimaxValue p q hq tau l u mProof (Lean source)
theorem measurableExactTableMinimaxValue_le_empiricalSideMinimaxValue [Nonempty Theta] (p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) (m : ℕ) : measurableExactTableMinimaxValue p q tau l u ≤ empiricalSideMinimaxValue p q hq tau l u m := by letI : Nonempty (EmpiricalSideProcedure X C m l u) := ⟨fun _ _ ↦ ⟨l, le_rfl, hlu⟩⟩ have htable_nonneg (d : MeasurableAmbientExactSideProcedure X C l u) (theta : Theta) : 0 ≤ measurableExactTableRisk p q tau d theta := by unfold measurableExactTableRisk exact sum_nonneg fun x _ ↦ mul_nonneg ((hp theta).1 x) (sq_nonneg _) unfold measurableExactTableMinimaxValue empiricalSideMinimaxValue refine minimaxValue_le_minimaxValue (bddBelow_range_worstCaseRisk htable_nonneg) ?_ intro d rcases exists_measurable_clippedAmbientExactSideProcedure hlu (conditionalAverageProcedure l u m d) (continuous_conditionalAverageProcedure l u m d) with ⟨g, hg, hgeq⟩ refine ⟨⟨g, hg⟩, ?_⟩ apply worstCaseRisk_le intro theta calc measurableExactTableRisk p q tau ⟨g, hg⟩ theta = exactSideRisk p q hq tau (conditionalAverageProcedure l u m d) theta := by unfold measurableExactTableRisk exactSideRisk congr 1 funext x simpa only [sidePmf] using congrArg (fun a : Icc l u ↦ p theta x * ((a : ℝ) - tau theta) ^ 2) (hgeq x (sidePmf q hq theta)) _ ≤ empiricalSideRisk p q hq tau m d theta := exactSideRisk_conditionalAverage_le p q tau hp hq hlu m d theta _ ≤ worstCaseRisk (empiricalSideRisk p q hq tau m) d := by apply le_worstCaseRisk refine ⟨(u - l) ^ 2, ?_⟩ rintro _ ⟨theta', rfl⟩ exact empiricalSideRisk_le p q hp hq tau hlu htau m d theta' -
measurableExactTableMinimax_squeeze_continuousSurjectiontheorem — Given a continuous parameter map, its surjectivity, model coordinates and target, simplex validity, ordered action bounds, and target containment, the measurable exact-table value on the source parameterization is squeezed between the target exact-side value and every target empirical-side value.hypothesesX :sharedType u_5C :sharedType u_6l :sharedℝu :sharedℝA B :phi :A → Bhcont :Continuous phihsurj :Surjective phip :B → X → ℝq :B → C → ℝtau :B → ℝhp :∀ b, p b ∈ stdSimplex ℝ Xhq :∀ b, q b ∈ stdSimplex ℝ Chlu :l ≤ uhtau :∀ b, tau b ∈ Icc l uconclusionconclusion 1exactSideMinimaxValue p q hq tau l u≤ measurableExactTableMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ tau (phi a)) l uconclusion 2m :measurableExactTableMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ tau (phi a)) l u≤ empiricalSideMinimaxValue p q hq tau l u mProof (Lean source)
theorem measurableExactTableMinimax_squeeze_continuousSurjection {A B : Type*} [TopologicalSpace A] [TopologicalSpace B] [CompactSpace A] [CompactSpace B] [Nonempty A] [Nonempty B] (phi : A → B) (hcont : Continuous phi) (hsurj : Surjective phi) (p : B → X → ℝ) (q : B → C → ℝ) (tau : B → ℝ) (hp : ∀ b, p b ∈ stdSimplex ℝ X) (hq : ∀ b, q b ∈ stdSimplex ℝ C) (hlu : l ≤ u) (htau : ∀ b, tau b ∈ Icc l u) : exactSideMinimaxValue p q hq tau l u ≤ measurableExactTableMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ tau (phi a)) l u ∧ ∀ m, measurableExactTableMinimaxValue (fun a ↦ p (phi a)) (fun a ↦ q (phi a)) (fun a ↦ tau (phi a)) l u ≤ empiricalSideMinimaxValue p q hq tau l u m := by have _hcont : Continuous phi := hcont rw [measurableExactTableMinimaxValue_comp_surjective p q tau l u phi hsurj] exact measurableExactTableMinimax_squeeze p q tau hp hq hlu htau -
measurableExactTableMinimaxValue_eq_of_tendstotheorem — Given simplex-valid label and side probabilities, a target, ordered action bounds, target containment, and convergence of the empirical-side minimax values to the exact-side value, the measurable exact-table minimax value equals that common limit.hypothesesTheta :sharedType u_4X :sharedType u_5C :sharedType u_6l :sharedℝu :sharedℝNonempty Thetap :Theta → X → ℝq :Theta → C → ℝtau :Theta → ℝhp :hq :hlu :l ≤ uhconv :Tendsto (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop (nhds (exactSideMinimaxValue p q hq tau l u))conclusionmeasurableExactTableMinimaxValue p q tau l u = exactSideMinimaxValue p q hq tau l uProof (Lean source)
theorem measurableExactTableMinimaxValue_eq_of_tendsto [Nonempty Theta] (p : Theta → X → ℝ) (q : Theta → C → ℝ) (tau : Theta → ℝ) (hp : ∀ theta, p theta ∈ stdSimplex ℝ X) (hq : ∀ theta, q theta ∈ stdSimplex ℝ C) (hlu : l ≤ u) (htau : ∀ theta, tau theta ∈ Icc l u) (hconv : Tendsto (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop (nhds (exactSideMinimaxValue p q hq tau l u))) : measurableExactTableMinimaxValue p q tau l u = exactSideMinimaxValue p q hq tau l u := by apply le_antisymm · apply ge_of_tendsto hconv exact Filter.Eventually.of_forall fun m ↦ measurableExactTableMinimaxValue_le_empiricalSideMinimaxValue p q tau hp hq hlu htau m · exact exactSideMinimaxValue_le_measurableExactTableMinimaxValue p q tau hp hq hlu htau
Selector 1 core · 0 supporting This module provides the measurable first-hit selector used to turn a finite cover of side-law space into a decision rule. ★ exists_measurable_finiteCoverSelector
Measurable finite-cover selectors
This module provides the measurable first-hit selector used to turn a finite cover of side-law space into a decision rule.
theorem exists_measurable_finiteCoverSelector reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
Given a number of centers with positive count, centers, radii that are positive, there is a measurable selector choosing a center within its radius at every point covered by the corresponding open balls.
Formal statement
hypotheses
conclusion
∃ select : E → Fin k,
Measurable select
Proof (Lean source)
theorem exists_measurable_finiteCoverSelector
{E : Type*} [PseudoMetricSpace E] [MeasurableSpace E] [BorelSpace E]
(k : ℕ) (hk : 0 < k) (center : Fin k → E) (radius : Fin k → ℝ)
(hr : ∀ i, 0 < radius i) :
∃ select : E → Fin k, Measurable select ∧
∀ y, (∃ i, dist y (center i) < radius i) →
dist y (center (select y)) < radius (select y) := by
classical
induction k with
| zero => omega
| succ n ih =>
by_cases hn : n = 0
· subst n
refine ⟨fun _ => 0, measurable_const, ?_⟩
intro y hy
obtain ⟨i, hi⟩ := hy
simpa [Fin.eq_zero i] using hi
· have hnpos : 0 < n := Nat.pos_of_ne_zero hn
obtain ⟨select, hselect_meas, hselect⟩ :=
ih hnpos (fun i => center i.succ) (fun i => radius i.succ)
(fun i => hr i.succ)
let firstBall : Set E := ball (center 0) (radius 0)
let result : E → Fin (n + 1) :=
fun y => if y ∈ firstBall then 0 else (select y).succ
refine ⟨result, ?_, ?_⟩
· exact (measurable_const.ite Metric.isOpen_ball.measurableSet
((measurable_of_finite fun i : Fin n => i.succ).comp hselect_meas))
· intro y hy
by_cases hfirst : y ∈ firstBall
· have hfirst' : dist y (center 0) < radius 0 := by
simpa [firstBall, Metric.mem_ball] using hfirst
simp [result, firstBall, hfirst']
· have hfirst' : ¬ dist y (center 0) < radius 0 := by
simpa [firstBall, Metric.mem_ball] using hfirst
have htail : ∃ i : Fin n,
dist y (center i.succ) < radius i.succ := by
obtain ⟨i, hi⟩ := hy
have hi0 : i ≠ 0 := by
intro hieq
subst i
exact hfirst' hi
refine ⟨i.pred hi0, ?_⟩
simpa [Fin.succ_pred i hi0] using hi
have hs := hselect y htail
simpa [result, firstBall, hfirst'] using hs
SimplexSpecialization 1 core · 2 supporting This module specializes the convergence theorem to model classes represented as closed subsets of a finite probability simplex, the form used by finite discrete-law applications. ★ closedSimplex_finiteSideInfo_minimax_tendsto
Closed finite-simplex parameter spaces
This module specializes the convergence theorem to model classes represented as closed subsets of a finite probability simplex, the form used by finite discrete-law applications.
theorem closedSimplex_finiteSideInfo_minimax_tendsto reviewed
⚑ flagged
Causalean.Stat.Minimax.FiniteSideInformation
For a nonempty closed model class inside a finite simplex, finite labeled and finite nonempty side alphabets, continuous simplex-valid label and side coordinates, and a continuous bounded target, the empirical-side minimax values converge to the exact-side benchmark.
Formal statement
hypotheses
I :
Type u_1
X :
Type u_2
C :
Type u_3
l :
ℝ
u :
ℝ
hK :
IsClosed K
hKne :
K.Nonempty
p :
K → X → ℝ
q :
K → C → ℝ
tau :
K → ℝ
hp :
hq :
hpcont :
hqcont :
htau :
Continuous tau
hlu :
l ≤ u
conclusion
Tendsto (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop (nhds (exactSideMinimaxValue p q hq tau l u))
Proof (Lean source)
theorem closedSimplex_finiteSideInfo_minimax_tendsto
(K : Set (FinitePmf I)) (hK : IsClosed K) (hKne : K.Nonempty)
(p : K → X → ℝ) (q : K → C → ℝ) (tau : K → ℝ)
(hp : ∀ theta, p theta ∈ stdSimplex ℝ X)
(hq : ∀ theta, q theta ∈ stdSimplex ℝ C)
(hpcont : ∀ x, Continuous (fun theta ↦ p theta x))
(hqcont : ∀ c, Continuous (fun theta ↦ q theta c)) (htau : Continuous tau)
(hlu : l ≤ u) (htau_mem : ∀ theta, tau theta ∈ Icc l u) :
Tendsto (fun m : ℕ ↦ empiricalSideMinimaxValue p q hq tau l u m) atTop
(nhds (exactSideMinimaxValue p q hq tau l u)) := by
-- Proof plan: install compactness and nonemptiness instances on K, then apply the main theorem.
letI : CompactSpace K := isCompact_iff_compactSpace.mp hK.isCompact
letI : Nonempty K := hKne.to_subtype
exact finiteSideInfo_minimax_tendsto p q tau hp hq hpcont hqcont htau hlu htau_mem
2 supporting declarations (lemmas, instances)
-
isCompact_closed_finitePmftheorem — A closed subset of a finite probability simplex is compact. -
continuous_closed_finitePmf_coordinatetheorem — Restricting an atom coordinate to a closed finite-simplex model class gives a continuous parameter coordinate.hypothesesconclusionContinuous (fun w : K ↦ w.1.1 i)Proof (Lean source)
theorem continuous_closed_finitePmf_coordinate (K : Set (FinitePmf I)) (i : I) : Continuous (fun w : K ↦ w.1.1 i) := by -- Proof plan: compose subtype-value maps with the continuous atom evaluation map. exact (continuous_atom I i).comp continuous_subtype_val