Proof of `The top-level fast/slow decomposition`
groundedproofs/Lax606786Proofs/NodeStatements.lean · lax-606786
What this proof establishes
- thm✓
Lax606786.BalancedKingman - thm✓
Lax606786.BirkhoffErgodicTheorem - thm✓
Lax606786.ExponentLimits - thm✓
Lax606786.GrowthFunctionProperties - thm✓
Lax606786.GrowthUnderProjections - thm✓
Lax606786.MaximalErgodicTheorem - thm✓
Lax606786.MeasurableBases - thm✓
Lax606786.MeasurableOperatorFamilies - thm✓
Lax606786.RecurrenceAndInvariance - thm✓
Lax606786.TopFastSpace - thm✓
Lax606786.VolumeGrowthComparison
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The slow projection is assembled from slow representatives of the cosets of the top fast space, and is tempered by Birkhoff's theorem along shifted averages.