Algorithmic stability and generalization

Formalizes the uniform stability framework of Bousquet-Elisseeff (2002). An algorithm A : (Fin n → Z) → ι has uniform stability β if replacing any single training point changes the loss of the selected hypothesis on any test point by at most β.

What is proved (all closed, no sorry)

• UniformStability A ℓ β: the stability predicate.
• trainingLoss_hasBoundedDifferences: stability + bounded loss imply bounded differences with constant β + 2B/n for the training loss. This can be fed to bounded-differences concentration tails.
• stability_genGap_hasBoundedDifferences: the generalization gap R(A(S)) - trainingLoss(A,S) has bounded differences with constant 2β + 2B/n. It feeds into the sharp McDiarmid stability wrappers.
• expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap : finite expected-gap adapter: under finite sample weights and a finite coordinate-swap identity, uniform stability gives expected gap ≤ β.
• expectedFiniteStabilityGap_le_uniformStability_finiteProduct : finite iid product-weight specialization: the coordinate-swap identity is proved by an explicit finite reindexing argument.
• abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct : finite iid two-sided expected generalization-gap bound: |E_S[R(A(S)) - Rhat_S(A(S))]| ≤ β.
• abs_expectedStabilityGap_le_uniformStability_piMeasure : measure-theoretic iid two-sided expected generalization-gap bound over Measure.pi, with explicit integrability assumptions on the selected losses induced by the algorithm.
• abs_expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss : finite-class bounded-loss adapter that discharges those integrability assumptions from measurability of A and the per-hypothesis losses.

Uniform stability predicate

def FormalSLT.AlgorithmicStability.UniformStability {ι : Type u_1} {Z : Type u_2} {n : ℕ} (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) (β : ℝ) : Prop

An algorithm A has uniform stability β if replacing any single training example changes the selected hypothesis's loss on any test point by at most β in absolute value.

Equations

• FormalSLT.AlgorithmicStability.UniformStability A ℓ β = ∀ (S : Fin n → Z) (k : Fin n) (z' z : Z), |ℓ (A S) z - ℓ (A (Function.update S k z')) z| ≤ β

theorem FormalSLT.AlgorithmicStability.uniformStability_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) : UniformStability A (fun (i : ι) (z : Z) => -ℓ i z) β

Negating the loss preserves uniform stability with the same β.

Training loss

noncomputable def FormalSLT.AlgorithmicStability.trainingLoss {ι : Type u_1} {Z : Type u_2} {n : ℕ} (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) (S : Fin n → Z) : ℝ

Training loss: empirical risk of the algorithm-selected hypothesis on the training data. trainingLoss A ℓ S = (1/n) ∑_k ℓ(A(S), S(k))

Equations

• FormalSLT.AlgorithmicStability.trainingLoss A ℓ S = (↑n)⁻¹ * ∑ k : Fin n, ℓ (A S) (S k)

Measure-theoretic coordinate swap

def FormalSLT.AlgorithmicStability.sampleCoordinateSwap {Z : Type u_2} {n : ℕ} (k : Fin n) : (Fin n → Z) × Z → (Fin n → Z) × Z

Swap sample coordinate k with an auxiliary fresh draw.

This is the measure-theoretic analogue of finiteCoordinateSwapEquiv: a pair (S, z) is sent to (Function.update S k z, S k). Under the iid product measure μⁿ × μ, this map preserves measure.

Equations

• FormalSLT.AlgorithmicStability.sampleCoordinateSwap k P = (Function.update P.1 k P.2, P.1 k)

theorem FormalSLT.AlgorithmicStability.sampleCoordinateSwap_involutive {Z : Type u_2} {n : ℕ} (k : Fin n) : Function.Involutive (sampleCoordinateSwap k)

The sample-coordinate swap is its own inverse.

theorem FormalSLT.AlgorithmicStability.measurable_sampleCoordinateSwap {Z : Type u_2} [MeasurableSpace Z] {n : ℕ} (k : Fin n) : Measurable (sampleCoordinateSwap k)

Measurability of the sample-coordinate swap.

def FormalSLT.AlgorithmicStability.sampleCoordinateSwapEquiv {Z : Type u_2} [MeasurableSpace Z] {n : ℕ} (k : Fin n) : (Fin n → Z) × Z ≃ᵐ (Fin n → Z) × Z

The sample-coordinate swap as a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.AlgorithmicStability.measurePreserving_sampleCoordinateSwap {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.SigmaFinite μ] {n : ℕ} (k : Fin n) : MeasureTheory.MeasurePreserving (sampleCoordinateSwap k) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)

The sample-coordinate swap preserves the iid product measure μⁿ × μ.

Equivalently, replacing the kth coordinate by a fresh draw and carrying the old coordinate as the auxiliary draw is just a finite coordinate permutation of the product index set Option (Fin n).

theorem FormalSLT.AlgorithmicStability.integral_sampleCoordinateSwap {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.SigmaFinite μ] {n : ℕ} (k : Fin n) (G : (Fin n → Z) × Z → ℝ) : ∫ (P : (Fin n → Z) × Z), G (sampleCoordinateSwap k P) ∂(MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ = ∫ (P : (Fin n → Z) × Z), G P ∂(MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ

Integral invariance under the sample-coordinate swap.

theorem FormalSLT.AlgorithmicStability.integral_update_eq_integral_coordinate {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.SigmaFinite μ] {n : ℕ} (k : Fin n) (G : (Fin n → Z) → Z → ℝ) : ∫ (P : (Fin n → Z) × Z), G (Function.update P.1 k P.2) P.2 ∂(MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ = ∫ (P : (Fin n → Z) × Z), G P.1 (P.1 k) ∂(MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ

Coordinate-swap integral identity in the update notation used by stability.

This is the measure-theoretic replacement for the finite sum reindexing used by finiteProductSampleWeight_coordinateSwapIdentity.

theorem FormalSLT.AlgorithmicStability.expectedStabilityGap_le_uniformStability_piMeasure {ι : Type u_1} {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (h_loss_int : MeasureTheory.Integrable (fun (P : (Fin n → Z) × Z) => ℓ (A P.1) P.2) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)) (h_update_int : ∀ (k : Fin n), MeasureTheory.Integrable (fun (P : (Fin n → Z) × Z) => ℓ (A (Function.update P.1 k P.2)) P.2) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)) (h_coord_int : ∀ (k : Fin n), MeasureTheory.Integrable (fun (S : Fin n → Z) => ℓ (A S) (S k)) (MeasureTheory.Measure.pi fun (x : Fin n) => μ)) : (∫ (S : Fin n → Z), Risk.risk μ ℓ (A S) - trainingLoss A ℓ S ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ) ≤ β

Measure-theoretic iid expected uniform-stability bound.

This is the iid product-measure lift of the finite coordinate-swap expected gap argument. It is deliberately scoped to a finite sample Fin n, scalar real-valued losses, an arbitrary data space with probability law μ, and explicit integrability hypotheses for the selected-loss functions induced by the learning algorithm A.

The proof is the Bousquet-Elisseeff coordinate-swap argument: Fubini rewrites selected population risk as an integral over μⁿ × μ, uniform stability compares it to the coordinate-replaced sample, and integral_update_eq_integral_coordinate swaps the fresh draw back into the training coordinate.

Stability implies bounded differences

theorem FormalSLT.AlgorithmicStability.trainingLoss_hasBoundedDifferences {ι : Type u_1} {Z : Type u_2} {n : ℕ} (hn : 0 < n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β B : ℝ} (hstab : UniformStability A ℓ β) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) : Azuma.BoundedDifferences.HasBoundedDifferences (trainingLoss A ℓ) fun (x : Fin n) => β + 2 * B / ↑n

Stability + bounded loss ⟹ bounded differences for training loss. The width is β + 2B/n: stability contributes β (all terms shift), and the evaluation-point change at coordinate k contributes 2B/n.

Generalization gap bounded differences

theorem FormalSLT.AlgorithmicStability.stability_genGap_hasBoundedDifferences {ι : Type u_1} {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β B : ℝ} (hstab : UniformStability A ℓ β) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) (hℓ_int : ∀ (i : ι), MeasureTheory.Integrable (ℓ i) μ) : Azuma.BoundedDifferences.HasBoundedDifferences (fun (S : Fin n → Z) => ∫ (z : Z), ℓ (A S) z ∂μ - trainingLoss A ℓ S) fun (x : Fin n) => 2 * β + 2 * B / ↑n

The generalization gap R(A(S)) - trainingLoss(A,S) has bounded differences with constant 2β + 2B/n. The risk integral changes by at most β (integrate the pointwise stability bound), and the training loss changes by at most β + 2B/n.

Finite expected stability adapter

noncomputable def FormalSLT.AlgorithmicStability.finitePopulationRisk {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (ℓ : ι → Z → ℝ) (i : ι) : ℝ

Finite population risk under an explicit finite probability mass function.

This is a finite-domain adapter for the expected-stability theorem below. It does not replace the measure-theoretic risk; it makes the coordinate-swap bookkeeping explicit while the full product-measure kernel decomposition is developed separately.

Equations

• FormalSLT.AlgorithmicStability.finitePopulationRisk p ℓ i = ∑ z : Z, p z * ℓ i z

noncomputable def FormalSLT.AlgorithmicStability.finiteSampleExpectation {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight F : (Fin n → Z) → ℝ) : ℝ

Finite expectation over samples with explicit sample weights.

Equations

• FormalSLT.AlgorithmicStability.finiteSampleExpectation sampleWeight F = ∑ S : Fin n → Z, sampleWeight S * F S

noncomputable def FormalSLT.AlgorithmicStability.expectedFiniteSelectedRisk {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : ℝ

Expected risk of the hypothesis selected by A under finite sample weights and a finite data distribution.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.AlgorithmicStability.expectedFiniteTrainingLoss {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : ℝ

Expected empirical training loss of the hypothesis selected by A under finite sample weights.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.AlgorithmicStability.expectedFiniteStabilityGap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : ℝ

Expected finite generalization gap for an algorithm-selected hypothesis.

This is E_S[R(A(S))] - E_S[Rhat(A(S), S)] with all expectations expanded as finite weighted sums.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.AlgorithmicStability.finiteStabilityGeneralizationGap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) (S : Fin n → Z) : ℝ

Pointwise finite generalization gap for an algorithm-selected hypothesis.

For a realized sample S, this is R(A(S)) - Rhat_S(A(S)) with both risks expanded as finite sums.

Equations

• FormalSLT.AlgorithmicStability.finiteStabilityGeneralizationGap p A ℓ S = FormalSLT.AlgorithmicStability.finitePopulationRisk p ℓ (A S) - FormalSLT.AlgorithmicStability.trainingLoss A ℓ S

noncomputable def FormalSLT.AlgorithmicStability.expectedFiniteGeneralizationGap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : ℝ

Finite expectation of the pointwise algorithmic-stability generalization gap.

This is the literal finite E_S[R(A(S)) - Rhat_S(A(S))] form.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.AlgorithmicStability.expectedFiniteGeneralizationGap_eq_expectedFiniteStabilityGap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : expectedFiniteGeneralizationGap sampleWeight p A ℓ = expectedFiniteStabilityGap sampleWeight p A ℓ

The pointwise-gap expectation agrees with selected risk minus expected training loss in the finite setting.

theorem FormalSLT.AlgorithmicStability.finitePopulationRisk_neg {ι : Type u_1} {Z : Type u_2} [Fintype Z] (p : Z → ℝ) (ℓ : ι → Z → ℝ) (i : ι) : finitePopulationRisk p (fun (i : ι) (z : Z) => -ℓ i z) i = -finitePopulationRisk p ℓ i

Finite population risk changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.trainingLoss_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) (S : Fin n → Z) : trainingLoss A (fun (i : ι) (z : Z) => -ℓ i z) S = -trainingLoss A ℓ S

Training loss changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.risk_neg {ι : Type u_1} {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) (ℓ : ι → Z → ℝ) (i : ι) : Risk.risk μ (fun (i : ι) (z : Z) => -ℓ i z) i = -Risk.risk μ ℓ i

Population risk changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.abs_expectedStabilityGap_le_uniformStability_piMeasure {ι : Type u_1} {Z : Type u_2} [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (h_loss_int : MeasureTheory.Integrable (fun (P : (Fin n → Z) × Z) => ℓ (A P.1) P.2) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)) (h_update_int : ∀ (k : Fin n), MeasureTheory.Integrable (fun (P : (Fin n → Z) × Z) => ℓ (A (Function.update P.1 k P.2)) P.2) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)) (h_coord_int : ∀ (k : Fin n), MeasureTheory.Integrable (fun (S : Fin n → Z) => ℓ (A S) (S k)) (MeasureTheory.Measure.pi fun (x : Fin n) => μ)) : |∫ (S : Fin n → Z), Risk.risk μ ℓ (A S) - trainingLoss A ℓ S ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ| ≤ β

Measure-theoretic iid two-sided expected uniform-stability bound.

This is the absolute-value wrapper around expectedStabilityGap_le_uniformStability_piMeasure, obtained by applying the one-sided theorem to the negated loss. It bounds the absolute value of the expected gap, not the expectation of the pointwise absolute gap.

theorem FormalSLT.AlgorithmicStability.finiteClass_loss_measurable {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace Z] (ℓ : ι → Z → ℝ) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) : Measurable fun (P : ι × Z) => ℓ P.1 P.2

A finite hypothesis-indexed scalar loss is jointly measurable when each hypothesis loss is measurable and the finite index type has measurable singletons.

This is a finite-class measurability adapter. It is not a measurability theorem for arbitrary hypothesis spaces or arbitrary stochastic kernels.

theorem FormalSLT.AlgorithmicStability.boundedLoss_selectedLoss_integrable {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {B : ℝ} (hA : Measurable A) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) : MeasureTheory.Integrable (fun (P : (Fin n → Z) × Z) => ℓ (A P.1) P.2) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)

Integrability of the algorithm-selected loss under μⁿ × μ, from finite hypothesis class measurability and a uniform bounded-loss assumption.

This adapter is for finite-sample, finite-class, scalar-valued stability theorems. It does not remove the need to prove the learning algorithm A : (Fin n → Z) → ι is measurable.

theorem FormalSLT.AlgorithmicStability.boundedLoss_updateSelectedLoss_integrable {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (k : Fin n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {B : ℝ} (hA : Measurable A) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) : MeasureTheory.Integrable (fun (P : (Fin n → Z) × Z) => ℓ (A (Function.update P.1 k P.2)) P.2) ((MeasureTheory.Measure.pi fun (x : Fin n) => μ).prod μ)

Integrability of the coordinate-updated selected loss under μⁿ × μ.

This is the bounded-loss adapter for the fresh-sample term ℓ (A (Function.update S k z')) z' used by the measure-theoretic stability coordinate-swap proof.

theorem FormalSLT.AlgorithmicStability.boundedLoss_coordinateSelectedLoss_integrable {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (k : Fin n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {B : ℝ} (hA : Measurable A) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) : MeasureTheory.Integrable (fun (S : Fin n → Z) => ℓ (A S) (S k)) (MeasureTheory.Measure.pi fun (x : Fin n) => μ)

Integrability of each empirical coordinate loss under μⁿ.

This is the bounded-loss adapter for the terms S ↦ ℓ (A S) (S k) in the training-loss integral.

theorem FormalSLT.AlgorithmicStability.expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β B : ℝ} (hstab : UniformStability A ℓ β) (hA : Measurable A) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) : (∫ (S : Fin n → Z), Risk.risk μ ℓ (A S) - trainingLoss A ℓ S ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ) ≤ β

Measure-theoretic iid expected uniform-stability bound with bounded-loss integrability discharged automatically.

This is the finite-class bounded-loss wrapper around expectedStabilityGap_le_uniformStability_piMeasure. It assumes a finite hypothesis index type, measurable algorithm A, measurable scalar losses ℓ i, and a uniform pointwise bound |ℓ i z| ≤ B; it is not an infinite-class or kernel-measurability theorem.

theorem FormalSLT.AlgorithmicStability.abs_expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss {ι : Type u_1} {Z : Type u_2} [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] [MeasurableSpace Z] (μ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β B : ℝ} (hstab : UniformStability A ℓ β) (hA : Measurable A) (hℓ_meas : ∀ (i : ι), Measurable (ℓ i)) (hℓ_bdd : ∀ (i : ι) (z : Z), |ℓ i z| ≤ B) : |∫ (S : Fin n → Z), Risk.risk μ ℓ (A S) - trainingLoss A ℓ S ∂MeasureTheory.Measure.pi fun (x : Fin n) => μ| ≤ β

Two-sided measure-theoretic iid expected uniform-stability bound with bounded-loss integrability discharged automatically.

This bounds the absolute value of the expected generalization gap for a finite hypothesis class and measurable bounded scalar losses. It is not a high-probability stability theorem and does not cover arbitrary infinite hypothesis spaces.

theorem FormalSLT.AlgorithmicStability.expectedFiniteSelectedRisk_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : (expectedFiniteSelectedRisk sampleWeight p A fun (i : ι) (z : Z) => -ℓ i z) = -expectedFiniteSelectedRisk sampleWeight p A ℓ

Expected selected finite risk changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.expectedFiniteTrainingLoss_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : (expectedFiniteTrainingLoss sampleWeight A fun (i : ι) (z : Z) => -ℓ i z) = -expectedFiniteTrainingLoss sampleWeight A ℓ

Expected finite training loss changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.expectedFiniteStabilityGap_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : (expectedFiniteStabilityGap sampleWeight p A fun (i : ι) (z : Z) => -ℓ i z) = -expectedFiniteStabilityGap sampleWeight p A ℓ

Expected finite stability gap changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.finiteStabilityGeneralizationGap_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) (S : Fin n → Z) : finiteStabilityGeneralizationGap p A (fun (i : ι) (z : Z) => -ℓ i z) S = -finiteStabilityGeneralizationGap p A ℓ S

Pointwise finite stability generalization gap changes sign when the loss is negated.

theorem FormalSLT.AlgorithmicStability.expectedFiniteGeneralizationGap_neg {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) (A : (Fin n → Z) → ι) (ℓ : ι → Z → ℝ) : (expectedFiniteGeneralizationGap sampleWeight p A fun (i : ι) (z : Z) => -ℓ i z) = -expectedFiniteGeneralizationGap sampleWeight p A ℓ

Expected finite pointwise generalization gap changes sign when the loss is negated.

def FormalSLT.AlgorithmicStability.FiniteCoordinateSwapIdentity {Z : Type u_2} {n : ℕ} [Fintype Z] (sampleWeight : (Fin n → Z) → ℝ) (p : Z → ℝ) : Prop

Finite coordinate-swap identity for replacing coordinate k with an independent draw from p.

For iid product weights this is the finite-sum analogue of the product-measure coordinate-swap symmetry. It is kept as an explicit hypothesis here so the expected-stability proof can be closed without hiding the product-kernel infrastructure still needed for the measure-theoretic theorem.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FormalSLT.AlgorithmicStability.finiteProductSampleWeight {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (S : Fin n → Z) : ℝ

Finite iid product sample weight induced by a finite data mass function.

For a sample S : Fin n → Z, this is ∏ k, p (S k). The definition is purely finite and is used to close the coordinate-swap symmetry needed by the finite expected-stability adapter.

Equations

• FormalSLT.AlgorithmicStability.finiteProductSampleWeight p S = ∏ k : Fin n, p (S k)

theorem FormalSLT.AlgorithmicStability.finiteProductSampleWeight_nonneg {Z : Type u_2} {n : ℕ} [Fintype Z] {p : Z → ℝ} (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (S : Fin n → Z) : 0 ≤ finiteProductSampleWeight p S

Finite iid product sample weights are nonnegative when the base mass function is nonnegative.

theorem FormalSLT.AlgorithmicStability.finiteProductSampleWeight_sum_eq_one {Z : Type u_2} {n : ℕ} [Fintype Z] {p : Z → ℝ} (hp_sum : ∑ z : Z, p z = 1) : ∑ S : Fin n → Z, finiteProductSampleWeight p S = 1

Finite iid product sample weights sum to one when the base mass function sums to one.

theorem FormalSLT.AlgorithmicStability.finiteProductSampleWeight_update_mul {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (S : Fin n → Z) (k : Fin n) (z : Z) : finiteProductSampleWeight p (Function.update S k z) * p (S k) = finiteProductSampleWeight p S * p z

Replacing coordinate k in a finite iid product weight and multiplying by the old coordinate mass equals the original weight times the replacement mass.

This is the algebraic core of the finite coordinate-swap proof.

def FormalSLT.AlgorithmicStability.finiteCoordinateSwapEquiv {Z : Type u_2} {n : ℕ} (k : Fin n) : (Fin n → Z) × Z ≃ (Fin n → Z) × Z

Involutive reindexing for finite coordinate swaps.

The pair (S, z) is sent to (Function.update S k z, S k): the replacement sample becomes the visible sample, and the old coordinate becomes the auxiliary summation variable.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.AlgorithmicStability.finiteProductSampleWeight_coordinateSwapIdentity {Z : Type u_2} {n : ℕ} [Fintype Z] (p : Z → ℝ) (hp_sum : ∑ z : Z, p z = 1) : FiniteCoordinateSwapIdentity (finiteProductSampleWeight p) p

Finite iid product sample weights satisfy the coordinate-swap identity.

This is a finite-domain theorem: finite data domain, finite samples, and all expectations expanded as finite sums. It removes the explicit coordinate-swap hypothesis from the finite expected-stability adapter for iid product weights. The measure-theoretic analogue is integral_update_eq_integral_coordinate.

theorem FormalSLT.AlgorithmicStability.expectedFiniteSelectedRisk_le_coordinateTraining_add_beta {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) (k : Fin n) : expectedFiniteSelectedRisk sampleWeight p A ℓ ≤ ∑ S : Fin n → Z, sampleWeight S * ℓ (A S) (S k) + β

One-coordinate finite expected stability bound.

The selected finite population risk is bounded by the coordinate-k expected training contribution plus β, provided the sample weights satisfy the finite coordinate-swap identity.

theorem FormalSLT.AlgorithmicStability.expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) : expectedFiniteStabilityGap sampleWeight p A ℓ ≤ β

Finite expected uniform-stability bound, conditional on the finite coordinate-swap identity.

If replacing one coordinate changes the selected loss by at most β, then the expected finite generalization gap of the algorithm-selected hypothesis is at most β. This closes the finite-sum adapter; the measure-theoretic iid lift is expectedStabilityGap_le_uniformStability_piMeasure.

theorem FormalSLT.AlgorithmicStability.expectedFiniteStabilityGap_le_uniformStability_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) : expectedFiniteStabilityGap (finiteProductSampleWeight p) p A ℓ ≤ β

Finite iid expected uniform-stability bound.

If the finite data law p is a probability mass function and replacing one coordinate changes the selected loss by at most β, then the expected finite generalization gap under iid finite product sample weights is at most β.

This theorem closes the finite iid coordinate-swap specialization. It does not replace the measure-theoretic iid theorem expectedStabilityGap_le_uniformStability_piMeasure, which works over Measure.pi with explicit integrability hypotheses.

theorem FormalSLT.AlgorithmicStability.neg_beta_le_expectedFiniteStabilityGap_of_coordinateSwap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) : -β ≤ expectedFiniteStabilityGap sampleWeight p A ℓ

Finite lower expected uniform-stability bound, conditional on the finite coordinate-swap identity.

This is the lower half of the two-sided finite expected-gap statement. It is obtained by applying the one-sided finite expected-stability theorem to the negated loss.

theorem FormalSLT.AlgorithmicStability.abs_expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) : |expectedFiniteStabilityGap sampleWeight p A ℓ| ≤ β

Finite two-sided expected uniform-stability bound, conditional on the finite coordinate-swap identity.

This is a finite-domain theorem: finite data domain, finite sample, explicit finite sample weights, and a finite coordinate-swap identity. It bounds the absolute value of the expected gap, not the expectation of the pointwise absolute gap.

theorem FormalSLT.AlgorithmicStability.neg_beta_le_expectedFiniteStabilityGap_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) : -β ≤ expectedFiniteStabilityGap (finiteProductSampleWeight p) p A ℓ

Finite iid lower expected uniform-stability bound.

The sample weights are the explicit finite iid product weights ∏ k, p (S k).

theorem FormalSLT.AlgorithmicStability.abs_expectedFiniteStabilityGap_le_uniformStability_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) : |expectedFiniteStabilityGap (finiteProductSampleWeight p) p A ℓ| ≤ β

Finite iid two-sided expected uniform-stability bound.

This bounds the absolute value of the expected finite stability gap under explicit finite iid product weights. It is not a measure-theoretic product space theorem.

theorem FormalSLT.AlgorithmicStability.expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) : expectedFiniteGeneralizationGap sampleWeight p A ℓ ≤ β

Finite expected generalization-gap bound, conditional on the finite coordinate-swap identity.

This is the literal E_S[R(A(S)) - Rhat_S(A(S))] ≤ β wrapper around expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap. It remains finite-domain and assumes the finite coordinate-swap identity explicitly.

theorem FormalSLT.AlgorithmicStability.expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) : expectedFiniteGeneralizationGap (finiteProductSampleWeight p) p A ℓ ≤ β

Finite iid expected generalization-gap bound for uniformly stable algorithms.

If the finite data law p is a probability mass function and replacing one training coordinate changes the selected loss by at most β, then

E_S[R(A(S)) - Rhat_S(A(S))] ≤ β

under the finite iid product sample weights ∏ k, p (S k).

This is a finite-domain theorem, scoped to finite data domains and explicit iid product weights rather than arbitrary measurable sample spaces.

theorem FormalSLT.AlgorithmicStability.neg_beta_le_expectedFiniteGeneralizationGap_of_coordinateSwap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) : -β ≤ expectedFiniteGeneralizationGap sampleWeight p A ℓ

Finite lower expected generalization-gap bound, conditional on the finite coordinate-swap identity.

This is the lower half of the two-sided literal finite E_S[R(A(S)) - Rhat_S(A(S))] statement.

theorem FormalSLT.AlgorithmicStability.neg_beta_le_expectedFiniteGeneralizationGap_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) : -β ≤ expectedFiniteGeneralizationGap (finiteProductSampleWeight p) p A ℓ

Finite iid lower expected generalization-gap bound.

theorem FormalSLT.AlgorithmicStability.abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {sampleWeight : (Fin n → Z) → ℝ} {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) (hw_nonneg : ∀ (S : Fin n → Z), 0 ≤ sampleWeight S) (hw_sum : ∑ S : Fin n → Z, sampleWeight S = 1) (hswap : FiniteCoordinateSwapIdentity sampleWeight p) : |expectedFiniteGeneralizationGap sampleWeight p A ℓ| ≤ β

Finite two-sided expected generalization-gap bound, conditional on the finite coordinate-swap identity.

This is the literal finite |E_S[R(A(S)) - Rhat_S(A(S))]| ≤ β statement. It bounds the absolute value of the expectation, not the expectation of the pointwise absolute gap.

theorem FormalSLT.AlgorithmicStability.abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct {ι : Type u_1} {Z : Type u_2} {n : ℕ} [Fintype Z] (hn : 0 < n) {p : Z → ℝ} {A : (Fin n → Z) → ι} {ℓ : ι → Z → ℝ} {β : ℝ} (hstab : UniformStability A ℓ β) (hp_nonneg : ∀ (z : Z), 0 ≤ p z) (hp_sum : ∑ z : Z, p z = 1) : |expectedFiniteGeneralizationGap (finiteProductSampleWeight p) p A ℓ| ≤ β

Finite iid two-sided expected generalization-gap bound.

For a finite data law p and explicit finite iid product sample weights, a uniformly stable algorithm satisfies |E_S[R(A(S)) - Rhat_S(A(S))]| ≤ β. This is still a finite-domain theorem, complementing the measure-theoretic product-space wrapper abs_expectedStabilityGap_le_uniformStability_piMeasure.