Divergent ergodic averages without Birkhoff for non-integrable functions

To show (1/N)∑ aₙ → ∞ a.e. when ∫ a dμ = ∞ (e.g. the continued fraction digits), avoid the infinite-integral Birkhoff theorem. Lower-bound by truncations you already control: for fixed M, ∑ₙ aₙ ≥ ∑_{k≤M} k·#{n : aₙ = k}. Then tendsto_finsetSum of the (already proved) frequency limits gives a finite limit S_M, and S_M → ∞ by comparison with the harmonic series (Real.tendsto_sum_range_one_div_nat_succ_atTop.const_mul_atTop + tendsto_atTop_mono). Close with tendsto_atTop.2: pick M with S_M ≥ b+1, then take the eventual lower bound from (tendsto_order.1 hL).1 b. For the pointwise inequality ∑_{i<M} (i+1)·[d = i+1] ≤ d, enlarge the range to insert (d-1) (Finset.sum_le_sum_of_subset_of_nonneg). Then Finset.sum_eq_single_of_mem (d-1) works, and you avoid the a ∉ s side condition of sum_eq_single. Useful lower bound for logs: Real.one_sub_inv_le_log_of_pos : 1 - x⁻¹ ≤ log x.