English
Given surjective L, a set s measurable satisfies almost-everywhere condition for y+Lx in s iff y in s holds almost everywhere.
Русский
Пусть L сюръективен; тогда условие почти везде для y+Lx в s эквивалентно тому, что почти везде y ∈ s.
LaTeX
$$ae_ae_add_linearMap_mem' (surjective L) : ∀ᵐ y, (∀ᵐ x, y+Lx ∈ s) ⇔ ∀ᵐ y, y ∈ s$$
Lean4
/-- Given a surjective linear map `L`, it is equivalent to require a property almost everywhere
in the source or the target spaces of `L`, with respect to additive Haar measures there. -/
theorem ae_comp_linearMap_mem_iff (h : Function.Surjective L) {s : Set F} (hs : MeasurableSet s) :
(∀ᵐ x ∂μ, L x ∈ s) ↔ ∀ᵐ y ∂ν, y ∈ s :=
by
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
have : AEMeasurable L μ := L.continuous_of_finiteDimensional.aemeasurable
apply (ae_map_iff this hs).symm.trans
rcases L.exists_map_addHaar_eq_smul_addHaar μ ν h with ⟨c, c_pos, hc⟩
rw [hc]
exact ae_smul_measure_iff c_pos.ne'
