Stat.FiniteRaoBlackwell
Guarded finite conditional laws and Rao–Blackwell reductions for arbitrary finite-design pushforwards and uniform allocation experiments, with exact disintegration, finite-prior posteriors, factorization sufficiency, and real-valued minimax bridges.
Core 11 core · 11 supporting This module gives the finite-sum probability substrate for an experiment that first chooses uniformly from a nonempty finite set of admissible allocations and then draws a finite observation. ★ disintegrate_sum
Finite uniform experiments and guarded conditional designs
This module gives the finite-sum probability substrate for an experiment that first chooses uniformly from a nonempty finite set of admissible allocations and then draws a finite observation. It defines the joint mass, the mass of a coarsening statistic, and a conditional design on every statistic fiber. Positive fibers use Bayes' formula; zero-mass fibers use a fixed point mass, so the result is a genuine probability design everywhere without changing any disintegration identity.
structure FiniteUniformExperiment reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell
A finite uniform-allocation experiment consists of a nonempty admissible allocation set, a normalized nonnegative observation mass for every state and allocation, a finite statistic, and a fallback observation used only to totalize conditioning on null fibers.
Definition (Lean source)
parameters
fields
The finite set of admissible fixed-size allocations.
allocations :
Finset Allocation
At least one admissible allocation is available.
allocations_nonempty :
allocations.Nonempty
Conditional observation mass at a latent state and allocation.
observationMass :
Latent → Allocation → Observation → ℝ
Every conditional observation mass is nonnegative.
observationMass_nonneg :
∀ θ a x, 0 ≤ observationMass θ a x
Conditional observation masses sum to one.
observationMass_sum :
∀ θ a, ∑ x, observationMass θ a x = 1
The coarsened statistic computed from allocation and observation.
statistic :
Allocation → Observation → Statistic
A fallback observation used to define null-fiber conditional laws.
fallbackObservation :
Observation
def fallbackAllocation reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, the fallback allocation is a chosen member of its nonempty set of admissible allocations.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
def
fallbackAllocation E :
Allocation
given by
E.allocations_nonempty.choose
def fallbackSample reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, the fallback full-data point pairs its fallback allocation with its fallback observation.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
def
fallbackSample E :
Allocation × Observation
given by
(E.fallbackAllocation, E.fallbackObservation)
def sampleStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment and a full-data point, the sample statistic is the statistic computed from that point's allocation and observation.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
z :
Allocation × Observation
def
sampleStatistic E z :
Statistic
given by
E.statistic z.1 z.2
def uniformAllocationMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment and an allocation, the uniform allocation mass is the reciprocal of the number of admissible allocations when that allocation is admissible, and zero otherwise.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
a :
Allocation
def
uniformAllocationMass E a :
ℝ
given by
by classical exact if a ∈ E.allocations then (E.allocations.card : ℝ)⁻¹ else 0
def jointMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a latent state, and a full-data point, the joint mass is the uniform allocation mass of its allocation multiplied by the conditional observation mass of its observation at that state and allocation.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
z :
Allocation × Observation
def
jointMass E θ z :
ℝ
given by
E.uniformAllocationMass z.1 * E.observationMass θ z.1 z.2
def statisticMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a latent state, and a statistic value, the statistic mass is the sum of joint masses of all full-data points whose statistic equals that value.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
s :
Statistic
def
statisticMass E θ s :
ℝ
given by
by classical exact ∑ z : Allocation × Observation, if E.sampleStatistic z
= s then E.jointMass θ z else 0
def conditionalWeight reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a latent state, a statistic value, and a full-data point, the guarded conditional weight is the joint mass divided by the statistic mass when that mass is positive and the point has the requested statistic, is zero for other points, and is instead a point mass at the fallback sample when the statistic mass is zero.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
s :
Statistic
z :
Allocation × Observation
def
conditionalWeight E θ s z :
ℝ
given by
by classical exact if 0 < E.statisticMass θ s then if E.sampleStatistic z
= s then E.jointMass θ z / E.statisticMass θ s else 0 else if z = E.fallbackSample then 1 else 0
def conditionalDesign reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a latent state, and a statistic value, the guarded conditional full-data design is the finite probability design whose probabilities are the guarded conditional weights.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
s :
Statistic
def
given by
clause 1
p := E.conditionalWeight θ s
clause 2
p_nonneg := E.conditionalWeight_nonneg θ s
clause 3
p_sum := E.conditionalWeight_sum θ s
def statisticDesign reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment and a latent state, the statistic design is the finite probability design whose probabilities are the statistic masses.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
def
given by
clause 1
p := E.statisticMass θ
clause 2
p_nonneg := E.statisticMass_nonneg θ
clause 3
p_sum := E.statisticMass_sum θ
theorem disintegrate_sum reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Every real test function has the same joint expectation as its statistic-marginal expectation of the guarded conditional expectation; null fibers contribute exactly zero.
Formal statement
hypotheses
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
f :
Allocation × Observation → ℝ
conclusion
∑ z, E.jointMass θ z * f z
= ∑ s, E.statisticMass θ s * (∑ z, E.conditionalWeight θ s z * f z)
Proof (Lean source)
theorem disintegrate_sum (θ : Latent) (f : Allocation × Observation → ℝ) :
∑ z, E.jointMass θ z * f z =
∑ s, E.statisticMass θ s *
(∑ z, E.conditionalWeight θ s z * f z) := by
/- Distribute products over the inner sums, use statisticMass_mul_conditionalWeight,
swap the finite sums, and collapse the unique statistic value of each sample point. -/
classical
simp_rw [Finset.mul_sum, ← mul_assoc,
E.statisticMass_mul_conditionalWeight θ]
rw [Finset.sum_comm]
simp
11 supporting declarations (lemmas, instances)
-
uniformAllocationMass_nonnegtheorem — The uniform allocation mass is nonnegative at every allocation.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4a :Allocationconclusion0 ≤ E.uniformAllocationMass aProof (Lean source)
theorem uniformAllocationMass_nonneg (a : Allocation) : 0 ≤ E.uniformAllocationMass a := by classical simp only [uniformAllocationMass] split_ifs · exact inv_nonneg.mpr (Nat.cast_nonneg _) · exact le_rfl -
jointMass_nonnegtheorem — The full-data joint mass is nonnegative at every state and sample point.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latentz :Allocation × Observationconclusion0 ≤ E.jointMass θ zProof (Lean source)
theorem jointMass_nonneg (θ : Latent) (z : Allocation × Observation) : 0 ≤ E.jointMass θ z := by exact mul_nonneg (E.uniformAllocationMass_nonneg z.1) (E.observationMass_nonneg θ z.1 z.2) -
jointMass_sumtheorem — At every latent state, the full-data joint mass sums to one.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latentconclusion∑ z : Allocation × Observation, E.jointMass θ z = 1Proof (Lean source)
theorem jointMass_sum (θ : Latent) : ∑ z : Allocation × Observation, E.jointMass θ z = 1 := by /- Expand the product sum, discard allocations off the support, use observationMass_sum, and cancel the nonzero finite support cardinality. -/ classical rw [Fintype.sum_prod_type] simp_rw [jointMass, ← Finset.mul_sum, E.observationMass_sum, mul_one] simp [uniformAllocationMass, E.allocations_nonempty.card_ne_zero] -
statisticMass_nonnegtheorem — Every statistic mass is nonnegative.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statisticconclusion0 ≤ E.statisticMass θ sProof (Lean source)
theorem statisticMass_nonneg (θ : Latent) (s : Statistic) : 0 ≤ E.statisticMass θ s := by classical exact sum_nonneg fun z _ => by split_ifs · exact E.jointMass_nonneg θ z · exact le_rfl -
statisticMass_sumtheorem — At every latent state, the statistic masses sum to one.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latentconclusion∑ s : Statistic, E.statisticMass θ s = 1Proof (Lean source)
theorem statisticMass_sum (θ : Latent) : ∑ s : Statistic, E.statisticMass θ s = 1 := by /- Swap the two finite sums; for each full-data point exactly one statistic value survives. -/ classical rw [← E.jointMass_sum θ] simp_rw [statisticMass] rw [Finset.sum_comm] simp -
conditionalWeight_of_postheorem — On a positive fiber, the guarded conditional weight is the usual fiber-restricted Bayes ratio.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statistich :0 < E.statisticMass θ sz :Allocation × ObservationconclusionE.conditionalWeight θ s z= if E.sampleStatistic z = s then E.jointMass θ z / E.statisticMass θ s else 0Proof (Lean source)
theorem conditionalWeight_of_pos {θ : Latent} {s : Statistic} (h : 0 < E.statisticMass θ s) (z : Allocation × Observation) : E.conditionalWeight θ s z = if E.sampleStatistic z = s then E.jointMass θ z / E.statisticMass θ s else 0 := by classical simp [conditionalWeight, h] -
conditionalWeight_of_eq_zerotheorem — On a zero-mass fiber, the guarded conditional weight is the fallback point mass.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statistich :E.statisticMass θ s = 0z :Allocation × ObservationconclusionE.conditionalWeight θ s z = if z = E.fallbackSample then 1 else 0Proof (Lean source)
theorem conditionalWeight_of_eq_zero {θ : Latent} {s : Statistic} (h : E.statisticMass θ s = 0) (z : Allocation × Observation) : E.conditionalWeight θ s z = if z = E.fallbackSample then 1 else 0 := by classical simp [conditionalWeight, h] -
conditionalWeight_nonnegtheorem — Every guarded conditional weight is nonnegative, including on null fibers.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statisticz :Allocation × Observationconclusion0 ≤ E.conditionalWeight θ s zProof (Lean source)
theorem conditionalWeight_nonneg (θ : Latent) (s : Statistic) (z : Allocation × Observation) : 0 ≤ E.conditionalWeight θ s z := by classical by_cases h : 0 < E.statisticMass θ s · simp only [E.conditionalWeight_of_pos h] split_ifs · exact div_nonneg (E.jointMass_nonneg θ z) (le_of_lt h) · exact le_rfl · have hs : E.statisticMass θ s = 0 := le_antisymm (le_of_not_gt h) (E.statisticMass_nonneg θ s) rw [E.conditionalWeight_of_eq_zero hs] split_ifs <;> norm_num -
conditionalWeight_sumtheorem — The guarded conditional weights sum to one on every fiber, with positive fibers normalized by Bayes' formula and null fibers normalized by the fallback point mass.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statisticconclusion∑ z : Allocation × Observation, E.conditionalWeight θ s z = 1Proof (Lean source)
theorem conditionalWeight_sum (θ : Latent) (s : Statistic) : ∑ z : Allocation × Observation, E.conditionalWeight θ s z = 1 := by /- Split on positivity of statisticMass. In the positive branch divide the defining fiber sum by its mass; in the null branch sum the fallback Kronecker mass. -/ classical by_cases h : 0 < E.statisticMass θ s · simp_rw [E.conditionalWeight_of_pos h] simp_rw [div_eq_mul_inv] have hfactor (z : Allocation × Observation) : (if E.sampleStatistic z = s then E.jointMass θ z * (E.statisticMass θ s)⁻¹ else 0) = (if E.sampleStatistic z = s then E.jointMass θ z else 0) * (E.statisticMass θ s)⁻¹ := by split_ifs <;> simp simp_rw [hfactor] rw [← Finset.sum_mul, show (∑ z : Allocation × Observation, if E.sampleStatistic z = s then E.jointMass θ z else 0) = E.statisticMass θ s from rfl] exact mul_inv_cancel₀ (ne_of_gt h) · have hs : E.statisticMass θ s = 0 := le_antisymm (le_of_not_gt h) (E.statisticMass_nonneg θ s) simp [E.conditionalWeight_of_eq_zero hs] -
statisticMass_mul_conditionalWeighttheorem — Multiplying a statistic marginal by its guarded conditional weight recovers the joint mass on that fiber and zero away from it, including when the marginal is zero.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statisticz :Allocation × ObservationconclusionE.statisticMass θ s * E.conditionalWeight θ s z= if E.sampleStatistic z = s then E.jointMass θ z else 0Proof (Lean source)
theorem statisticMass_mul_conditionalWeight (θ : Latent) (s : Statistic) (z : Allocation × Observation) : E.statisticMass θ s * E.conditionalWeight θ s z = if E.sampleStatistic z = s then E.jointMass θ z else 0 := by /- Positive mass is field cancellation. If the mass is zero, nonnegativity and the fact that jointMass is one summand in statisticMass force every mass on the fiber to vanish. -/ classical by_cases h : 0 < E.statisticMass θ s · rw [E.conditionalWeight_of_pos h] split_ifs · exact mul_div_cancel₀ _ (ne_of_gt h) · exact mul_zero _ · have hs : E.statisticMass θ s = 0 := le_antisymm (le_of_not_gt h) (E.statisticMass_nonneg θ s) rw [hs, zero_mul] split_ifs with hz · have hsum : (∑ z' : Allocation × Observation, if E.sampleStatistic z' = s then E.jointMass θ z' else 0) = 0 := by simpa [statisticMass] using hs have hterm := (Finset.sum_eq_zero_iff_of_nonneg (fun z' _ => by split_ifs · exact E.jointMass_nonneg θ z' · exact le_rfl)).mp hsum z (Finset.mem_univ z) simpa [hz] using hterm.symm · rfl -
jointMass_eq_statisticMass_mul_conditionalWeighttheorem — Every full-data atom factors into its statistic marginal and guarded conditional weight.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latentz :Allocation × ObservationconclusionE.jointMass θ z= E.statisticMass θ (E.sampleStatistic z) * E.conditionalWeight θ (E.sampleStatistic z) zProof (Lean source)
theorem jointMass_eq_statisticMass_mul_conditionalWeight (θ : Latent) (z : Allocation × Observation) : E.jointMass θ z = E.statisticMass θ (E.sampleStatistic z) * E.conditionalWeight θ (E.sampleStatistic z) z := by simpa using (E.statisticMass_mul_conditionalWeight θ (E.sampleStatistic z) z).symm
Sufficiency 6 core · 5 supporting This module gives a finite Fisher--Neyman factorization criterion for the statistic of a FiniteUniformExperiment. ★ commonConditionalWeight_eq_conditionalWeight
Finite factorization sufficiency
This module gives a finite Fisher--Neyman factorization criterion for the statistic of a
FiniteUniformExperiment. A state-dependent factor through the statistic and a nonnegative
state-independent carrier weight determine a common conditional distribution of the full data
given the statistic. Null carrier fibers are totalized by the experiment's fallback point.
structure CommonConditionalKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
A common finite conditional law assigns normalized nonnegative full-data weights to every statistic value and agrees with each statewise Bayes conditional on every positive-mass fiber.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
fields
The state-independent conditional full-data weights.
weight :
Statistic → Allocation × Observation → ℝ
Common conditional weights are nonnegative.
weight_nonneg :
∀ s z, 0 ≤ weight s z
Common conditional weights are normalized at every statistic value.
weight_sum :
∀ s, ∑ z, weight s z = 1
Positive statewise fibers have the common conditional weights.
eq_conditionalWeight :
∀ θ s
if
0 < E.statisticMass θ s
then
∀ z, weight s z = E.conditionalWeight θ s z
structure SufficientFactorization reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
A sufficient factorization writes every full-data mass as a nonnegative factor depending on the state and data only through the statistic, times a nonnegative state-independent carrier weight on the full data.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
fields
The state-independent carrier weight on full-data points.
carrierWeight :
Allocation × Observation → ℝ
Carrier weights are nonnegative.
carrierWeight_nonneg :
∀ z, 0 ≤ carrierWeight z
The state-and-statistic likelihood factor.
statisticFactor :
Latent → Statistic → ℝ
State-and-statistic factors are nonnegative.
statisticFactor_nonneg :
∀ θ s, 0 ≤ statisticFactor θ s
The full-data mass factors through the statistic.
jointMass_factor :
∀ θ z, E.jointMass θ z = statisticFactor θ (E.sampleStatistic z) * carrierWeight z
def fiberCarrierMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment.SufficientFactorization
For a finite uniform experiment, a sufficient factorization of that experiment's full-data masses, and a statistic value, the carrier mass of that statistic fiber is the sum of the factorization's state-independent carrier weights over all allocation--observation pairs having that statistic value.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
F :
E.SufficientFactorization
s :
Statistic
def
fiberCarrierMass F s :
ℝ
given by
∑ z : Allocation × Observation, if E.sampleStatistic z = s then F.carrierWeight z else 0
def commonConditionalWeight reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment.SufficientFactorization
For a finite uniform experiment, a sufficient factorization of its full-data masses, a statistic value, and an allocation--observation pair, the common conditional weight equals the carrier weight divided by the carrier mass when that mass is positive and the pair has the stated statistic, equals zero when the mass is positive but the pair has another statistic, and otherwise is a unit mass at the experiment's designated fallback pair.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
F :
E.SufficientFactorization
s :
Statistic
z :
Allocation × Observation
def
commonConditionalWeight F s z :
ℝ
given by
if 0 < F.fiberCarrierMass s then if E.sampleStatistic z
= s then F.carrierWeight z / F.fiberCarrierMass s else 0 else if z = E.fallbackSample then 1 else 0
theorem commonConditionalWeight_eq_conditionalWeight reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment.SufficientFactorization
On every positive statewise statistic fiber, factorization identifies the common conditional weight with the guarded Bayes conditional weight.
Formal statement
hypotheses
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
F :
E.SufficientFactorization
θ :
Latent
s :
Statistic
h :
0 < E.statisticMass θ s
z :
Allocation × Observation
conclusion
F.commonConditionalWeight s z = E.conditionalWeight θ s z
Proof (Lean source)
theorem commonConditionalWeight_eq_conditionalWeight
(θ : Latent) (s : Statistic) (h : 0 < E.statisticMass θ s)
(z : Allocation × Observation) :
F.commonConditionalWeight s z = E.conditionalWeight θ s z := by
/- Positive statistic mass makes both factor terms positive. Expand both guarded weights,
rewrite statisticMass and jointMass by factorization, then cancel the statistic factor. -/
classical
have hcarrier : 0 < F.fiberCarrierMass s :=
F.fiberCarrierMass_pos_of_statisticMass_pos h
have hprod : 0 < F.statisticFactor θ s * F.fiberCarrierMass s := by
rwa [← F.statisticMass_eq_factor_mul_fiberCarrierMass θ s]
have hfactor : 0 < F.statisticFactor θ s :=
pos_of_mul_pos_left hprod (F.fiberCarrierMass_nonneg s)
rw [E.conditionalWeight_of_pos h]
simp only [commonConditionalWeight, hcarrier, if_pos]
by_cases hz : E.sampleStatistic z = s
· simp only [hz, if_pos]
rw [F.jointMass_factor, F.statisticMass_eq_factor_mul_fiberCarrierMass, hz]
exact (mul_div_mul_left (F.carrierWeight z) (F.fiberCarrierMass s)
(ne_of_gt hfactor)).symm
· simp [hz]
def toCommonConditionalKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment.SufficientFactorization
For a finite uniform experiment and a sufficient factorization of its full-data masses, the common conditional kernel induced by that factorization assigns the factorization-induced common conditional weights to every statistic value and allocation--observation pair.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
F :
E.SufficientFactorization
def
toCommonConditionalKernel F :
E.CommonConditionalKernel
given by
clause 1
weight := F.commonConditionalWeight
clause 2
weight_nonneg := F.commonConditionalWeight_nonneg
clause 3
weight_sum := F.commonConditionalWeight_sum
clause 4
eq_conditionalWeight := F.commonConditionalWeight_eq_conditionalWeight
5 supporting declarations (lemmas, instances)
-
fiberCarrierMass_nonnegtheorem — Every carrier fiber mass is nonnegative.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3F :sharedE.SufficientFactorizations :Statisticconclusion0 ≤ F.fiberCarrierMass sProof (Lean source)
theorem fiberCarrierMass_nonneg (s : Statistic) : 0 ≤ F.fiberCarrierMass s := by /- Expand the fiber sum and use carrierWeight_nonneg in the matching branch. -/ classical exact sum_nonneg fun z _ => by split_ifs · exact F.carrierWeight_nonneg z · exact le_rfl -
statisticMass_eq_factor_mul_fiberCarrierMasstheorem — The statistic mass factors as the state-and-statistic factor times the carrier fiber mass.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3F :sharedE.SufficientFactorizationθ :Latents :StatisticconclusionE.statisticMass θ s = F.statisticFactor θ s * F.fiberCarrierMass sProof (Lean source)
theorem statisticMass_eq_factor_mul_fiberCarrierMass (θ : Latent) (s : Statistic) : E.statisticMass θ s = F.statisticFactor θ s * F.fiberCarrierMass s := by /- Rewrite every joint atom by jointMass_factor; on the selected fiber the statistic factor is constant, so Finset.mul_sum factors it out. -/ classical simp only [FiniteUniformExperiment.statisticMass, fiberCarrierMass, Finset.mul_sum] apply Finset.sum_congr rfl intro z _ by_cases hz : E.sampleStatistic z = s · simp [hz, F.jointMass_factor] · simp [hz] -
fiberCarrierMass_pos_of_statisticMass_postheorem — Positive statistic mass forces the state-independent carrier fiber to have positive mass.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3F :sharedE.SufficientFactorizationθ :Latents :Statistich :0 < E.statisticMass θ sconclusion0 < F.fiberCarrierMass sProof (Lean source)
theorem fiberCarrierMass_pos_of_statisticMass_pos {θ : Latent} {s : Statistic} (h : 0 < E.statisticMass θ s) : 0 < F.fiberCarrierMass s := by /- Rewrite statisticMass using the product formula. Both factors are nonnegative, so a positive product forces the carrier factor to be positive. -/ have hprod : 0 < F.statisticFactor θ s * F.fiberCarrierMass s := by rwa [← F.statisticMass_eq_factor_mul_fiberCarrierMass θ s] exact pos_of_mul_pos_right hprod (F.statisticFactor_nonneg θ s) -
commonConditionalWeight_nonnegtheorem — Factorization-induced common conditional weights are nonnegative on every fiber.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3F :sharedE.SufficientFactorizations :Statisticz :Allocation × Observationconclusion0 ≤ F.commonConditionalWeight s zProof (Lean source)
theorem commonConditionalWeight_nonneg (s : Statistic) (z : Allocation × Observation) : 0 ≤ F.commonConditionalWeight s z := by /- Split on positive carrier fiber mass and on fiber membership; use div_nonneg in the positive branch and the fallback Kronecker mass in the null branch. -/ classical by_cases hs : 0 < F.fiberCarrierMass s · simp only [commonConditionalWeight, hs, if_pos] split_ifs · exact div_nonneg (F.carrierWeight_nonneg z) (le_of_lt hs) · exact le_rfl · simp only [commonConditionalWeight, hs, if_false] split_ifs <;> norm_num -
commonConditionalWeight_sumtheorem — Factorization-induced common conditional weights sum to one on every fiber.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3F :sharedE.SufficientFactorizations :Statisticconclusion∑ z, F.commonConditionalWeight s z = 1Proof (Lean source)
theorem commonConditionalWeight_sum (s : Statistic) : ∑ z, F.commonConditionalWeight s z = 1 := by /- On a positive carrier fiber, the numerator sum is fiberCarrierMass and division cancels. On a null fiber, sum the fallback point mass. -/ classical by_cases hs : 0 < F.fiberCarrierMass s · simp only [commonConditionalWeight, hs, if_pos] simp_rw [div_eq_mul_inv] have hfactor (z : Allocation × Observation) : (if E.sampleStatistic z = s then F.carrierWeight z * (F.fiberCarrierMass s)⁻¹ else 0) = (if E.sampleStatistic z = s then F.carrierWeight z else 0) * (F.fiberCarrierMass s)⁻¹ := by split_ifs <;> simp simp_rw [hfactor] rw [← Finset.sum_mul, show (∑ z : Allocation × Observation, if E.sampleStatistic z = s then F.carrierWeight z else 0) = F.fiberCarrierMass s from rfl] exact mul_inv_cancel₀ (ne_of_gt hs) · simp [commonConditionalWeight, hs]
Posterior 6 core · 9 supporting This module mixes a finite latent-state prior with the statistic law of a FiniteUniformExperiment. ★ posterior_disintegrate_sum
Finite prior joint laws and guarded posterior kernels
This module mixes a finite latent-state prior with the statistic law of a
FiniteUniformExperiment. It defines the resulting state--statistic joint mass, statistic
marginal, and guarded posterior law of the latent state given the statistic. On a null
statistic fiber the posterior is totalized by the original prior, which preserves normalization
and does not affect disintegration.
def priorJointStatisticMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a finite prior design on latent states, a latent state, and a statistic value, the prior joint state--statistic mass is the prior probability of the state multiplied by that state's statistic mass at the specified value.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
θ :
Latent
s :
Statistic
def
priorJointStatisticMass E prior θ s :
ℝ
given by
prior.p θ * E.statisticMass θ s
def priorStatisticMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a finite prior design on latent states, and a statistic value, the prior-predictive statistic mass is the sum of the prior joint state--statistic masses over all latent states.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
s :
Statistic
def
priorStatisticMass E prior s :
ℝ
given by
∑ θ, E.priorJointStatisticMass prior θ s
def posteriorWeight reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a finite prior design on latent states, a statistic value, and a latent state, the guarded posterior weight is the prior joint state--statistic mass divided by the prior-predictive statistic mass when the latter is positive, and is the original prior probability of the state when it is zero.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
s :
Statistic
θ :
Latent
def
posteriorWeight E prior s θ :
ℝ
given by
if 0 < E.priorStatisticMass prior s then E.priorJointStatisticMass prior θ s / E.priorStatisticMass prior s else prior.p θ
def posteriorDesign reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a finite prior design on latent states, and a statistic value, the guarded posterior design is the finite probability design on latent states whose probabilities are the guarded posterior weights.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
s :
Statistic
def
given by
clause 1
p := E.posteriorWeight prior s
clause 2
p_nonneg := E.posteriorWeight_nonneg prior s
clause 3
p_sum := E.posteriorWeight_sum prior s
def priorStatisticDesign reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment and a finite prior design on latent states, the prior-predictive statistic design is the finite probability design whose probabilities are the prior-predictive statistic masses.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
def
given by
clause 1
p := E.priorStatisticMass prior
clause 2
p_nonneg := E.priorStatisticMass_nonneg prior
clause 3
p_sum := E.priorStatisticMass_sum prior
theorem posterior_disintegrate_sum reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Every real test function of latent state and statistic has the same prior-joint expectation as prior-predictive statistic expectation of posterior conditional expectation; null fibers contribute exactly zero.
Formal statement
hypotheses
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
f :
Latent → Statistic → ℝ
conclusion
∑ θ, ∑ s, E.priorJointStatisticMass prior θ s * f θ s
= ∑ s, E.priorStatisticMass prior s * (∑ θ, E.posteriorWeight prior s θ * f θ s)
Proof (Lean source)
theorem posterior_disintegrate_sum (prior : FiniteDesign Latent)
(f : Latent → Statistic → ℝ) :
∑ θ, ∑ s, E.priorJointStatisticMass prior θ s * f θ s =
∑ s, E.priorStatisticMass prior s *
(∑ θ, E.posteriorWeight prior s θ * f θ s) := by
/- Distribute the outer marginal through each inner sum, apply the atomwise posterior
factorization, and swap the two finite sums. -/
classical
simp_rw [Finset.mul_sum, ← mul_assoc,
E.priorStatisticMass_mul_posteriorWeight prior]
rw [Finset.sum_comm]
9 supporting declarations (lemmas, instances)
-
priorJointStatisticMass_nonnegtheorem — Every prior state--statistic joint mass is nonnegative.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latentθ :Latents :Statisticconclusion0 ≤ E.priorJointStatisticMass prior θ sProof (Lean source)
theorem priorJointStatisticMass_nonneg (prior : FiniteDesign Latent) (θ : Latent) (s : Statistic) : 0 ≤ E.priorJointStatisticMass prior θ s := by /- Multiply prior and statewise-statistic nonnegativity. -/ exact mul_nonneg (prior.p_nonneg θ) (E.statisticMass_nonneg θ s) -
priorJointStatisticMass_sumtheorem — The prior state--statistic joint masses sum to one.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latentconclusion∑ p : Latent × Statistic, E.priorJointStatisticMass prior p.1 p.2 = 1Proof (Lean source)
theorem priorJointStatisticMass_sum (prior : FiniteDesign Latent) : ∑ p : Latent × Statistic, E.priorJointStatisticMass prior p.1 p.2 = 1 := by /- Expand the product sum, use statisticMass_sum at each state, then prior.p_sum. -/ classical rw [Fintype.sum_prod_type] simp_rw [priorJointStatisticMass, ← Finset.mul_sum, E.statisticMass_sum, mul_one] exact prior.p_sum -
priorStatisticMass_nonnegtheorem — Every prior-predictive statistic mass is nonnegative.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statisticconclusion0 ≤ E.priorStatisticMass prior sProof (Lean source)
theorem priorStatisticMass_nonneg (prior : FiniteDesign Latent) (s : Statistic) : 0 ≤ E.priorStatisticMass prior s := by /- Sum the nonnegative prior joint atoms over latent states. -/ classical exact sum_nonneg fun θ _ => E.priorJointStatisticMass_nonneg prior θ s -
priorStatisticMass_sumtheorem — The prior-predictive statistic masses sum to one.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latentconclusion∑ s, E.priorStatisticMass prior s = 1Proof (Lean source)
theorem priorStatisticMass_sum (prior : FiniteDesign Latent) : ∑ s, E.priorStatisticMass prior s = 1 := by /- Swap the statistic/state sums and reuse the joint normalization calculation. -/ classical simp_rw [priorStatisticMass] rw [Finset.sum_comm] simpa only [Fintype.sum_prod_type] using E.priorJointStatisticMass_sum prior -
posteriorWeight_of_postheorem — On a positive prior-predictive fiber, the guarded posterior is the usual Bayes ratio.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statistich :0 < E.priorStatisticMass prior sθ :LatentconclusionE.posteriorWeight prior s θ= E.priorJointStatisticMass prior θ s / E.priorStatisticMass prior sProof (Lean source)
theorem posteriorWeight_of_pos (prior : FiniteDesign Latent) {s : Statistic} (h : 0 < E.priorStatisticMass prior s) (θ : Latent) : E.posteriorWeight prior s θ = E.priorJointStatisticMass prior θ s / E.priorStatisticMass prior s := by /- Unfold posteriorWeight and simplify the positive guard. -/ simp [posteriorWeight, h] -
posteriorWeight_of_eq_zerotheorem — On a null prior-predictive fiber, the guarded posterior is the original prior.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statistich :E.priorStatisticMass prior s = 0θ :LatentconclusionE.posteriorWeight prior s θ = prior.p θProof (Lean source)
theorem posteriorWeight_of_eq_zero (prior : FiniteDesign Latent) {s : Statistic} (h : E.priorStatisticMass prior s = 0) (θ : Latent) : E.posteriorWeight prior s θ = prior.p θ := by /- Unfold posteriorWeight; nonnegativity plus zero mass rules out the positive guard. -/ simp [posteriorWeight, h] -
posteriorWeight_nonnegtheorem — Every guarded posterior weight is nonnegative.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statisticθ :Latentconclusion0 ≤ E.posteriorWeight prior s θProof (Lean source)
theorem posteriorWeight_nonneg (prior : FiniteDesign Latent) (s : Statistic) (θ : Latent) : 0 ≤ E.posteriorWeight prior s θ := by /- Split on positive priorStatisticMass; use div_nonneg or prior.p_nonneg. -/ classical by_cases h : 0 < E.priorStatisticMass prior s · rw [E.posteriorWeight_of_pos prior h] exact div_nonneg (E.priorJointStatisticMass_nonneg prior θ s) (le_of_lt h) · have hs : E.priorStatisticMass prior s = 0 := le_antisymm (le_of_not_gt h) (E.priorStatisticMass_nonneg prior s) rw [E.posteriorWeight_of_eq_zero prior hs] exact prior.p_nonneg θ -
posteriorWeight_sumtheorem — Guarded posterior weights sum to one on positive and null prior-predictive fibers.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statisticconclusion∑ θ, E.posteriorWeight prior s θ = 1Proof (Lean source)
theorem posteriorWeight_sum (prior : FiniteDesign Latent) (s : Statistic) : ∑ θ, E.posteriorWeight prior s θ = 1 := by /- Positive fibers divide the defining marginal sum by itself; null fibers use prior.p_sum. -/ classical by_cases h : 0 < E.priorStatisticMass prior s · simp_rw [E.posteriorWeight_of_pos prior h, div_eq_mul_inv] rw [← Finset.sum_mul, show (∑ θ, E.priorJointStatisticMass prior θ s) = E.priorStatisticMass prior s from rfl] exact mul_inv_cancel₀ (ne_of_gt h) · have hs : E.priorStatisticMass prior s = 0 := le_antisymm (le_of_not_gt h) (E.priorStatisticMass_nonneg prior s) simp [E.posteriorWeight_of_eq_zero prior hs, prior.p_sum] -
priorStatisticMass_mul_posteriorWeighttheorem — Multiplying the statistic marginal by its guarded posterior weight recovers each state--statistic joint atom, including on null fibers.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statisticθ :LatentconclusionE.priorStatisticMass prior s * E.posteriorWeight prior s θ= E.priorJointStatisticMass prior θ sProof (Lean source)
theorem priorStatisticMass_mul_posteriorWeight (prior : FiniteDesign Latent) (s : Statistic) (θ : Latent) : E.priorStatisticMass prior s * E.posteriorWeight prior s θ = E.priorJointStatisticMass prior θ s := by /- Positive mass is cancellation. If the marginal is zero, nonnegativity of every joint summand forces the selected joint atom to vanish. -/ classical by_cases h : 0 < E.priorStatisticMass prior s · rw [E.posteriorWeight_of_pos prior h] exact mul_div_cancel₀ _ (ne_of_gt h) · have hs : E.priorStatisticMass prior s = 0 := le_antisymm (le_of_not_gt h) (E.priorStatisticMass_nonneg prior s) rw [hs, zero_mul] have hsum : (∑ θ', E.priorJointStatisticMass prior θ' s) = 0 := by simpa [priorStatisticMass] using hs have hterm := (Finset.sum_eq_zero_iff_of_nonneg (fun θ' _ => E.priorJointStatisticMass_nonneg prior θ' s)).mp hsum θ (Finset.mem_univ θ) exact hterm.symm
RaoBlackwell 6 core · 15 supporting This module averages a real estimator over the guarded conditional design from Core and proves finite Jensen and squared-risk contraction. ★ statisticRisk_raoBlackwellEstimator_le_fullRisk
Finite Rao--Blackwell reduction for squared loss
This module averages a real estimator over the guarded conditional design from Core and proves
finite Jensen and squared-risk contraction. The state-indexed conditional mean is retained as
an analytic fiberwise device. The usable Rao--Blackwell estimator is a single statistic-only
function constructed from a sufficient factorization, and it yields statewise, finite-prior,
worst-case, and minimax-compatible corollaries.
def conditionalMean reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a real-valued full-data estimator, a latent state, and a statistic value, the conditional mean is the estimator's finite expectation under the guarded conditional design given that state and statistic value.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
est :
Allocation × Observation → ℝ
θ :
Latent
s :
Statistic
def
conditionalMean E est θ s :
ℝ
given by
∑ z, E.conditionalWeight θ s z * est z
def fullRisk reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a real-valued target indexed by latent state, a real-valued full-data estimator, and a latent state, the full-data squared-error risk is the joint expected value of the estimator's squared error relative to the target at that state.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
target :
Latent → ℝ
est :
Allocation × Observation → ℝ
θ :
Latent
def
fullRisk E target est θ :
ℝ
given by
∑ z, E.jointMass θ z * (est z - target θ) ^ 2
def statisticRisk reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a real-valued target indexed by latent state, a real-valued statistic-only estimator, and a latent state, the statistic-only squared-error risk is the joint expected squared error after applying the estimator to the sample statistic.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
target :
Latent → ℝ
est :
Statistic → ℝ
θ :
Latent
def
statisticRisk E target est θ :
ℝ
given by
∑ z, E.jointMass θ z * (est (E.sampleStatistic z) - target θ) ^ 2
def commonRaoBlackwellEstimator reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a common conditional kernel, and a real-valued full-data estimator, the common Rao--Blackwell estimator assigns to each statistic value the finite weighted average of the full-data estimator under that kernel.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
K :
E.CommonConditionalKernel
est :
Allocation × Observation → ℝ
def
commonRaoBlackwellEstimator E K est :
Statistic → ℝ
given by
fun s ↦ ∑ z, K.weight s z * est z
def raoBlackwellEstimator reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
For a finite uniform-allocation experiment, a sufficient factorization, and a real-valued full-data estimator, the Rao--Blackwell estimator is the statistic-only estimator obtained by averaging the full-data estimator with the factorization's derived common conditional law.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
F :
E.SufficientFactorization
est :
Allocation × Observation → ℝ
def
raoBlackwellEstimator E F est :
Statistic → ℝ
given by
E.commonRaoBlackwellEstimator F.toCommonConditionalKernel est
theorem statisticRisk_raoBlackwellEstimator_le_fullRisk reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
A sufficient factorization produces one statistic-only Rao--Blackwell estimator whose squared-error risk is no larger than the full-data estimator at every latent state.
Formal statement
hypotheses
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
F :
E.SufficientFactorization
target :
Latent → ℝ
est :
Allocation × Observation → ℝ
θ :
Latent
conclusion
E.statisticRisk target (E.raoBlackwellEstimator F est) θ ≤ E.fullRisk target est θ
Proof (Lean source)
theorem statisticRisk_raoBlackwellEstimator_le_fullRisk
(F : E.SufficientFactorization)
(target : Latent → ℝ) (est : Allocation × Observation → ℝ) (θ : Latent) :
E.statisticRisk target (E.raoBlackwellEstimator F est) θ ≤
E.fullRisk target est θ := by
exact E.statisticRisk_commonRaoBlackwellEstimator_le_fullRisk
F.toCommonConditionalKernel target est θ
15 supporting declarations (lemmas, instances)
-
measurable_conditionalMeantheorem — On a finite statistic space, the state-indexed conditional mean is measurable for the discrete sigma algebra.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4MeasurableSpace StatisticMeasurableSingletonClass Statisticest :Allocation × Observation → ℝθ :LatentconclusionMeasurable (E.conditionalMean est θ)Proof (Lean source)
theorem measurable_conditionalMean [MeasurableSpace Statistic] [MeasurableSingletonClass Statistic] (est : Allocation × Observation → ℝ) (θ : Latent) : Measurable (E.conditionalMean est θ) := by exact measurable_of_finite _ -
fullRisk_nonnegtheorem — Full-data squared-error risk is nonnegative at every latent state.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4target :Latent → ℝest :Allocation × Observation → ℝθ :Latentconclusion0 ≤ E.fullRisk target est θProof (Lean source)
theorem fullRisk_nonneg (target : Latent → ℝ) (est : Allocation × Observation → ℝ) (θ : Latent) : 0 ≤ E.fullRisk target est θ := by exact sum_nonneg fun z _ ↦ mul_nonneg (E.jointMass_nonneg θ z) (sq_nonneg _) -
statisticRisk_nonnegtheorem — Statistic-only squared-error risk is nonnegative at every latent state.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4target :Latent → ℝest :Statistic → ℝθ :Latentconclusion0 ≤ E.statisticRisk target est θProof (Lean source)
theorem statisticRisk_nonneg (target : Latent → ℝ) (est : Statistic → ℝ) (θ : Latent) : 0 ≤ E.statisticRisk target est θ := by exact sum_nonneg fun z _ ↦ mul_nonneg (E.jointMass_nonneg θ z) (sq_nonneg _) -
conditionalMean_sq_letheorem — Conditional Jensen for squared loss: the squared error of the conditional mean is at most the conditional mean squared error on every guarded fiber.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4target :ℝest :Allocation × Observation → ℝθ :Latents :Statisticconclusion(E.conditionalMean est θ s - target) ^ 2≤ ∑ z, E.conditionalWeight θ s z * (est z - target) ^ 2Proof (Lean source)
theorem conditionalMean_sq_le (target : ℝ) (est : Allocation × Observation → ℝ) (θ : Latent) (s : Statistic) : (E.conditionalMean est θ s - target) ^ 2 ≤ ∑ z, E.conditionalWeight θ s z * (est z - target) ^ 2 := by /- Apply ConvexOn.map_sum_le to x ↦ x^2 with the conditional weights. Linearity and conditionalWeight_sum identify the weighted centered mean with conditionalMean - target. -/ classical have hJ := (Even.convexOn_pow (by norm_num : Even (2 : ℕ)) : ConvexOn ℝ univ (fun x : ℝ ↦ x ^ 2)).map_sum_le (t := univ) (w := fun z ↦ E.conditionalWeight θ s z) (p := fun z ↦ est z - target) (fun z _ ↦ E.conditionalWeight_nonneg θ s z) (by simpa using E.conditionalWeight_sum θ s) (fun _ _ ↦ Set.mem_univ _) have hcenter : (∑ z, E.conditionalWeight θ s z • (est z - target)) = E.conditionalMean est θ s - target := by simp only [smul_eq_mul, mul_sub, Finset.sum_sub_distrib, conditionalMean, ← Finset.sum_mul, E.conditionalWeight_sum, one_mul] rw [hcenter] at hJ simpa only [smul_eq_mul] using hJ -
statisticRisk_conditionalMean_le_fullRisktheorem — At any fixed state, composing that state's conditional mean with the statistic has no larger squared-error risk than the original estimator. This is a fiberwise analytic inequality; the conditional mean in this statement is not asserted to be one estimator shared across states.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4target :Latent → ℝest :Allocation × Observation → ℝθ :LatentconclusionE.statisticRisk target (E.conditionalMean est θ) θ ≤ E.fullRisk target est θProof (Lean source)
theorem statisticRisk_conditionalMean_le_fullRisk (target : Latent → ℝ) (est : Allocation × Observation → ℝ) (θ : Latent) : E.statisticRisk target (E.conditionalMean est θ) θ ≤ E.fullRisk target est θ := by /- Rewrite both risks through disintegrate_sum and sum conditionalMean_sq_le with the nonnegative statistic masses. -/ classical have hstat : E.statisticRisk target (E.conditionalMean est θ) θ = ∑ s, E.statisticMass θ s * (E.conditionalMean est θ s - target θ) ^ 2 := by simp only [statisticRisk, statisticMass, Finset.sum_mul] rw [Finset.sum_comm] simp rw [hstat, fullRisk, E.disintegrate_sum] exact Finset.sum_le_sum fun s _ ↦ mul_le_mul_of_nonneg_left (E.conditionalMean_sq_le (target θ) est θ s) (E.statisticMass_nonneg θ s) -
conditionalMean_eq_commonRaoBlackwellEstimatortheorem — On every positive statewise fiber, the state-indexed conditional mean equals the common Rao--Blackwell estimator supplied by the sufficient conditional kernel.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4K :E.CommonConditionalKernelest :Allocation × Observation → ℝθ :Latents :Statistichpos :0 < E.statisticMass θ sconclusionE.conditionalMean est θ s = E.commonRaoBlackwellEstimator K est sProof (Lean source)
theorem conditionalMean_eq_commonRaoBlackwellEstimator (K : E.CommonConditionalKernel) (est : Allocation × Observation → ℝ) (θ : Latent) (s : Statistic) (hpos : 0 < E.statisticMass θ s) : E.conditionalMean est θ s = E.commonRaoBlackwellEstimator K est s := by apply Finset.sum_congr rfl intro z _ rw [K.eq_conditionalWeight θ s hpos z] -
measurable_commonRaoBlackwellEstimatortheorem — On finite statistic spaces, the common Rao--Blackwell estimator is measurable for the discrete sigma algebra.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4MeasurableSpace StatisticMeasurableSingletonClass StatisticK :E.CommonConditionalKernelest :Allocation × Observation → ℝconclusionMeasurable (E.commonRaoBlackwellEstimator K est)Proof (Lean source)
theorem measurable_commonRaoBlackwellEstimator [MeasurableSpace Statistic] [MeasurableSingletonClass Statistic] (K : E.CommonConditionalKernel) (est : Allocation × Observation → ℝ) : Measurable (E.commonRaoBlackwellEstimator K est) := by exact measurable_of_finite _ -
statisticRisk_commonRaoBlackwellEstimator_le_fullRisktheorem — A common sufficient conditional kernel produces one statistic-only Rao--Blackwell estimator whose squared-error risk is no larger at every latent state.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4K :E.CommonConditionalKerneltarget :Latent → ℝest :Allocation × Observation → ℝθ :LatentconclusionE.statisticRisk target (E.commonRaoBlackwellEstimator K est) θ ≤ E.fullRisk target est θProof (Lean source)
theorem statisticRisk_commonRaoBlackwellEstimator_le_fullRisk (K : E.CommonConditionalKernel) (target : Latent → ℝ) (est : Allocation × Observation → ℝ) (θ : Latent) : E.statisticRisk target (E.commonRaoBlackwellEstimator K est) θ ≤ E.fullRisk target est θ := by /- Apply the state-indexed contraction on positive statistic fibers. Null fibers vanish after multiplication by statisticMass, so no cross-state support assumption is needed. -/ classical have hrb : E.statisticRisk target (E.commonRaoBlackwellEstimator K est) θ = ∑ s, E.statisticMass θ s * (E.commonRaoBlackwellEstimator K est s - target θ) ^ 2 := by simp only [statisticRisk, statisticMass, Finset.sum_mul] rw [Finset.sum_comm] simp have hcm : E.statisticRisk target (E.conditionalMean est θ) θ = ∑ s, E.statisticMass θ s * (E.conditionalMean est θ s - target θ) ^ 2 := by simp only [statisticRisk, statisticMass, Finset.sum_mul] rw [Finset.sum_comm] simp have heq : E.statisticRisk target (E.commonRaoBlackwellEstimator K est) θ = E.statisticRisk target (E.conditionalMean est θ) θ := by rw [hrb, hcm] apply Finset.sum_congr rfl intro s _ by_cases hpos : 0 < E.statisticMass θ s · rw [E.conditionalMean_eq_commonRaoBlackwellEstimator K est θ s hpos] · have hzero : E.statisticMass θ s = 0 := le_antisymm (le_of_not_gt hpos) (E.statisticMass_nonneg θ s) simp [hzero] rw [heq] exact E.statisticRisk_conditionalMean_le_fullRisk target est θ -
priorRisk_commonRaoBlackwellEstimator_letheorem — Under any finite prior on latent states, the common Rao--Blackwell estimator has no larger prior-averaged squared-error risk than the original estimator.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4K :E.CommonConditionalKernelprior :FiniteDesign Latenttarget :Latent → ℝest :Allocation × Observation → ℝconclusionprior.E (E.statisticRisk target (E.commonRaoBlackwellEstimator K est))≤ prior.E (E.fullRisk target est)Proof (Lean source)
theorem priorRisk_commonRaoBlackwellEstimator_le (K : E.CommonConditionalKernel) (prior : FiniteDesign Latent) (target : Latent → ℝ) (est : Allocation × Observation → ℝ) : prior.E (E.statisticRisk target (E.commonRaoBlackwellEstimator K est)) ≤ prior.E (E.fullRisk target est) := by /- Sum the statewise contraction against the nonnegative prior weights. -/ exact Finset.sum_le_sum fun θ _ ↦ mul_le_mul_of_nonneg_left (E.statisticRisk_commonRaoBlackwellEstimator_le_fullRisk K target est θ) (prior.p_nonneg θ) -
worstCaseRisk_commonRaoBlackwellEstimator_letheorem — Under state-independent conditional laws, Rao--Blackwellization weakly decreases the finite worst-case squared risk, in the real-valued worstCaseRisk API.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4K :E.CommonConditionalKerneltarget :Latent → ℝest :Allocation × Observation → ℝconclusionworstCaseRisk (E.statisticRisk target) (E.commonRaoBlackwellEstimator K est)≤ worstCaseRisk (E.fullRisk target) estProof (Lean source)
theorem worstCaseRisk_commonRaoBlackwellEstimator_le (K : E.CommonConditionalKernel) (target : Latent → ℝ) (est : Allocation × Observation → ℝ) : worstCaseRisk (E.statisticRisk target) (E.commonRaoBlackwellEstimator K est) ≤ worstCaseRisk (E.fullRisk target) est := by /- Finite state spaces bound both risk ranges. Apply worstCaseRisk_le to the statewise contraction followed by le_worstCaseRisk for the full estimator. -/ cases isEmpty_or_nonempty Latent with | inl _ => simp only [worstCaseRisk_of_isEmpty_class] exact le_rfl | inr _ => apply worstCaseRisk_le intro θ exact (E.statisticRisk_commonRaoBlackwellEstimator_le_fullRisk K target est θ).trans (le_worstCaseRisk (Set.finite_range _ |>.bddAbove) θ) -
minimaxValue_statistic_le_full_of_commonConditionalKerneltheorem — If every full-data estimator is Rao--Blackwellized through state-independent conditionals, the minimax value over statistic-only estimators is no larger than the full-data minimax value.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4K :E.CommonConditionalKerneltarget :Latent → ℝconclusionminimaxValue (E.statisticRisk target)≤ minimaxValue (E.fullRisk target)Proof (Lean source)
theorem minimaxValue_statistic_le_full_of_commonConditionalKernel (K : E.CommonConditionalKernel) (target : Latent → ℝ) : minimaxValue (E.statisticRisk target) ≤ minimaxValue (E.fullRisk target) := by /- Use minimaxValue_le_minimaxValue, pairing each full estimator with its common raoBlackwellEstimator. Nonnegativity supplies the lower bound for statistic risks. -/ apply minimaxValue_le_minimaxValue (bddBelow_range_worstCaseRisk fun est θ ↦ E.statisticRisk_nonneg target est θ) intro est exact ⟨E.commonRaoBlackwellEstimator K est, E.worstCaseRisk_commonRaoBlackwellEstimator_le K target est⟩ -
measurable_raoBlackwellEstimatortheorem — The factorization-based Rao--Blackwell estimator is measurable on a finite discrete statistic space.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4MeasurableSpace StatisticMeasurableSingletonClass StatisticF :E.SufficientFactorizationest :Allocation × Observation → ℝconclusionMeasurable (E.raoBlackwellEstimator F est)Proof (Lean source)
theorem measurable_raoBlackwellEstimator [MeasurableSpace Statistic] [MeasurableSingletonClass Statistic] (F : E.SufficientFactorization) (est : Allocation × Observation → ℝ) : Measurable (E.raoBlackwellEstimator F est) := by exact E.measurable_commonRaoBlackwellEstimator F.toCommonConditionalKernel est -
priorRisk_raoBlackwellEstimator_letheorem — Under any finite prior, the one statistic-only estimator derived from a sufficient factorization has no larger prior-averaged squared-error risk than the full-data estimator.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4F :E.SufficientFactorizationprior :FiniteDesign Latenttarget :Latent → ℝest :Allocation × Observation → ℝconclusionprior.E (E.statisticRisk target (E.raoBlackwellEstimator F est))≤ prior.E (E.fullRisk target est)Proof (Lean source)
theorem priorRisk_raoBlackwellEstimator_le (F : E.SufficientFactorization) (prior : FiniteDesign Latent) (target : Latent → ℝ) (est : Allocation × Observation → ℝ) : prior.E (E.statisticRisk target (E.raoBlackwellEstimator F est)) ≤ prior.E (E.fullRisk target est) := by exact E.priorRisk_commonRaoBlackwellEstimator_le F.toCommonConditionalKernel prior target est -
worstCaseRisk_raoBlackwellEstimator_letheorem — Under a sufficient factorization, the one statistic-only Rao--Blackwell estimator has no larger finite worst-case squared risk than the full-data estimator.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4F :E.SufficientFactorizationtarget :Latent → ℝest :Allocation × Observation → ℝconclusionworstCaseRisk (E.statisticRisk target) (E.raoBlackwellEstimator F est)≤ worstCaseRisk (E.fullRisk target) estProof (Lean source)
theorem worstCaseRisk_raoBlackwellEstimator_le (F : E.SufficientFactorization) (target : Latent → ℝ) (est : Allocation × Observation → ℝ) : worstCaseRisk (E.statisticRisk target) (E.raoBlackwellEstimator F est) ≤ worstCaseRisk (E.fullRisk target) est := by exact E.worstCaseRisk_commonRaoBlackwellEstimator_le F.toCommonConditionalKernel target est -
minimaxValue_statistic_le_fulltheorem — If the statistic satisfies the finite factorization criterion, its estimator class has minimax squared-risk value no larger than the full-data estimator class.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4F :E.SufficientFactorizationtarget :Latent → ℝconclusionminimaxValue (E.statisticRisk target)≤ minimaxValue (E.fullRisk target)Proof (Lean source)
theorem minimaxValue_statistic_le_full (F : E.SufficientFactorization) (target : Latent → ℝ) : minimaxValue (E.statisticRisk target) ≤ minimaxValue (E.fullRisk target) := by exact E.minimaxValue_statistic_le_full_of_commonConditionalKernel F.toCommonConditionalKernel target
DesignPushforward 5 core · 14 supporting This module develops finite conditional expectation along an arbitrary deterministic coarsening of a finite randomization design. ★ E_map_conditionalMeanAlongMap_sq_le
Conditional means along finite-design pushforwards
This module develops finite conditional expectation along an arbitrary deterministic coarsening of a finite randomization design. Fibers of zero design mass are totalized by a caller-supplied default, while exact disintegration, interval preservation, and squared-loss Rao--Blackwell contraction remain valid without uniformity, independence, surjectivity, or full support.
def fiberMass reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell
For a finite probability design on source points, a deterministic coarsening map, and a coarsened value, the fiber mass is the total design probability of source points mapped to that value.
Definition (Lean source)
parameters
def
fiberMass D φ b :
ℝ
given by
by classical exact ∑ ω, if φ ω = b then D.p ω else 0
def fiberNumerator reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell
For a finite probability design on source points, a deterministic coarsening map, a real-valued source function indexed by values, a coarsened value, and an index value, the fiber numerator is the sum of the design probability times the source-function value over source points mapped to that coarsened value.
Definition (Lean source)
parameters
Ω :
Type u_1
B :
Type u_2
V :
Type u_3
D :
φ :
Ω → B
h :
Ω → V → ℝ
b :
B
v :
V
def
fiberNumerator D φ h b v :
ℝ
given by
by classical exact ∑ ω, if φ ω = b then D.p ω * h ω v else 0
def conditionalFiberWeight reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell
For a finite probability design on source points, a deterministic coarsening map, a coarsened value, and a source point, the conditional fiber weight is its design probability divided by the fiber mass when that mass is nonzero and the point maps to the value, and zero otherwise.
Definition (Lean source)
parameters
def
conditionalFiberWeight D φ b ω :
ℝ
def conditionalMeanAlongMap reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell
For a finite probability design on source points, a deterministic coarsening map, a real-valued default, a real-valued source function indexed by values, a coarsened value, and an index value, the conditional mean along the map is the design-weighted fiber mean when the fiber has nonzero mass and the supplied default when it has zero mass.
Definition (Lean source)
parameters
Ω :
Type u_1
B :
Type u_2
V :
Type u_3
D :
φ :
Ω → B
d :
ℝ
h :
Ω → V → ℝ
b :
B
v :
V
def
conditionalMeanAlongMap D φ d h b v :
ℝ
given by
theorem E_map_conditionalMeanAlongMap_sq_le reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell
Conditioning over the fibers of any deterministic pushforward weakly contracts covariate-parametric squared loss under an arbitrary finite design.
Formal statement
hypotheses
Ω :
Type u_1
B :
Type u_2
V :
Type u_3
D :
φ :
Ω → B
d :
ℝ
h :
Ω → V → ℝ
v :
B → V
t :
ℝ
conclusion
(D.map φ).E (fun b => (conditionalMeanAlongMap D φ d h b (v b) - t) ^ 2)
≤ D.E (fun ω => (h ω (v (φ ω)) - t) ^ 2)
Proof (Lean source)
theorem E_map_conditionalMeanAlongMap_sq_le
(D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ)
(h : Ω → V → ℝ) (v : B → V) (t : ℝ) :
(D.map φ).E (fun b =>
(conditionalMeanAlongMap D φ d h b (v b) - t) ^ 2) ≤
D.E (fun ω => (h ω (v (φ ω)) - t) ^ 2) := by
classical
simp only [FiniteDesign.E, ← fiberMass_eq_map_p]
rw [← sum_fiberMass_mul_conditionalMeanAlongMap D φ 0
(fun ω v => (h ω v - t) ^ 2) v]
apply Finset.sum_le_sum
intro b _
by_cases hb : fiberMass D φ b = 0
· simp [hb]
· apply mul_le_mul_of_nonneg_left _ (fiberMass_nonneg D φ b)
rw [conditionalMeanAlongMap_eq_sum_conditionalFiberWeight D φ 0
(fun ω v => (h ω v - t) ^ 2) b (v b) hb]
exact conditionalMeanAlongMap_sq_le D φ d h b (v b) t hb
14 supporting declarations (lemmas, instances)
-
fiberMass_eq_map_ptheorem — A coarsening fiber's total design mass equals the probability of its value under the pushforward design.hypothesesconclusionfiberMass D φ b = (D.map φ).p bProof (Lean source)
theorem fiberMass_eq_map_p (D : FiniteDesign Ω) (φ : Ω → B) (b : B) : fiberMass D φ b = (D.map φ).p b := by classical rfl -
fiberMass_nonnegtheorem — Every coarsening fiber has nonnegative design mass.hypothesesconclusion0 ≤ fiberMass D φ bProof (Lean source)
theorem fiberMass_nonneg (D : FiniteDesign Ω) (φ : Ω → B) (b : B) : 0 ≤ fiberMass D φ b := by rw [fiberMass_eq_map_p] exact (D.map φ).p_nonneg b -
fiberMass_sumtheorem — The masses of all coarsening fibers sum to one.hypothesesconclusion∑ b, fiberMass D φ b = 1Proof (Lean source)
theorem fiberMass_sum (D : FiniteDesign Ω) (φ : Ω → B) : ∑ b, fiberMass D φ b = 1 := by simp only [fiberMass_eq_map_p] exact (D.map φ).p_sum -
conditionalFiberWeight_nonnegtheorem — Conditional fiber weights are nonnegative on both positive-mass and null fibers.hypothesesconclusion0 ≤ conditionalFiberWeight D φ b ωProof (Lean source)
theorem conditionalFiberWeight_nonneg (D : FiniteDesign Ω) (φ : Ω → B) (b : B) (ω : Ω) : 0 ≤ conditionalFiberWeight D φ b ω := by classical unfold conditionalFiberWeight by_cases hb : fiberMass D φ b = 0 · simp [hb] by_cases hω : φ ω = b · simp only [hb, hω, if_false, if_true] exact div_nonneg (D.p_nonneg ω) (fiberMass_nonneg D φ b) · simp [hb, hω] -
sum_conditionalFiberWeight_eq_onetheorem — When the requested fiber has nonzero mass, its conditional weights sum to one.hypothesesconclusion∑ ω, conditionalFiberWeight D φ b ω = 1Proof (Lean source)
theorem sum_conditionalFiberWeight_eq_one (D : FiniteDesign Ω) (φ : Ω → B) (b : B) (hb : fiberMass D φ b ≠ 0) : ∑ ω, conditionalFiberWeight D φ b ω = 1 := by classical simp only [conditionalFiberWeight, hb, if_false] calc (∑ ω, if φ ω = b then D.p ω / fiberMass D φ b else 0) = ∑ ω, (if φ ω = b then D.p ω else 0) * (fiberMass D φ b)⁻¹ := by apply Finset.sum_congr rfl intro ω _ by_cases hω : φ ω = b <;> simp [hω, div_eq_mul_inv] _ = fiberMass D φ b * (fiberMass D φ b)⁻¹ := by rw [← Finset.sum_mul] rfl _ = 1 := mul_inv_cancel₀ hb -
p_eq_zero_of_mem_fiberMass_eq_zerotheorem — If a fiber has zero design mass and a source point maps into that fiber, the source point itself has zero design probability.hypothesesΩ :sharedType u_1B :sharedType u_2D :φ :Ω → Bb :Bhb :fiberMass D φ b = 0ω :Ωhω :φ ω = bconclusionD.p ω = 0Proof (Lean source)
theorem p_eq_zero_of_mem_fiberMass_eq_zero (D : FiniteDesign Ω) (φ : Ω → B) (b : B) (hb : fiberMass D φ b = 0) (ω : Ω) (hω : φ ω = b) : D.p ω = 0 := by classical unfold fiberMass at hb have hnonneg : ∀ x ∈ univ, 0 ≤ if φ x = b then D.p x else 0 := by intro x _ by_cases hx : φ x = b <;> simp [hx, D.p_nonneg x] have hzero := (Finset.sum_eq_zero_iff_of_nonneg hnonneg).mp hb simpa [hω] using hzero ω (Finset.mem_univ ω) -
fiberNumerator_eq_zero_of_fiberMass_eq_zerotheorem — If a fiber has zero design mass, the design-weighted numerator of every real-valued source function vanishes on that fiber.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bh :Ω → V → ℝb :Bv :Vhb :fiberMass D φ b = 0conclusionfiberNumerator D φ h b v = 0Proof (Lean source)
theorem fiberNumerator_eq_zero_of_fiberMass_eq_zero (D : FiniteDesign Ω) (φ : Ω → B) (h : Ω → V → ℝ) (b : B) (v : V) (hb : fiberMass D φ b = 0) : fiberNumerator D φ h b v = 0 := by classical unfold fiberNumerator apply Finset.sum_eq_zero intro ω _ by_cases hω : φ ω = b · simp [hω, p_eq_zero_of_mem_fiberMass_eq_zero D φ b hb ω hω] · simp [hω] -
conditionalMeanAlongMap_of_fiberMass_eq_zerotheorem — On a zero-mass fiber, the guarded conditional mean equals its supplied default.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝb :Bv :Vhb :fiberMass D φ b = 0conclusionconditionalMeanAlongMap D φ d h b v = dProof (Lean source)
theorem conditionalMeanAlongMap_of_fiberMass_eq_zero (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (b : B) (v : V) (hb : fiberMass D φ b = 0) : conditionalMeanAlongMap D φ d h b v = d := by simp [conditionalMeanAlongMap, hb] -
conditionalMeanAlongMap_eq_sum_conditionalFiberWeighttheorem — On a nonzero-mass fiber, the guarded conditional mean equals the source-value average under the normalized conditional fiber weights.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝb :Bv :Vhb :fiberMass D φ b ≠ 0conclusionconditionalMeanAlongMap D φ d h b v = ∑ ω, conditionalFiberWeight D φ b ω * h ω vProof (Lean source)
theorem conditionalMeanAlongMap_eq_sum_conditionalFiberWeight (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (b : B) (v : V) (hb : fiberMass D φ b ≠ 0) : conditionalMeanAlongMap D φ d h b v = ∑ ω, conditionalFiberWeight D φ b ω * h ω v := by classical simp only [conditionalMeanAlongMap, hb, if_false, fiberNumerator, conditionalFiberWeight] rw [div_eq_mul_inv, Finset.sum_mul] apply Finset.sum_congr rfl intro ω _ by_cases hω : φ ω = b <;> simp [hω, div_eq_mul_inv] ring -
sum_fiberMass_mul_conditionalMeanAlongMaptheorem — The original design-weighted sum equals the sum of each fiber mass times its guarded conditional mean, with null fibers contributing zero regardless of the default.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝv :B → Vconclusion∑ b, fiberMass D φ b * conditionalMeanAlongMap D φ d h b (v b)= ∑ ω, D.p ω * h ω (v (φ ω))Proof (Lean source)
theorem sum_fiberMass_mul_conditionalMeanAlongMap (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (v : B → V) : ∑ b, fiberMass D φ b * conditionalMeanAlongMap D φ d h b (v b) = ∑ ω, D.p ω * h ω (v (φ ω)) := by classical calc ∑ b, fiberMass D φ b * conditionalMeanAlongMap D φ d h b (v b) = ∑ b, fiberNumerator D φ h b (v b) := by apply Finset.sum_congr rfl intro b _ by_cases hb : fiberMass D φ b = 0 · rw [conditionalMeanAlongMap_of_fiberMass_eq_zero D φ d h b (v b) hb, hb, zero_mul, fiberNumerator_eq_zero_of_fiberMass_eq_zero D φ h b (v b) hb] · simp only [conditionalMeanAlongMap, hb, if_false] field_simp _ = ∑ ω, D.p ω * h ω (v (φ ω)) := by unfold fiberNumerator rw [Finset.sum_comm] apply Finset.sum_congr rfl intro ω _ simp -
E_map_conditionalMeanAlongMaptheorem — The pushforward expectation of the guarded conditional mean equals the original-design expectation of the source value evaluated at the covariate selected by its coarsening.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝv :B → Vconclusion(D.map φ).E (fun b => conditionalMeanAlongMap D φ d h b (v b))= D.E (fun ω => h ω (v (φ ω)))Proof (Lean source)
theorem E_map_conditionalMeanAlongMap (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (v : B → V) : (D.map φ).E (fun b => conditionalMeanAlongMap D φ d h b (v b)) = D.E (fun ω => h ω (v (φ ω))) := by simpa only [FiniteDesign.E, ← fiberMass_eq_map_p] using sum_fiberMass_mul_conditionalMeanAlongMap D φ d h v -
E_conditionalMeanAlongMap_comptheorem — Composing the guarded conditional mean with the coarsening has the same expectation under the original design as the corresponding source value.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝv :B → VconclusionD.E (fun ω => conditionalMeanAlongMap D φ d h (φ ω) (v (φ ω)))= D.E (fun ω => h ω (v (φ ω)))Proof (Lean source)
theorem E_conditionalMeanAlongMap_comp (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (v : B → V) : D.E (fun ω => conditionalMeanAlongMap D φ d h (φ ω) (v (φ ω))) = D.E (fun ω => h ω (v (φ ω))) := by rw [← D.E_map φ (fun b => conditionalMeanAlongMap D φ d h b (v b))] exact E_map_conditionalMeanAlongMap D φ d h v -
conditionalMeanAlongMap_mem_Icctheorem — If the default lies in a fixed closed interval and every source value lies in that interval, the guarded conditional mean also lies in the interval.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝb :Bv :Vl u :ℝhd :d ∈ Icc l uhh :∀ ω v, h ω v ∈ Icc l uconclusionconditionalMeanAlongMap D φ d h b v ∈ Icc l uProof (Lean source)
theorem conditionalMeanAlongMap_mem_Icc (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (b : B) (v : V) {l u : ℝ} (hd : d ∈ Icc l u) (hh : ∀ ω v, h ω v ∈ Icc l u) : conditionalMeanAlongMap D φ d h b v ∈ Icc l u := by classical by_cases hb : fiberMass D φ b = 0 · simpa [conditionalMeanAlongMap, hb] using hd rw [conditionalMeanAlongMap_eq_sum_conditionalFiberWeight D φ d h b v hb] constructor · calc l = (∑ ω, conditionalFiberWeight D φ b ω) * l := by rw [sum_conditionalFiberWeight_eq_one D φ b hb, one_mul] _ = ∑ ω, conditionalFiberWeight D φ b ω * l := by rw [Finset.sum_mul] _ ≤ ∑ ω, conditionalFiberWeight D φ b ω * h ω v := by exact Finset.sum_le_sum fun ω _ => mul_le_mul_of_nonneg_left (hh ω v).1 (conditionalFiberWeight_nonneg D φ b ω) · calc ∑ ω, conditionalFiberWeight D φ b ω * h ω v ≤ ∑ ω, conditionalFiberWeight D φ b ω * u := by exact Finset.sum_le_sum fun ω _ => mul_le_mul_of_nonneg_left (hh ω v).2 (conditionalFiberWeight_nonneg D φ b ω) _ = (∑ ω, conditionalFiberWeight D φ b ω) * u := by rw [Finset.sum_mul] _ = u := by rw [sum_conditionalFiberWeight_eq_one D φ b hb, one_mul] -
conditionalMeanAlongMap_sq_letheorem — On a nonzero-mass fiber, the squared loss of the conditional mean is at most the conditional fiber average of the source squared losses.hypothesesΩ :sharedType u_1B :sharedType u_2V :sharedType u_3D :φ :Ω → Bd :ℝh :Ω → V → ℝb :Bv :Vt :ℝhb :fiberMass D φ b ≠ 0conclusion(conditionalMeanAlongMap D φ d h b v - t) ^ 2≤ ∑ ω, conditionalFiberWeight D φ b ω * (h ω v - t) ^ 2Proof (Lean source)
theorem conditionalMeanAlongMap_sq_le (D : FiniteDesign Ω) (φ : Ω → B) (d : ℝ) (h : Ω → V → ℝ) (b : B) (v : V) (t : ℝ) (hb : fiberMass D φ b ≠ 0) : (conditionalMeanAlongMap D φ d h b v - t) ^ 2 ≤ ∑ ω, conditionalFiberWeight D φ b ω * (h ω v - t) ^ 2 := by classical rw [conditionalMeanAlongMap_eq_sum_conditionalFiberWeight D φ d h b v hb] have hmean : (∑ ω, conditionalFiberWeight D φ b ω * h ω v) - t = ∑ ω, conditionalFiberWeight D φ b ω * (h ω v - t) := by calc (∑ ω, conditionalFiberWeight D φ b ω * h ω v) - t = (∑ ω, conditionalFiberWeight D φ b ω * h ω v) - (∑ ω, conditionalFiberWeight D φ b ω) * t := by rw [sum_conditionalFiberWeight_eq_one D φ b hb, one_mul] _ = ∑ ω, (conditionalFiberWeight D φ b ω * h ω v - conditionalFiberWeight D φ b ω * t) := by rw [Finset.sum_mul, Finset.sum_sub_distrib] _ = ∑ ω, conditionalFiberWeight D φ b ω * (h ω v - t) := by apply Finset.sum_congr rfl intro ω _ ring rw [hmean] simpa only [smul_eq_mul] using (show Even 2 from even_two).convexOn_pow.map_sum_le (fun ω _ => conditionalFiberWeight_nonneg D φ b ω) (sum_conditionalFiberWeight_eq_one D φ b hb) (fun _ _ => Set.mem_univ _)
KernelBridge 6 core · 12 supporting This module realizes the algebraic finite designs from Core as genuine Markov kernels on finite labeled measurable spaces. ★ kernelMean_conditionalKernel_eq_conditionalMean
Markov-kernel and finite-Bayes bridges
This module realizes the algebraic finite designs from Core as genuine Markov kernels on
finite labeled measurable spaces. It exposes the full-data law, statistic law, and guarded
conditional laws in the kernel API, including the factorization-derived common conditional law
and a finite-prior posterior law of the latent state given the statistic. Singleton
probabilities are identified with real finite masses, so the kernels can be passed directly to
Causalean.Stat.Minimax.FiniteKernelBayes without an ENNReal loss conversion.
def fullKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Given a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with σ-algebras on the latent, allocation, and observation spaces and measurable singleton latent states, the full-data Markov kernel assigns to each latent state the experiment's finite joint probability law of the allocation and observation at that state.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
def
given by
Kernel.ofFunOfCountable fun θ ↦ ({ p := E.jointMass θ p_nonneg := E.jointMass_nonneg θ p_sum := E.jointMass_sum θ } : FiniteDesign (Allocation × Observation)).toMeasure
def statisticKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Given a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with σ-algebras on the latent and statistic spaces and measurable singleton latent states, the statistic Markov kernel assigns to each latent state the experiment's finite marginal probability law of the statistic.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
def
given by
Kernel.ofFunOfCountable fun θ ↦ (E.statisticDesign θ).toMeasure
def conditionalKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Given a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with σ-algebras on the allocation, observation, and statistic spaces and measurable singleton statistic values, and a latent state, the guarded conditional Markov kernel assigns to each statistic value the experiment's conditional probability law of the allocation--observation pair at that state, using the fallback law when the statistic fiber has zero probability.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
θ :
Latent
def
given by
Kernel.ofFunOfCountable fun s ↦ (E.conditionalDesign θ s).toMeasure
def commonConditionalMarkovKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Given a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with σ-algebras on the allocation, observation, and statistic spaces and measurable singleton statistic values, and a sufficient factorization of its full-data masses, the common conditional Markov kernel assigns to each statistic value the factorization-induced state-independent conditional probability law of the allocation--observation pair.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
F :
E.SufficientFactorization
def
given by
Kernel.ofFunOfCountable fun s ↦ ({ p := F.toCommonConditionalKernel.weight s p_nonneg := F.toCommonConditionalKernel.weight_nonneg s p_sum := F.toCommonConditionalKernel.weight_sum s } : FiniteDesign (Allocation × Observation)).toMeasure
def posteriorKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
Given a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with σ-algebras on the latent and statistic spaces and measurable singleton statistic values, and a finite prior probability distribution on latent states, the posterior Markov kernel assigns to each statistic value the guarded posterior probability law of the latent state, using the designated fallback law on prior-predictive statistic fibers of zero probability.
Definition (Lean source)
parameters
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
prior :
FiniteDesign Latent
def
given by
Kernel.ofFunOfCountable fun s ↦ (E.posteriorDesign prior s).toMeasure
theorem kernelMean_conditionalKernel_eq_conditionalMean reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.FiniteUniformExperiment
The measure-theoretic conditional-kernel mean of a full-data estimator equals the finite conditional mean, so no ENNReal conversion appears in Rao--Blackwell calculations.
Formal statement
hypotheses
Latent :
Type u_1
Allocation :
Type u_2
Observation :
Type u_3
Statistic :
Type u_4
est :
Allocation × Observation → ℝ
θ :
Latent
s :
Statistic
conclusion
(∫ z, est z ∂(E.conditionalKernel θ) s) = E.conditionalMean est θ s
Proof (Lean source)
theorem kernelMean_conditionalKernel_eq_conditionalMean
(est : Allocation × Observation → ℝ) (θ : Latent) (s : Statistic) :
(∫ z, est z ∂(E.conditionalKernel θ) s) = E.conditionalMean est θ s := by
/- Evaluate the finite-design integral and unfold the two finite expectations. -/
change (∫ z, est z ∂(E.conditionalDesign θ s).toMeasure) = E.conditionalMean est θ s
rw [FiniteDesign.integral_toMeasure]
rfl
12 supporting declarations (lemmas, instances)
-
fullKernel_isMarkovKernelinstance — For a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with distinguishable allocation, observation, and statistic values, σ-algebras on the latent, allocation, and observation spaces, and measurable singleton latent states, the full-data kernel is a Markov kernel: at every latent state, its output law is a probability measure.parametersLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4instancegiven byisProbabilityMeasure θ := by change IsProbabilityMeasure (({ p := E.jointMass θ p_nonneg := E.jointMass_nonneg θ p_sum := E.jointMass_sum θ } : FiniteDesign (Allocation × Observation)).toMeasure) infer_instance -
statisticKernel_isMarkovKernelinstance — For a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with distinguishable allocation, observation, and statistic values, σ-algebras on the latent and statistic spaces, and measurable singleton latent states, the statistic kernel is a Markov kernel: at every latent state, its output law is a probability measure.parametersLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4instancegiven byisProbabilityMeasure θ := by change IsProbabilityMeasure (E.statisticDesign θ).toMeasure infer_instance -
conditionalKernel_isMarkovKernelinstance — For a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with distinguishable allocation, observation, and statistic values, σ-algebras on the allocation, observation, and statistic spaces, and measurable singleton statistic values and a latent state, the guarded conditional kernel is a Markov kernel: at every statistic value, including a zero-probability fibre, its output law is a probability measure.parametersLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latentinstancegiven byisProbabilityMeasure s := by change IsProbabilityMeasure (E.conditionalDesign θ s).toMeasure infer_instance -
commonConditionalMarkovKernel_isMarkovKernelinstance — For a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with distinguishable allocation, observation, and statistic values, σ-algebras on the allocation, observation, and statistic spaces, and measurable singleton statistic values and a sufficient factorization of its full-data probability masses, the factorization-derived common conditional kernel is a Markov kernel: at every statistic value, including a zero-probability fibre, its output law is a probability measure.parametersLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4F :E.SufficientFactorizationinstancecommonConditionalMarkovKernel_isMarkovKernel E F :IsMarkovKernel (E.commonConditionalMarkovKernel F)given byisProbabilityMeasure s := by change IsProbabilityMeasure (({ p := F.toCommonConditionalKernel.weight s p_nonneg := F.toCommonConditionalKernel.weight_nonneg s p_sum := F.toCommonConditionalKernel.weight_sum s } : FiniteDesign (Allocation × Observation)).toMeasure) infer_instance -
posteriorKernel_isMarkovKernelinstance — For a finite uniform experiment on finite latent, allocation, observation, and statistic spaces, with distinguishable allocation, observation, and statistic values, σ-algebras on the latent and statistic spaces, and measurable singleton statistic values and a finite prior probability distribution on latent states, the guarded posterior kernel is a Markov kernel: at every statistic value, including a prior-predictive zero-probability fibre, its output law is a probability measure.parametersLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latentinstancegiven byisProbabilityMeasure s := by change IsProbabilityMeasure (E.posteriorDesign prior s).toMeasure infer_instance -
fullKernel_singletonRealtheorem — The real singleton probability of the full-data kernel equals the finite joint mass.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latentz :Allocation × Observationconclusion(E.fullKernel θ).real {z} = E.jointMass θ zProof (Lean source)
theorem fullKernel_singletonReal (θ : Latent) (z : Allocation × Observation) : (E.fullKernel θ).real {z} = E.jointMass θ z := by change (({ p := E.jointMass θ p_nonneg := E.jointMass_nonneg θ p_sum := E.jointMass_sum θ } : FiniteDesign (Allocation × Observation)).toMeasure).real {z} = E.jointMass θ z rw [show ({z} : Set (Allocation × Observation)) = {x | x = z} by ext; simp] rw [FiniteDesign.toMeasure_real_setOf] change (∑ x, E.jointMass θ x * if x = z then 1 else 0) = E.jointMass θ z simp -
statisticKernel_singletonRealtheorem — The real singleton probability of the statistic kernel equals the finite statistic mass.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statisticconclusion(E.statisticKernel θ).real {s} = E.statisticMass θ sProof (Lean source)
theorem statisticKernel_singletonReal (θ : Latent) (s : Statistic) : (E.statisticKernel θ).real {s} = E.statisticMass θ s := by change (E.statisticDesign θ).toMeasure.real {s} = E.statisticMass θ s rw [show ({s} : Set Statistic) = {x | x = s} by ext; simp] rw [FiniteDesign.toMeasure_real_setOf] change (∑ x, E.statisticMass θ x * if x = s then 1 else 0) = E.statisticMass θ s simp -
conditionalKernel_singletonRealtheorem — The real singleton probability of the guarded conditional kernel equals its finite conditional weight.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4θ :Latents :Statisticz :Allocation × Observationconclusion(E.conditionalKernel θ s).real {z} = E.conditionalWeight θ s zProof (Lean source)
theorem conditionalKernel_singletonReal (θ : Latent) (s : Statistic) (z : Allocation × Observation) : (E.conditionalKernel θ s).real {z} = E.conditionalWeight θ s z := by change (E.conditionalDesign θ s).toMeasure.real {z} = E.conditionalWeight θ s z rw [show ({z} : Set (Allocation × Observation)) = {x | x = z} by ext; simp] rw [FiniteDesign.toMeasure_real_setOf] change (∑ x, E.conditionalWeight θ s x * if x = z then 1 else 0) = E.conditionalWeight θ s z simp -
commonConditionalMarkovKernel_singletonRealtheorem — The real singleton probability of the factorization-derived common conditional Markov kernel equals its finite common conditional weight.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4F :E.SufficientFactorizations :Statisticz :Allocation × Observationconclusion(E.commonConditionalMarkovKernel F s).real {z} = F.toCommonConditionalKernel.weight s zProof (Lean source)
theorem commonConditionalMarkovKernel_singletonReal (F : E.SufficientFactorization) (s : Statistic) (z : Allocation × Observation) : (E.commonConditionalMarkovKernel F s).real {z} = F.toCommonConditionalKernel.weight s z := by change (({ p := F.toCommonConditionalKernel.weight s p_nonneg := F.toCommonConditionalKernel.weight_nonneg s p_sum := F.toCommonConditionalKernel.weight_sum s } : FiniteDesign (Allocation × Observation)).toMeasure).real {z} = F.toCommonConditionalKernel.weight s z rw [show ({z} : Set (Allocation × Observation)) = {x | x = z} by ext; simp] rw [FiniteDesign.toMeasure_real_setOf] change (∑ x, F.toCommonConditionalKernel.weight s x * if x = z then 1 else 0) = F.toCommonConditionalKernel.weight s z simp -
posteriorKernel_singletonRealtheorem — The real singleton probability of the finite-prior posterior kernel equals the guarded posterior weight of that latent state.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4prior :FiniteDesign Latents :Statisticθ :Latentconclusion(E.posteriorKernel prior s).real {θ} = E.posteriorWeight prior s θProof (Lean source)
theorem posteriorKernel_singletonReal (prior : FiniteDesign Latent) (s : Statistic) (θ : Latent) : (E.posteriorKernel prior s).real {θ} = E.posteriorWeight prior s θ := by classical change (E.posteriorDesign prior s).toMeasure.real {θ} = E.posteriorWeight prior s θ rw [show ({θ} : Set Latent) = {x | x = θ} by ext; simp] rw [FiniteDesign.toMeasure_real_setOf] change (∑ x, E.posteriorWeight prior s x * if x = θ then 1 else 0) = E.posteriorWeight prior s θ simp -
kernelAverageLoss_statisticKernel_eq_sumtheorem — Kernel averaging through the statistic kernel is exactly the real finite sum of statistic losses weighted by their statistic masses, matching FiniteKernelBayes.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4Action :Type*loss :Action → Statistic → ℝa :Actionθ :LatentconclusionkernelAverageLoss E.statisticKernel loss a θ= ∑ s, E.statisticMass θ s * loss a sProof (Lean source)
theorem kernelAverageLoss_statisticKernel_eq_sum {Action : Type*} (loss : Action → Statistic → ℝ) (a : Action) (θ : Latent) : kernelAverageLoss E.statisticKernel loss a θ = ∑ s, E.statisticMass θ s * loss a s := by /- Rewrite with kernelAverageLoss_eq_sum and the singleton bridge. -/ letI : Nonempty Statistic := ⟨E.sampleStatistic E.fallbackSample⟩ rw [kernelAverageLoss_eq_sum] simp_rw [E.statisticKernel_singletonReal] -
kernelAverageLoss_posteriorKernel_eq_sumtheorem — Kernel averaging a real latent-state loss through the finite-prior posterior kernel is exactly the finite posterior-weighted sum, matching the real FiniteKernelBayes interface.hypothesesLatent :sharedType u_1Allocation :sharedType u_2Observation :sharedType u_3Statistic :sharedType u_4Action :Type*prior :FiniteDesign Latentloss :Action → Latent → ℝa :Actions :StatisticconclusionkernelAverageLoss (E.posteriorKernel prior) loss a s= ∑ θ, E.posteriorWeight prior s θ * loss a θProof (Lean source)
theorem kernelAverageLoss_posteriorKernel_eq_sum {Action : Type*} (prior : FiniteDesign Latent) (loss : Action → Latent → ℝ) (a : Action) (s : Statistic) : kernelAverageLoss (E.posteriorKernel prior) loss a s = ∑ θ, E.posteriorWeight prior s θ * loss a θ := by change (∫ θ, loss a θ ∂(E.posteriorDesign prior s).toMeasure) = ∑ θ, E.posteriorWeight prior s θ * loss a θ rw [FiniteDesign.integral_toMeasure] rfl