Shared helper for the alphaIicCE endpoint limits

Both alphaIicCE_ae_tendsto_zero_atBot (EndpointAtBot) and alphaIicCE_ae_tendsto_one_atTop (EndpointAtTop) need the same generic measure-theoretic fact:

If a uniformly bounded sequence f : ℕ → Ω → ℝ converges pointwise a.e. (to some L) and also converges to a constant c in L¹, then the pointwise limit equals c a.e., so f n ω → c a.e.

This is the "L¹-limit-of-a-constant-identifies-the-pointwise-limit" lemma, extracted into one private helper so the endpoint files can each derive pointwise convergence to their target without duplicating the dominated-convergence + integral_eq_zero_iff_of_nonneg_ae machinery.

theorem Exchangeability.DeFinetti.ViaL2.ae_tendsto_const_of_ae_convergent_of_L1_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {f : ℕ → Ω → ℝ} {L : Ω → ℝ} {c C : ℝ} (hf_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hf_bound : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, ‖f n ω‖ ≤ C) (hf_ae : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds (L ω))) (hf_L1 : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |f n ω - c| ∂μ) Filter.atTop (nhds 0)) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds c)

A.e. pointwise limit equals the L¹-limit constant.

If a uniformly bounded sequence f : ℕ → Ω → ℝ converges pointwise a.e. to L : Ω → ℝ and also converges to a constant c in L¹ (in the sense that ∫ |f n - c| → 0), then L = c a.e., so f n ω → c for a.e. ω.

The proof routes through dominated convergence: |f n - c| is uniformly bounded by C + |c|, converges pointwise a.e. to |L - c|, and has integrals tending to 0, so ∫ |L - c| = 0. Since |L - c| ≥ 0, that forces L = c a.e.