Compact-image measure bounds under uniform convergence. Compactness controls image neighborhoods; injectivity of the limiting map is not assumed.

theorem KamProject.Arnold1963.limsup_measure_image_le {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MetricSpace E] [ProperSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {K : Set α} (hK : IsCompact K) {F : ℕ → α → E} {f : α → E} (hf : ContinuousOn f K) (hF : TendstoUniformlyOn F f Filter.atTop K) : Filter.limsup (fun (s : ℕ) => μ (F s '' K)) Filter.atTop ≤ μ (f '' K)

theorem KamProject.Arnold1963.measure_image_ge_of_uniform_limit {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MetricSpace E] [ProperSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {K : Set α} (hK : IsCompact K) {F : ℕ → α → E} {f : α → E} (hf : ContinuousOn f K) (hF : TendstoUniformlyOn F f Filter.atTop K) {a : ENNReal} (ha : ∀ᶠ (s : ℕ) in Filter.atTop, a ≤ μ (F s '' K)) : a ≤ μ (f '' K)

theorem KamProject.Arnold1963.measure_image_gt_of_uniform_limit {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MetricSpace E] [ProperSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {K : Set α} (hK : IsCompact K) {F : ℕ → α → E} {f : α → E} (hf : ContinuousOn f K) (hF : TendstoUniformlyOn F f Filter.atTop K) {a c : ENNReal} (hca : c < a) (ha : ∀ᶠ (s : ℕ) in Filter.atTop, a ≤ μ (F s '' K)) : c < μ (f '' K)