Trainability: exponential concentration and barren plateaus

The unifying notion behind barren plateaus (McClean et al. 2018) and quantum-kernel concentration (Thanasilp et al. 2022, Def. 1) is exponential concentration: a quantity indexed by system size n (a loss, a gradient variance, or a kernel value) deviates from a fixed value μ by at most C / b ^ n for some b > 1. The practical consequence is that the quantity becomes exponentially flat — it converges to μ, so resolving it requires exponentially many samples.

This module gives the definition and its convergence consequence, and records the barren-plateau models on top of it in the GroverModel/ParamShiftModel style: the hard Haar / t-design / Weingarten input (the variance bound) is bundled as a hypothesis, and the trainability consequence is derived.

Sources: McClean, Boixo, Smelyanskiy, Babbush, Neven (2018); Cerezo, Sone, Volkoff, Cincio, Coles (2021); Ragone et al. (2023); Thanasilp, Wang, Cerezo, Holmes (2022).

def QuantumAlg.ExpConcentrated (X : ℕ → ℝ) (μ : ℝ) : Prop

Exponential concentration. X n deviates from μ by at most C / b ^ n for some base b > 1 (McClean 2018; Thanasilp 2022, Def. 1).

Equations

• QuantumAlg.ExpConcentrated X μ = ∃ (b : ℝ), 1 < b ∧ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ), |X n - μ| ≤ C / b ^ n

theorem QuantumAlg.ExpConcentrated.tendsto {X : ℕ → ℝ} {μ : ℝ} (h : ExpConcentrated X μ) : Filter.Tendsto X Filter.atTop (nhds μ)

An exponentially concentrated quantity converges to its concentration value: the landscape becomes exponentially flat.

def QuantumAlg.HasBarrenPlateau (variance : ℕ → ℝ) : Prop

A model has a barren plateau when its loss/gradient variance is exponentially concentrated to 0 (so the trainable signal vanishes with system size).

Equations

• QuantumAlg.HasBarrenPlateau variance = QuantumAlg.ExpConcentrated variance 0

theorem QuantumAlg.HasBarrenPlateau.variance_tendsto_zero {variance : ℕ → ℝ} (h : HasBarrenPlateau variance) : Filter.Tendsto variance Filter.atTop (nhds 0)

Under a barren plateau the variance vanishes in the large-system limit.

Lie-algebraic barren plateaus

structure QuantumAlg.LieAlgebraicVariance : Type

Lie-algebraic barren plateaus (Ragone et al. 2023). In the simple-DLA case the loss variance is P_g(ρ) P_g(O) / dim(g) (their Eq. (10)); bundling the numerator and the DLA dimension, an exponentially large dynamical Lie algebra forces a barren plateau.

• gdim : ℕ → ℝ

  dim g as a function of the system size.

• numer : ℝ

  The g-purity numerator P_g(ρ) P_g(O).

• numer_nonneg : 0 ≤ self.numer

  The numerator is nonnegative.

• gdim_pos (n : ℕ) : 0 < self.gdim n

  The DLA dimension is positive.

• variance : ℕ → ℝ

  The loss variance.

• variance_eq (n : ℕ) : self.variance n = self.numer / self.gdim n

  Ragone et al. (2023), Eq. (10): variance = P_g(ρ) P_g(O) / dim(g).

theorem QuantumAlg.LieAlgebraicVariance.hasBarrenPlateau_of_exp_dim (M : LieAlgebraicVariance) {b : ℝ} (hb : 1 < b) (hdim : ∀ (n : ℕ), b ^ n ≤ M.gdim n) : HasBarrenPlateau M.variance

An exponentially large dynamical Lie algebra forces a barren plateau.

Cost-function-dependent barren plateaus

structure QuantumAlg.CostDependentBP : Type

Cost-function-dependent barren plateaus (Cerezo et al. 2021): a global cost exhibits a barren plateau (exponentially concentrated gradient variance), whereas a local cost is trainable (its gradient variance has a polynomial lower bound).

• globalVariance : ℕ → ℝ

  Gradient variance of the global cost.

• localVariance : ℕ → ℝ

  Gradient variance of the local cost.

• global_bp : HasBarrenPlateau self.globalVariance

  The global cost has a barren plateau.

• local_lb (n : ℕ) : 0 < n → 1 / ↑n ≤ self.localVariance n

  The local cost keeps a polynomial lower bound.

theorem QuantumAlg.CostDependentBP.global_tendsto_zero (M : CostDependentBP) : Filter.Tendsto M.globalVariance Filter.atTop (nhds 0)

The global cost's gradient vanishes (barren plateau).

theorem QuantumAlg.CostDependentBP.local_pos (M : CostDependentBP) {n : ℕ} (hn : 0 < n) : 0 < M.localVariance n

The local cost's gradient variance stays strictly positive (trainable).

Quantum-kernel concentration

def QuantumAlg.KernelConcentration (kernel : ℕ → ℝ) (κ₀ : ℝ) : Prop

Quantum-kernel concentration (Thanasilp et al. 2022): the kernel value concentrates exponentially to a fixed κ₀, so a polynomial number of measurement shots cannot distinguish inputs (the model becomes input-independent).

This is the abstract deterministic-sequence form. The genuine probabilistic result — a concrete quantum kernel whose data-averaged value provably concentrates exponentially, derived from first principles with no Haar assumption — is LeanPool.LeanQuantumAlg.ryKernel_concentrates in QuantumAlg/Primitives/KernelConcentration.lean, built on the probabilistic engine LeanPool.LeanQuantumAlg.ExpConcentratedProb.

Equations

• QuantumAlg.KernelConcentration kernel κ₀ = QuantumAlg.ExpConcentrated kernel κ₀

theorem QuantumAlg.KernelConcentration.tendsto {kernel : ℕ → ℝ} {κ₀ : ℝ} (h : KernelConcentration kernel κ₀) : Filter.Tendsto kernel Filter.atTop (nhds κ₀)

A concentrated kernel converges to its concentration value.

Geometric/equivariant QML trainability

structure QuantumAlg.GeometricQMLTrainable : Type

Geometric/equivariant QML trainability (Ragone et al. 2022 + the DLA variance law). A symmetry-structured model whose dynamical Lie algebra has only polynomial dimension keeps a polynomial lower bound on its gradient variance, hence avoids a barren plateau.

• variance : ℕ → ℝ

  Gradient variance.

• deg : ℕ

  Polynomial degree of the lower bound.

• variance_lb (n : ℕ) : 0 < n → 1 / ↑n ^ self.deg ≤ self.variance n

  The variance is bounded below by 1 / n ^ deg (polynomial trainability).

theorem QuantumAlg.GeometricQMLTrainable.variance_pos (M : GeometricQMLTrainable) {n : ℕ} (hn : 0 < n) : 0 < M.variance n

A geometric/equivariant model with polynomial dynamical Lie algebra has strictly positive (not exponentially vanishing) gradient variance: it is trainable.