Stat.Coupling.Atomic­Spectral­Law

This roll-up module provides model-independent bounds that transfer a collision-safe diagonalizable functional calculus estimate to finite atomic one-Wasserstein laws represented by anchored operator evaluations.

Basic 2 core · 0 supporting This module composes the two-diagonalizer functional-calculus estimate with attained finite-atomic Kantorovich--Rubinstein duality. ★ atomicW1_le_operator_anchor_perturbation

Collision-safe operator-to-law composition

This module composes the two-diagonalizer functional-calculus estimate with attained finite-atomic Kantorovich--Rubinstein duality. Its public theorem is entirely model-independent: a consumer only supplies valid (nonnegative, unit-mass) atomic laws whose Lipschitz tests are represented by left-right functional-calculus evaluations.

def RepresentsAtomicLaw reviewed
Causalean.Stat.Coupling.AtomicSpectralLaw

A finite atomic law is represented by a diagonalized real square matrix together with a left and a right anchor vector when, for every one-Lipschitz real test function vanishing at zero, the law's weighted expectation of the test function equals the inner product of the left anchor with the image of the right anchor under the matrix function obtained by applying the test function to the eigenvalues of the diagonalization.

Definition (Lean source)
parameters
ι :
Type*
Fintype ι
n :
ℕ
RectMatrix n n
D :
RealDiagonalization A
a c :
Euc n
μ :
AtomicLaw ι
f :
ℝ → ℝ
LipschitzWith 1 f
f 0 = 0
def
RepresentsAtomicLaw D a c μ :
Prop
given by
μ.integral f = anchorEval a c (D.applyFunction f)
Causalean.Stat.Coupling.AtomicSpectralLaw.RepresentsAtomicLaw · Causalean/Stat/Coupling/AtomicSpectralLaw/Basic.lean:21 · uses Euc , RealDiagonalization , RectMatrix , AtomicLaw
theorem atomicW1_le_operator_anchor_perturbation reviewed
Causalean.Stat.Coupling.AtomicSpectralLaw

Finite slot types, a matrix dimension and two real matrices, their real diagonalizations, left and right anchor vectors, finite atomic laws with valid probability weights, their anchored functional-calculus representations, condition-number bounds, and a nonnegative common spectral envelope give a collision-safe one-Wasserstein bound controlled only by operator and anchor perturbations: the one-Wasserstein distance between the two laws is at most ‖a − b‖·κA·R·‖c‖ + ‖b‖·n²·κA·κB·‖A − B‖·‖c‖ + ‖b‖·κB·R·‖c − d‖.

Formal statement
hypotheses
ι κ :
Type*
Fintype ι
Fintype κ
n :
ℕ
RectMatrix n n
DA :
RealDiagonalization A
DB :
RealDiagonalization B
a b c d :
Euc n
μ :
AtomicLaw ι
ν :
AtomicLaw κ
hμ :
μ.Valid
hν :
ν.Valid
hrepA :
RepresentsAtomicLaw DA a c μ
hrepB :
RepresentsAtomicLaw DB b d ν
κA κB R :
ℝ
hκA :
DA.conditionNumber ≤ κA
hκB :
DB.conditionNumber ≤ κB
hR0 :
0 ≤ R
hRA :
DA.SpectrumBound R
hRB :
DB.SpectrumBound R
conclusion
AtomicLaw.w1 μ ν
≤ ‖a - b‖ * (κA * R) * ‖c‖
+ ‖b‖ * ((n : ℝ) ^ 2 * κA * κB * ‖A - B‖) * ‖c‖
+ ‖b‖ * (κB * R) * ‖c - d‖
Proof (Lean source)
theorem atomicW1_le_operator_anchor_perturbation {ι κ : Type*} [Fintype ι] [Fintype κ] {n : ℕ} {A B : RectMatrix n n} (DA : RealDiagonalization A) (DB : RealDiagonalization B) (a b c d : Euc n) (μ : AtomicLaw ι) (ν : AtomicLaw κ) (hμ : μ.Valid) (hν : ν.Valid) (hrepA : RepresentsAtomicLaw DA a c μ) (hrepB : RepresentsAtomicLaw DB b d ν) {κA κB R : ℝ} (hκA : DA.conditionNumber ≤ κA) (hκB : DB.conditionNumber ≤ κB) (hR0 : 0 ≤ R) (hRA : DA.SpectrumBound R) (hRB : DB.SpectrumBound R) : AtomicLaw.w1 μ ν ≤ ‖a - b‖ * (κA * R) * ‖c‖ + ‖b‖ * ((n : ℝ) ^ 2 * κA * κB * ‖A - B‖) * ‖c‖ + ‖b‖ * (κB * R) * ‖c - d‖ := by /- Use the attained `krPotential`, which is already one-Lipschitz and normalized at zero. Rewrite both expectations with `hrepA` and `hrepB`, then apply `abs_anchorEval_applyFunction_sub_le`; the attainment equality avoids having to normalize an arbitrary dual test function. -/ obtain ⟨hf, hatt⟩ := AtomicLaw.krPotential_attains μ ν hμ hν rw [hatt, hrepA _ hf (AtomicLaw.krPotential_zero μ ν), hrepB _ hf (AtomicLaw.krPotential_zero μ ν)] exact abs_anchorEval_applyFunction_sub_le DA DB a b c d _ hf (AtomicLaw.krPotential_zero μ ν) hκA hκB hR0 hRA hRB
Causalean.Stat.Coupling.AtomicSpectralLaw.atomicW1_le_operator_anchor_perturbation · Causalean/Stat/Coupling/AtomicSpectralLaw/Basic.lean:31 · uses Euc , RealDiagonalization , SpectrumBound , conditionNumber , RectMatrix , AtomicLaw , Valid , w1 , RepresentsAtomicLaw
Sharp 1 core · 0 supporting Two finite atomic probability laws on the real line are each represented through a real diagonalizable n × n matrix and a pair of anchor vectors, in the sense that the expectation of every 1-Lipschitz test function vanis ★ atomicW1_le_operator_anchor_perturbation_sqrt_dim

One-Wasserstein stability of spectrally represented atomic laws, with a √n dimension factor

Two finite atomic probability laws on the real line are each represented through a real diagonalizable n × n matrix and a pair of anchor vectors, in the sense that the expectation of every 1-Lipschitz test function vanishing at zero equals the anchored evaluation of that function of the matrix. Their one-Wasserstein distance is then bounded by the perturbations of the anchors and of the matrices, with no eigenvalue-gap assumption:

W₁(μ, ν) ≤ ‖a − b‖ κA R ‖c‖ + ‖b‖ √n κA κB ‖A − B‖ ‖c‖ + ‖b‖ κB R ‖c − d‖,

where κA, κB bound the condition numbers of the two diagonalizations and R bounds the absolute values of all their eigenvalues.

Main result

* atomicW1_le_operator_anchor_perturbation_sqrt_dim — the bound above. It sharpens the factor n² of atomicW1_le_operator_anchor_perturbation to √n; optimality of √n is not proved.

theorem atomicW1_le_operator_anchor_perturbation_sqrt_dim reviewed
Causalean.Stat.Coupling.AtomicSpectralLaw

Finite slot types, a matrix dimension and two real matrices, their real diagonalizations, left and right anchor vectors, finite atomic laws with valid probability weights, their anchored functional-calculus representations, condition-number bounds, and a nonnegative common spectral envelope give the square-root-dimensional collision-safe one-Wasserstein bound: the one-Wasserstein distance between the two laws is at most ‖a − b‖·κA·R·‖c‖ + ‖b‖·√n·κA·κB·‖A − B‖·‖c‖ + ‖b‖·κB·R·‖c − d‖.

Formal statement
hypotheses
ι κ :
Type*
Fintype ι
Fintype κ
n :
ℕ
RectMatrix n n
DA :
RealDiagonalization A
DB :
RealDiagonalization B
a b c d :
Euc n
μ :
AtomicLaw ι
ν :
AtomicLaw κ
hμ :
μ.Valid
hν :
ν.Valid
hrepA :
RepresentsAtomicLaw DA a c μ
hrepB :
RepresentsAtomicLaw DB b d ν
κA κB R :
ℝ
hκA :
DA.conditionNumber ≤ κA
hκB :
DB.conditionNumber ≤ κB
hR0 :
0 ≤ R
hRA :
DA.SpectrumBound R
hRB :
DB.SpectrumBound R
conclusion
AtomicLaw.w1 μ ν
≤ ‖a - b‖ * (κA * R) * ‖c‖
+ ‖b‖ * (sqrt n * κA * κB * ‖A - B‖) * ‖c‖
+ ‖b‖ * (κB * R) * ‖c - d‖
Proof (Lean source)
theorem atomicW1_le_operator_anchor_perturbation_sqrt_dim {ι κ : Type*} [Fintype ι] [Fintype κ] {n : ℕ} {A B : RectMatrix n n} (DA : RealDiagonalization A) (DB : RealDiagonalization B) (a b c d : Euc n) (μ : AtomicLaw ι) (ν : AtomicLaw κ) (hμ : μ.Valid) (hν : ν.Valid) (hrepA : RepresentsAtomicLaw DA a c μ) (hrepB : RepresentsAtomicLaw DB b d ν) {κA κB R : ℝ} (hκA : DA.conditionNumber ≤ κA) (hκB : DB.conditionNumber ≤ κB) (hR0 : 0 ≤ R) (hRA : DA.SpectrumBound R) (hRB : DB.SpectrumBound R) : AtomicLaw.w1 μ ν ≤ ‖a - b‖ * (κA * R) * ‖c‖ + ‖b‖ * (sqrt n * κA * κB * ‖A - B‖) * ‖c‖ + ‖b‖ * (κB * R) * ‖c - d‖ := by obtain ⟨hf, hatt⟩ := AtomicLaw.krPotential_attains μ ν hμ hν rw [hatt, hrepA _ hf (AtomicLaw.krPotential_zero μ ν), hrepB _ hf (AtomicLaw.krPotential_zero μ ν)] exact abs_anchorEval_applyFunction_sub_le_sqrt_dim DA DB a b c d _ hf (AtomicLaw.krPotential_zero μ ν) hκA hκB hR0 hRA hRB
Causalean.Stat.Coupling.AtomicSpectralLaw.atomicW1_le_operator_anchor_perturbation_sqrt_dim · Causalean/Stat/Coupling/AtomicSpectralLaw/Sharp.lean:32 · uses Euc , RealDiagonalization , SpectrumBound , conditionNumber , RectMatrix , AtomicLaw , Valid , w1 , RepresentsAtomicLaw