Commit 2026-03-02 18:03 453897ba

feat(MeasureTheory): tightness of the range of a sequence (#26292)

• isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt: in a proper normed group, the range of a sequence of measures μ : ℕ → Measure E is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖x‖}) atTop tends to 0 at infinity.
• isTightMeasureSet_range_iff_tendsto_limsup_inner: in a finite-dimensional inner product space, the range of a sequence of measures μ : ℕ → Measure E is tight if and only if the function r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop tends to 0 at infinity for all y.