Add unit-level contrasts and finite-population average effects

[bocowgill]

Motivation

Add the next small potential-outcomes layer after #40 and #41: a unit-level contrast and its average over a finite population. This gives us a useful estimand without adding assignment mechanisms, observed outcomes, probability, identification, estimation, or inference.

Implementation: #44

Proposed Lean API

Create Statlib/Causal/PotentialResponse/Contrast.lean with the following API:

open scoped BigOperators

namespace PotentialResponse

variable {Intervention Unit Value : Type*}

/-- 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) :
    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

/-- 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.

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]
    [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

The file imports Statlib.Causal.PotentialResponse and Mathlib.Algebra.BigOperators.Expect; Statlib.lean imports the new module.

Mathematical role

• Primitive objects: none; this builds on PotentialResponse.
• Derived definitions: contrast and finitePopulationAverageContrast.
• Assumptions: no causal assumptions. contrast needs only Sub Value; the signed laws use AddGroup Value. The finite average uses Fintype Unit, AddCommGroup Value, and Module ℚ≥0 Value, but no probability measure. Its value for empty Unit is zero by algebraic convention, not a substantive causal claim.
• Estimands: the unit-level contrast and its finite-population average. The latter is the conventional ATE when interventions encode two unit-level treatments; with complete allocation vectors it instead compares regimes and does not assume noninterference.
• Identification theorems: none.
• Estimators and statistical inference: none.

More general or weighted contrasts, averages over an explicit Finset Unit, and superpopulation effects are future extensions for applications that need them, not requirements of #44. Assignment mechanisms, recorded outcomes, consistency, identification, estimators, and inference also remain out of scope.

Textbooks consulted

• Peng Ding, A First Course in Causal Inference
• Guido W. Imbens and Donald B. Rubin, Causal Inference for Statistics, Social, and Biomedical Sciences: An Introduction

[bocowgill]

@rajarshi-mukherjee24 @richardkwo, I’d welcome your feedback on this proposed next layer, particularly the API names and the typeclass assumptions for finite-population averages.

[rajarshi-mukherjee24]

1. Sub Value vs AddGroup Value and types of Contrasts: For contrast definition one right now uses only [Sub Value]. Of course, this may be the weakest assumption needed. However, I am curious if we want to also think about algebraic laws and manipulations. Can we provide some documentation/discussion on choice between using [AddGroup Value] vs [Sub Value]. I think if we follow Mathlib-style approach, Sub Value might make more sense to keep the definition general while introducing the mathematically meaningful signed properties under the appropriate stronger assumptions – but its worth thinking about. Also wondering if contrast should be defined more generally – e.g. while considering more than two potential outcomes? If one considers a vector of potential response and one can define contrast through inner product with a vector whose elements sum to zero. One can be even more general and have a general space of potential response, have a measure on it, take an element in the space whose integral w.r.t. the measure is 0 and take inner product with it. It might be worthwhile documenting choices accordingly.
2. Some simple corollaries/laws: As you with the identity and associativity laws added for PotentialResponse.id and comp in the earlier PR, do we think it would be useful for this API to record its elementary algebraic behavior rather than requiring downstream users to unfold the definition? For example even very simple things like contrast of same intervention is zero or swapping interventions gives negative of the same contrast etc? These are simple consequences of the definitions, but named theorems might give downstream proofs a stable interface.
3. Finite Population related: With [Fintype Unit] and 𝔼 unit, response.contrast intervention₁ intervention₀ unit, we are treating the type Unit itself is the complete finite target population. Thus 𝔼 unit, ... is the uniform Finset.expect over Finset.univ and it does not introduce a probability law, random sampling, or a superpopulation expectation. Should we state directly in the declaration-level documentation that:
   • Unit represents the entire finite target population;
   • every unit receives equal weight;
   • the notation 𝔼 here denotes finite uniform averaging over Finset.univ;
   • no probability distribution is being introduced.
4. Finite, Infinite, and Superpopulation I was wondering if the eventual goal is also to support finite- and superpopulation estimands on the same unit space and if so whether it would be useful to consider the more general finite operation with something like
   def finitePopulationAverageContrastSub
   [AddCommGroup Value] [Module ℚ≥0 Value]
   (response : PotentialResponse Intervention Unit Value)
   (population : Finset Unit)
   (intervention₁ intervention₀ : Intervention) :
   Value :=
   𝔼 unit ∈ population,
   response.contrast intervention₁ intervention₀ unit
   This defines relevant things on finite S, a part of U and without requiring the ambient Unit type itself to be finite. The currently proposed definition could then remain as the relevant specialization? I was thinking if this distinction becomes useful if we later have something like:
   population : Finset Unit
   μ : ProbabilityMeasure Unit
   response : PotentialResponse Intervention Unit ℝ
   on the same ambient unit space. I understand that the issue currently does not have explicit subpopulations in its scope. However, given the eventual finite/superpopulation connection, should we consider adding finitePopulationAverageContrastSub now and retaining the proposed definition as a Finset.univ special case. Of course, if that is considered too large for Add unit-level contrasts and finite-population average effects #43, it should at least be recorded as a natural follow-up, and the current type-as-population interpretation should be documented explicitly. Also, a future superpopulation estimand should be a separate measure-theoretic definition of the form. The code would require additional measure theoretic structure together with an integrability assumption on the contrast.The finite and superpopulation definitions should remain separate but built on the common unit-level contrast: the finite definition is algebraic and uses a finite sum; the superpopulation definition is analytic and uses integration. Then we should have suitable bridge results to connect. These bridge results belong in later probability and sampling modules, not in Add unit-level contrasts and finite-population average effects #43, but maybe worth thinking about.
5. Empty-population convention: I am curious about empty population consideration. I think its good to keep Mathlib’s convention that the average over an empty population is zero but make a note of it. Specifically, the documentation can say that this is an algebraic convention, not a substantive assertion that an empty population has zero causal effect.
   An alternative would be to require [Nonempty Unit], for an explicit finset. Although I do not think that is necessary if the convention is clearly documented.
6. Interpretation of finite-population ATE: The sentence: “For binary treatment, this is the finite-population average treatment effect.”
   can be qualified further. In the general API, this is an average contrast between two interventions. It is the conventional finite-population ATE when the interventions encode the two unit-level treatments. However, if Intervention is instead a complete allocation vector, as permitted by [Question] Introduce a minimal potential-response core #40, the object is an average contrast between two allocations or regimes and should not be read as silently imposing no interference. Once again this is a clarification.

[bocowgill]

Thanks, Rajarshi. I’ve updated #44 and the issue description. Responding to your points in order:

1. I kept the existing contrast definition at [Sub Value], as you suggest, and documented that choice in its docstring. The new laws involving zero and negation use [AddGroup Value]. The two-intervention definition is not meant to rule out more general contrasts. With suitable scalar structure, zero-sum weights over several interventions could give a finite generalization; an inner product could express that construction in the finite-dimensional, real-valued case. A measure-based version would also require choices about the measured space, a zero-integral condition, and integrability. The issue records broader contrasts as possible follow-ups, but I have not chosen one of those APIs for Add unit-level contrasts and finite-population average effects #44.

2. I added the named laws contrast_self and contrast_swap. I did not mark contrast_self as @[simp]: the existing simp rules already prove it, and lint flagged the extra attribute as redundant.

3. The average’s docstring now says that Unit is the entire finite target population, each unit has equal weight, and 𝔼 is Finset.expect over Finset.univ. It introduces no probability distribution or sampling mechanism.

4. A finite-subset average and a superpopulation average could use the same unit-level contrast on the same Unit type. A later definition taking population : Finset Unit would not require [Fintype Unit]; the current whole-population definition would be its Finset.univ case. A separate superpopulation definition would integrate over a probability measure on Unit, with the necessary measurability and integrability assumptions. A bridge theorem could compare them for a nonempty finite population equipped with its uniform measure. I’ve left these as follow-ups and documented the current type-as-population interpretation.

5. I kept mathlib’s zero value for an empty population and documented that it is an algebraic convention, not a claim about causal effects.

6. I qualified the ATE interpretation: it applies when interventions represent unit-level treatments. With complete allocation vectors, the definition compares regimes and does not assume noninterference.

The changes are pushed and CI passes. If this resolves the questions relevant to #44, would you take another look at the PR? I’d be glad to discuss the broader contrast and population APIs separately.

[qingyuanzhao]

Hi Bo, thanks for continuing the work!

I met with @richardkwo and @zixiaowang17 today and we discussed your PR (the meeting was mostly about the goal of our graphical models project). Here are a few points from that discussion:

1. We thought the pairwise subtraction is a bit narrow as a definition of causal contrast, especially considering you are building the basic infrastructure at the moment. Personally I would define causal contrast as any function of potential outcomes. I am a bit biased because I work on counterfactual problems (so generally partially identified), but perhaps we also want general definitions for a lean library?
2. We thought you might want to also consider, as part of this effort, formalizing the concept of exposure mapping, which maps treatment assignments (higher dimensional, often one dimension per experimental unit but that's not necessary) to exposures (lower dimensional). This concept is quite common in study interference (Aronow and Samii were among the first people popularizing that: https://arxiv.org/abs/1305.6156). In teaching causal inference I also find it useful to distinguish treatment (which is assigned by the experimenter) and exposure (which is received by the experimental subject).
3. We thought it might be useful to have a more concrete milestone in mind when having this discussion. Some ideas are unbiasedness of Horvitz-Thompson estimator (I think there is a version in the Aronow-Samii paper) and, if you are more ambitious, Neyman's randomization variance calculation (there is an algebraic and tedious proof in the Imbens-Rubin book and a more interesting proof that David Cox suggested in passage).

It would also be great if we could meet up at some point to coordinate.