From 3b8bc1799aa1092267a1ae100258991eba9f25a8 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Sat, 19 Sep 2026 09:45:07 -0400 Subject: [PATCH 1/3] Add potential-response contrasts --- Statlib.lean | 1 + .../Causal/PotentialResponse/Contrast.lean | 64 +++++++++++++++++++ 2 files changed, 65 insertions(+) create mode 100644 Statlib/Causal/PotentialResponse/Contrast.lean diff --git a/Statlib.lean b/Statlib.lean index 707dba3..e8a9d9f 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -1,4 +1,5 @@ import Statlib.Causal.PotentialResponse +import Statlib.Causal.PotentialResponse.Contrast import Statlib.EValues.DPI import Statlib.EValues.EVariable import Statlib.EValues.Utility.Basic diff --git a/Statlib/Causal/PotentialResponse/Contrast.lean b/Statlib/Causal/PotentialResponse/Contrast.lean new file mode 100644 index 0000000..54da6d1 --- /dev/null +++ b/Statlib/Causal/PotentialResponse/Contrast.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Bo Cowgill. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bo Cowgill +-/ + +module + +public import Mathlib.Algebra.BigOperators.Expect +public import Statlib.Causal.PotentialResponse + +/-! +# Potential-Response Contrasts + +This module defines unit-level contrasts between two interventions and their averages over a finite +population. It introduces estimands but no assignment mechanism, causal assumption, identification +result, estimator, or statistical inference. +-/ + +@[expose] public section + +open scoped BigOperators + +namespace PotentialResponse + +variable {Intervention Unit Value : Type*} + +/-- The unit-level contrast between two interventions, first minus second. -/ +def contrast [Sub Value] + (response : PotentialResponse Intervention Unit Value) + (intervention₁ intervention₀ : Intervention) : + Unit → Value := + fun unit ↦ response intervention₁ unit - response intervention₀ unit + +@[simp] theorem contrast_apply [Sub Value] + (response : PotentialResponse Intervention Unit Value) + (intervention₁ intervention₀ : Intervention) + (unit : Unit) : + response.contrast intervention₁ intervention₀ unit = + response intervention₁ unit - response intervention₀ unit := rfl + +/-- The average unit-level contrast over a finite population. + +This is zero when the population is empty, following the convention for `Finset.expect`. +-/ +def finitePopulationAverageContrast + [Fintype Unit] + [AddCommGroup Value] [Module ℚ≥0 Value] + (response : PotentialResponse Intervention Unit Value) + (intervention₁ intervention₀ : Intervention) : + Value := + 𝔼 unit, response.contrast intervention₁ intervention₀ unit + +theorem finitePopulationAverageContrast_eq_sub + [Fintype Unit] + [AddCommGroup Value] [Module ℚ≥0 Value] + (response : PotentialResponse Intervention Unit Value) + (intervention₁ intervention₀ : Intervention) : + response.finitePopulationAverageContrast intervention₁ intervention₀ = + (𝔼 unit, response intervention₁ unit) - + (𝔼 unit, response intervention₀ unit) := by + simp [finitePopulationAverageContrast, Finset.expect_sub_distrib] + +end PotentialResponse From cc1bcb9b05c30632b74c6b73bf57e0e868987e64 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Wed, 30 Sep 2026 09:11:36 -0400 Subject: [PATCH 2/3] Add basic potential-response contrast laws --- Statlib/Causal/PotentialResponse/Contrast.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Statlib/Causal/PotentialResponse/Contrast.lean b/Statlib/Causal/PotentialResponse/Contrast.lean index 54da6d1..640466c 100644 --- a/Statlib/Causal/PotentialResponse/Contrast.lean +++ b/Statlib/Causal/PotentialResponse/Contrast.lean @@ -39,6 +39,21 @@ def contrast [Sub Value] response.contrast intervention₁ intervention₀ unit = response intervention₁ unit - response intervention₀ unit := rfl +/-- A unit's contrast with itself is zero. -/ +theorem contrast_self [AddGroup Value] + (response : PotentialResponse Intervention Unit Value) + (intervention : Intervention) (unit : Unit) : + response.contrast intervention intervention unit = 0 := by + simp + +/-- Swapping the interventions negates the unit-level contrast. -/ +theorem contrast_swap [AddGroup Value] + (response : PotentialResponse Intervention Unit Value) + (intervention₁ intervention₀ : Intervention) (unit : Unit) : + response.contrast intervention₁ intervention₀ unit = + -response.contrast intervention₀ intervention₁ unit := by + simp only [contrast_apply, neg_sub] + /-- The average unit-level contrast over a finite population. This is zero when the population is empty, following the convention for `Finset.expect`. From cf4407f83a0e739687dd5a41f2e7dff00cdcba59 Mon Sep 17 00:00:00 2001 From: Bo Cowgill Date: Wed, 30 Sep 2026 09:16:59 -0400 Subject: [PATCH 3/3] Clarify finite-population contrast semantics --- Statlib/Causal/PotentialResponse/Contrast.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/Statlib/Causal/PotentialResponse/Contrast.lean b/Statlib/Causal/PotentialResponse/Contrast.lean index 640466c..748824f 100644 --- a/Statlib/Causal/PotentialResponse/Contrast.lean +++ b/Statlib/Causal/PotentialResponse/Contrast.lean @@ -25,7 +25,10 @@ namespace PotentialResponse variable {Intervention Unit Value : Type*} -/-- The unit-level contrast between two interventions, first minus second. -/ +/-- The unit-level contrast between two interventions, first minus second. + +The definition needs only `Sub Value`; laws involving zero and negation use `AddGroup Value`. +-/ def contrast [Sub Value] (response : PotentialResponse Intervention Unit Value) (intervention₁ intervention₀ : Intervention) : @@ -56,7 +59,17 @@ theorem contrast_swap [AddGroup Value] /-- The average unit-level contrast over a finite population. -This is zero when the population is empty, following the convention for `Finset.expect`. +The elements of `Unit` are the entire finite target population. The notation `𝔼` denotes the +uniform `Finset.expect` over `Finset.univ`, giving every unit equal weight. It introduces no +probability distribution, random sampling, or superpopulation expectation. + +For empty `Unit`, this is zero by an algebraic convention of `Finset.expect`, not a substantive +claim about the causal effect in an empty population. + +When the interventions encode two unit-level treatments, this is the conventional +finite-population average treatment effect. If they encode complete allocation vectors, it is +instead an average contrast between two allocation regimes; this definition does not assume +noninterference. -/ def finitePopulationAverageContrast [Fintype Unit]