English
If f_i ≡ f'_i almost everywhere for each i and g ≡ g' almost everywhere, TendstoInMeasure holds for (f,g) and also for (f',g').
Русский
Если f_i эквивалентны f'_i почти всюду для каждого i, и g эквивалентно g' почти всюду, то предел сохраняется при таких заменах.
LaTeX
$$TendstoInMeasure μ f l g → TendstoInMeasure μ f' l g' under ae-equality assumptions$$
Lean4
protected theorem congr' (h_left : ∀ᶠ i in l, f i =ᵐ[μ] f' i) (h_right : g =ᵐ[μ] g')
(h_tendsto : TendstoInMeasure μ f l g) : TendstoInMeasure μ f' l g' :=
by
intro ε hε
suffices (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) =ᶠ[l] fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
by
rw [tendsto_congr' this]
exact h_tendsto ε hε
filter_upwards [h_left] with i h_ae_eq
refine measure_congr ?_
filter_upwards [h_ae_eq, h_right] with x hxf hxg
rw [eq_iff_iff]
change ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g x)
rw [hxg, hxf]
