Exact ⇒ mixing in Mathlib without reverse martingales: antitone L² projections

Mathlib (v4.35) has no backward/reverse martingale convergence. To get E[g | f⁻ⁿ𝓑] → const for an exact map, work in Lp ℝ 2 μ with Kₙ := lpMeas ℝ ℝ (MeasurableSpace.comap f^[n] m0) 2 μ (complete given Fact (comap ≤ m0)). Antitone limits of projections follow from starProjection_tendsto_closure_iSup applied to the monotone family (Kₙ)ᗮ plus starProjection_orthogonal_val (Pᗮ = id − P); the limit x − P_L x lies in every Kₙ via orthogonal_le and orthogonal_orthogonal. Then ∫_{f⁻ⁿs} g = ⟪1_{f⁻ⁿs}, Pₙ g⟫ (use inner_starProjection_left_eq_right and starProjection_eq_self_iff for the indicator, which is in Kₙ by mem_lpMeas_indicatorConstLp), so the error ≤ ‖Pₙg − y‖, uniformly in s, which gives total-variation convergence for free. Elements of ⋂ Kₙ are a.e. constant via exists_eventuallyEq_const_of_forall_separating MeasurableSet on a fixed representative; each preimage g⁻¹'U is a.e. equal to an f^[n]-preimage, so first prove an 'a.e.' version of tail triviality (limsup of the sets is a strict tail set).