[Swag-Pseudopy]

Part of #72.

This adds Statlib/Invariance/Lindeberg/Basic.lean, a formalization of Chatterjee's version of the Lindeberg swap (S. Chatterjee, A simple invariance theorem, arXiv:math/0508213, Theorem 1.1).

Statement. Statlib.Invariance.swap_bound: if X = (X_1, ..., X_n) and Y = (Y_1, ..., Y_n) have jointly independent coordinates with matching first and second moments, then for a test function g and a function f that is smooth in each coordinate,

|E g(f(X)) - E g(f(Y))| <= C_1(g) lam_2(f) sum_i (E(X_i^2; |X_i| > K) + E(Y_i^2; |Y_i| > K)) + C_2(g) lam_3(f) sum_i (E(|X_i|^3; |X_i| <= K) + E(|Y_i|^3; |Y_i| <= K)),

with lam_r the coordinatewise derivative scale from the paper and C_1, C_2 the constants from the paper.

Proof structure. Hybrids Z_k = (X_1..X_k, Y_{k+1}..Y_n) and a telescoping sum. In slot k the function is expanded to second order around the same base point for X_k and Y_k. Independence and matched moments cancel the first two terms (slot_expansion, slot_swap), and the remainder is bounded pointwise (remainder_slice_le). The file header has the full outline.

Hypotheses that differ from the paper. The paper does not discuss these, so I made them explicit:

• g is bounded, besides having bounded derivatives up to order 3.
• f and its first two coordinate derivatives are measurable.
• the 2n variables are jointly independent: iIndepFun (Sum.elim X Y) P.
• f is only assumed C^3 along each coordinate line (CoordC3), not jointly.

Status. lake build Statlib.Invariance.Lindeberg.Basic passes locally with no sorry. This is a draft because:

• the file still has public import Mathlib, which I will narrow to the modules actually used,
• the hypotheses and the lam : ENNReal design are open on [Design] Lindeberg swap proof for CLT #72.