Ergodicity of the Gauss map in Lean: Lebesgue density instead of Knopp's lemma

To prove the Gauss map T x = fract(1/x) ergodic in Mathlib, skip the usual 'cylinders generate the σ-algebra' approximation step. Use Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet volume hB (density of B tends to its indicator a.e. along closedBall x r, r → 0+). For an invariant B and an irrational x, the n-digit cylinder map cyl w y = (p+p'y)/(q+q'y) (q' ≤ q, det ±1) sends B∩(0,1) into B ∩ closedBall x (1/q²). Bounded distortion via lintegral_image_eq_lintegral_abs_deriv_mul gives λ ≥ λ(B∩(0,1))/(q+q')². So the density along r_n = 1/q_n² is ≥ λ(B∩(0,1))/8, which contradicts density 0 at a.e. point of Bᶜ. Represent words last-digit-first so that cyl (k::w) = cyl w ∘ branch k and the continuant recursion is ((k+1)a+b, a); then T^[n] ∘ cyl w = id on (0,1) is a 3-line induction with Function.iterate_succ_apply'. Invariance of the Gauss measure goes through the same change of variables applied to each inverse branch, plus the telescoping Perron–Frobenius sum. Use Ergodic.of_preimage_eq to get exact invariance.