No flow generated by a compact group has decaying correlations #
Category: 1-Mathlib. No CSD content.
Two facts the corpus already owns, joined:
HasCorrelationDecay.integral_mul_self_eq_of_recurrent— a correlation that keeps returning to its lag-zero value cannot decay to⟨f⟩²;exists_le_pow_mem_of_compactSpace— the powers of any element of a compact group keep returning to the identity.
★★ not_hasCorrelationDecay_of_compactGroup is the consequence: for a flow of the form Ψ U,
where Ψ turns powers of U into iterates and U lives in a compact group, correlation decay is
impossible for any observable of nonzero variance — provided only that the correlation function
V ↦ ∫ f(x)·f(Ψ V x) is continuous at 1.
Why it is stated with a bare Ψ, not a MulAction #
The two flows this is applied to are an action of the unitary group and a shift on a torus. The
second is additive and is not registered as an AddAction anywhere, so demanding an action
typeclass would exclude it. All the argument uses is (Ψ U)^[n] = Ψ (U ^ n), so that is what it
asks for — hpow — and Ψ 1 = id comes free from it at n = 0. Each result carries a
to_additive twin, which is what lets one proof serve both a multiplicative group action and an
additive shift.
What it does and does not say #
It does not say mixing is impossible. It says mixing is impossible for this class of
generators: genuinely mixing systems exist (MeasureTheory.circ_hasCorrelationDecay is one, on the
circle doubling map), and they are exactly the ones that are not compact-group translations.
The theorem is therefore a statement about where to look, not a no-go for the phenomenon.
Reference: specs/q12-fibre-mechanism-scoping.md (W1, of which this is the general form);
specs/equilibration-arc-plan.md (E4/E6, the source); specs/future-work.md. Consumers:
CSD.Thermo.not_hasCorrelationDecay_blockPop_of_unitary (the unitary base action) and
CSD.LF4.KahlerFlow.not_hasCorrelationDecay_kFlow (the T² fibre shift).
The correlation of a compact-group flow recurs. For any δ > 0 and any bound M there is a
lag u ≥ M at which the correlation is within δ of its lag-zero value.
This is exists_le_pow_mem_of_compactSpace transported along the correlation function: continuity
at 1 turns the neighbourhood of the identity into a neighbourhood of ⟨f²⟩.
★★ No flow generated by a compact group has decaying correlations.
For Ψ U with U in a compact group, an observable whose variance is nonzero cannot have a
summable decay envelope. Compare HasCorrelationDecay.integral_mul_self_eq_of_periodic, which is
the same obstruction in the special case where the return is exact.
The hypotheses are the minimum: hpow makes Ψ a flow along the powers of U, and hcont is what
lets a neighbourhood of the identity be read as a neighbourhood of the lag-zero correlation.
continuousAt_correlation_of_abs_sub_le supplies hcont from a uniform modulus.
A uniform modulus vanishing at the identity gives the continuity the no-go needs.
This is the shape a physical estimate actually comes in: a bound on how far the correlation can move
when the generator moves, in terms of a continuous deviation of the generator from 1.