Formalization: A Lower-Bound Calibration for Joint Margin--Overlap Decay in Offline Policy Learning

A uniform class-level localized envelope supplies the old per-law envelope for every law.

A uniform class-level localized offset envelope supplies the old per-law offset envelope for every law.

The feasible box of schedule exponents is compact when the overlap exponent is positive. The set of pairs consisting of a clip exponent between zero and one half and a margin-window exponent between zero and the clip exponent divided by the overlap exponent is closed and bounded, hence compact. This is what allows the balance objective to attain its supremum.

The balance objective attains its supremum on the feasible box when the overlap exponent is positive: there is a pair of schedule exponents inside the box at which the objective equals the joint feasible exponent. Continuity of the objective on a nonempty compact set supplies the maximizer.

Defining property of the selected feasible maximizer. When the overlap exponent is positive, the chosen pair of schedule exponents lies in the feasible box — clip exponent between zero and one half, margin-window exponent between zero and the clip exponent divided by the overlap exponent — and the balance objective evaluated there equals the joint feasible exponent. This is the specification satisfied by the arbitrary choice of maximizer.

The feasibleMaximizer epsilon-choice lands in the compact feasible box (γ>0). Existence of a maximizer — continuity of feasiblePhi on the nonempty compact box {0≤s≤1/2, 0≤t≤s/γ} (Mathlib IsCompact.exists_isMaxOn) — makes the Classical.epsilon specification inhabited, so its first/second components are feasible. (Certifies def:feasible-rate's "let (s_feas,t_feas) be any maximizer".)

The feasibleMaximizer epsilon-choice MAXIMIZES feasiblePhi over the compact feasible box (γ>0); hence g_joint = feasiblePhi (s_feas) (t_feas).

The selected feasible maximizer attains the joint exponent value.

Eventual schedule admissibility q_n ≤ c_o u_n^γ (γ>0): the selected clip q_n = q_0 n^{-s_feas} stays under c_o u_n^γ = c_o ū^γ n^{-γ t_feas} for all large n, because q_0 ≤ c_o ū^γ (input domain FeasibleRateInputs) and t_feas ≤ s_feas/γ (maximizer feasibility) give the exponent comparison. This is the construction's "Then q_n ≤ c_o u_n^γ for all large n" conclusion, derived from the inputs rather than separately assumed.

thm:welfare-identity. Under the well-formed law (τ = μ₁-μ₀) and bounded outcomes, regret equals the |τ|-weighted disagreement mass. hwf is load-bearing: the integral identity needs τ integrable, and BoundedOutcome bounds only μ₀,μ₁ — the contrast field is bounded (τ ∈ [-2,2]) only once WellFormedLaw ties τ = μ₁-μ₀. Both are global standing setup conditions of the observed law.

The disagreement set is measurable when the policy and contrast are measurable.

The welfare identity controls disagreement on the region with contrast above u.

The margin/large-contrast decomposition used in thm:margin-localization: up to the zero-effect null part, D_π ⊆ {0<|τ|≤u} ∪ (D_π ∩ {|τ|>u}), hence P_X(D_π) ≤ C_m u^α + R_P(π)/u.

thm:margin-localization. Under the margin and zero-effect conditions, disagreement mass is controlled by regret at the fast exponent α/(1+α): P_X(D_π) ≤ C R_P(π)^{α/(1+α)} for every π ∈ policySet.

prop:overlap-envelope. At the tight window v=h^β, u=h^{β/γ}, the envelope value equals h^{(α+1)β/γ}, admissibility ≥ h^α is equivalent to β ≤ αγ/(α+1)=β_{α,γ}, with equality at β=β_{α,γ}. Hence (final conjunct) a block of mass ~h^α with weak-arm exponent β' meets the ass:overlap-decay envelope iff β' ≤ β_{α,γ}, so β_{α,γ} ≥ 0 is the LEAST INFORMATIVE (largest) admissible weak-arm exponent.

A measurable real function that is bounded in absolute value by a single constant is integrable against any finite measure.

Welfare-regret continuity along a pointwise-convergent skeleton sequence: if seq j x = π x eventually for every x, then lawRegret P (seq j) → lawRegret P π. (welfare = ∫ boolIndicator(π x)·τ x dP_X converges by dominated convergence with dominating function |τ| ≤ 2.)

Pooled cross-fit process continuity along a pointwise-convergent skeleton sequence, for a uniformly bounded, policy-compatible, measurable increment g. The finite-sample average n⁻¹ ∑ᵢ g(assign i)(seq j)(sample i) is eventually exactly equal to its π-value (each of the finitely many evaluation points stabilizes), and each centering integral ∫ g(assign i)(seq j) dP converges by dominated convergence (dominating constant B).

Fold-subsample centered process continuity along a pointwise-convergent skeleton sequence (same dominated-convergence content as pooledCrossfitProcess_tendsto_of_skeleton, specialized to a single fold's subsample average). This is the building block for the foldOffsetSubSup integrability conjunct.

Discharges the four Bochner integrability/BddAbove side conditions (hBochner) of the feasible achievability bound: eventually in n, for every law in the class, the selected regret loss is integrable, and the pooled/fold localized offset-process suprema over the policy class are integrable, BddAbove, and (per fold) integrable.

The covariate coordinate of an observation is a measurable function of the observation.

The outcome coordinate of an observation is a measurable function of the observation.

The real treatment indicator of an observation — one when treated, zero when untreated — is a measurable function of the observation.

Clipping a measurable propensity function into the band [q, 1-q] leaves it measurable.

Truncation to the symmetric window [-B, B] acts as the identity on any real number already bounded in absolute value by B.

The truncated cross-fit policy increment is policy-compatible: it depends on the candidate policy only through the single binary treatment decision that policy makes at the observation's covariate.

For a well-formed law, a measurable candidate policy, and measurable fold-k cross-fitted nuisances, the truncated cross-fit policy increment is a measurable function of the observation.

The truncated cross-fit policy increment is bounded in absolute value by the truncation level B, uniformly over candidate policies and observations, for any nonnegative B. So B is a genuine envelope for the whole increment class.

A pointwise product of two uniformly bounded real functions on the covariate space is again uniformly bounded.

The clipped propensity is at least min(q, 1-q), whatever value the underlying propensity takes. No constraint on the clipping level q is needed.

The clipped propensity never exceeds the upper clipping level 1 - q, whatever value the underlying propensity takes.

When the clipping level lies strictly between zero and one, the clipped propensity is strictly positive — this is what keeps the treated arm's inverse-propensity weight finite.

For a strictly positive clipping level, one minus the clipped propensity is strictly positive — this is what keeps the control arm's inverse-propensity weight finite.

The second moment of the truncated cross-fit policy increment under the data law is at most the squared truncation level times the covariate probability of the set where the candidate policy and the law-optimal policy disagree.

Under a well-formed law with bounded outcomes, the conditional treatment-effect contrast is uniformly bounded over the covariate space — the witnessing constant is 2, since the contrast is the difference of two outcome regressions each valued in [-1,1].

lem:clip-bias. Exact clipped-score conditional-mean drift identity E_P[Γ_q(O;η̄)∣X]-τ_P = (ē_q-e_P)(Δ₁/ē_q+Δ₀/(1-ē_q)) = b_q. This is the GENUINE conditional-expectation identity: its first conjunct is stated against the data law P.dataMeasure via the observed-law SEMANTIC conditions packaged in WellFormedLaw P (which pin e_P=P(A=1∣X), μ_a=E[Y∣A=a,X]), so it is NOT a free-standing algebraic identity over the nuisance fields — it ties the dataMeasure-integral of the clipped score to the closed-form drift b_q = clipBias. In tested (conditional-expectation defining) form: for every bounded measurable covariate test function φ, ∫ φ(X) Γ_q dP - ∫ φ τ_P dP_X = ∫ φ b_q dP_X, i.e. E_P[Γ_q∣X] = τ_P + b_q a.s. hbdd (bounded outcomes) is the regularity premise making the score integrals genuine. The second conjunct records the NL CANCELLATION characterization read off b_q: the drift vanishes WHERE the clipped propensity already equals the true propensity (ē_q(x)=e_P(x)) or both regression errors vanish (μ̂_a(x)=μ_a(x)) — so double-robust cancellation does NOT follow merely from p_P(x)>q.

Restricting an i.i.d. product sample to one cross-fitting fold is measure preserving onto the product law over that fold. Delegates to Causalean.Stat.measurePreserving_pi_restrict.

Averaging the fold-k localized supremum over the full-sample product law gives exactly the expected localized supremum for an i.i.d. sample whose size is the number of observations in that fold.

Averaging the fold-k offset supremum over the full-sample product law gives exactly the expected offset supremum of the centered empirical process for an i.i.d. sample whose size is the number of observations in that fold — the offset counterpart of the localized fold reduction.

The cross-fitting fold weights — each fold's size divided by the total sample size — sum to one. So the pooled cross-fit process is a genuine convex combination of the foldwise processes.

Averaging any fold-indexed quantity across the observations of the sample is the same as taking its fold-weighted average, with each fold weighted by its size relative to the sample size.

No cross-fitting fold contains more observations than the whole sample.

A fold's weight times its own root-m rate is at most the full-sample root-n rate: (m/n)·m^{-1/2} ≤ n^{-1/2} whenever 0 < m ≤ n.

The pooling step for the offset rate: (m/n)·(B²/m)^A ≤ (B²/n)^A whenever 0 < m ≤ n and the exponent A is at most one.

The logarithmic factor is monotone in the sample size: (log m)^p ≤ (log n)^p for a nonnegative power p and 1 ≤ m ≤ n. So replacing a fold's size by the full sample size in a (log ·)^p factor only weakens the bound.

The law-optimal policy — treat exactly where the contrast is nonnegative — is a measurable policy whenever the law is well formed, since well-formedness makes the contrast measurable.

Welfare regret is nonnegative for every measurable policy, under a well-formed law with bounded outcomes. By the welfare identity it is the integral of the absolute contrast against the disagreement indicator, and both factors are nonnegative.

Sample by sample, the localized supremum of the pooled cross-fit process is at most the fold-weighted sum of the foldwise localized suprema.

Sample by sample, the offset supremum of the pooled cross-fit process is at most the fold-weighted sum of the foldwise offset suprema.

lem:clipped-region-localization. For γ>0, the disagreement mass inside the clipped region is controlled: P_X(D_π ∩ {p_P≤q}) ≤ C u^α q^{1/γ}+r/u.

Cauchy–Schwarz in the shape used to form product rates: if two square-integrable functions have mean squares bounded by r_f^2 and r_g^2, then the integral of the product of their absolute values is at most r_f r_g. This is the step that turns two separate root-mean-square nuisance rates into a single product rate.

Cauchy-Schwarz against an indicator. Under a probability measure, the integral of a function's absolute value over a measurable set is at most the square root of that set's probability times the function's root-mean-square bound. This is what converts an integral localized to a small region into a mass factor multiplied by a rate.

Truncating a real number into the band between q and 1-q never pushes two inputs further apart than they already were: the operation is nonexpansive.

Pointwise error of the clipped propensity. For a clip level between zero and one half, the distance between the clipped estimated propensity and the true propensity is at most the raw estimation error plus the clip level itself, and that extra charge is incurred only at covariate values whose true overlap is at or below the clip level. Away from the clipped region, clipping costs nothing.

The disagreement weight between two policies, restricted to a set, is dominated by the indicator of the intersection. The absolute difference of the two policies' treatment indicators is at most one and is zero wherever the policies agree, so multiplying it by the indicator of any set is bounded by the indicator of that set intersected with the region where the policies disagree.

Pointwise bound on the disagreement-weighted clipped-AIPW bias. At each covariate value, the product of the policy-disagreement weight and the clip bias is at most the propensity error times each of the two outcome-regression errors, divided by the clip level, plus each outcome-regression error restricted to the part of the disagreement region whose overlap is at or below the clip level. The first group is the familiar product-bias term; the second is the price of clipping, and it is charged only inside the clipped region.

Integrated clip-bias drift bound in terms of the clipped-region mass. If the two outcome-regression errors have root-mean-square bound r_μ and the propensity error has root-mean-square bound r_e, then the policy-weighted population drift is at most twice the product rate divided by the clip level, plus twice r_μ times the square root of the probability that a covariate both lies in the disagreement region and has overlap at or below the clip level. Only that mass enters; bounding it is left to the localization step.

The square root is subadditive: the square root of a sum of two nonnegative numbers is at most the sum of their square roots.

Taking the square root of the localized-mass bound distributes across its three positive factors and halves each exponent: the square root of a constant times the margin window raised to α times the clip level raised to 1/γ equals the square root of the constant times the window raised to α/2 times the clip level raised to 1/(2γ).

Drift bound from a supplied localization estimate. Given as an input a bound on the mass of the clipped disagreement region of the form C u^α q^{1/γ} + R_P(π)/u, the policy-weighted clip-bias drift is at most 4 times the sum of the product-rate term r_μ r_e / q, the clipped-region term r_μ C^{1/2} u^{α/2} q^{1/(2γ)} and the regret-localization term r_μ (R_P(π)/u)^{1/2}. At the strict-overlap endpoint, where the overlap exponent is zero and the clip level is fixed at no more than half the overlap floor, the drift instead collapses to max(1, 2/q) times the product rate r_μ r_e. This is the form that takes the localization estimate as a hypothesis; the companion result derives that estimate itself from overlap decay and zero-effect regularity.

Deterministic bound on the policy-weighted clip-bias drift — the population average of the clipped-AIPW conditional-mean error weighted by the disagreement between the candidate policy and the law-optimal policy — in BOTH overlap regimes.

lem:feasible-erm-basic-inequality. The feasible ERM (enum-skeleton, foldwise cross-fit) is a MEASURABLE Π-valued estimator: it is Π-valued for every realized sample, the induced regret map sample ↦ R_P(π̂_n(sample)) is measurable (so the U_n/M_n integrals are well-defined), and against EVERY comparator π^b ∈ Π the 1/n basic inequality holds; under OptimalInClass it applies in particular to π^b = π_⋆. The comparator inequality over ALL of Π is load-bearing on enum being a POINTWISE-DENSE skeleton of Π (the countable Π₀ of ass:policy-class that def:feasible-erm fixes): hdense says every π ∈ Π is a pointwise limit of enum-indexed policies, which is what reduces sup_Π V̂ to sup_j V̂(enum j). Without it the bare henum : enum j ∈ Π would not license the Π-wide near-maximality.