English
Same equivalence as above but in a general ae-map context: equivalence of measurable property under mapping.
Русский
Та же эквивалентность для отображения и мер АЕ.
LaTeX
$$ae_comp_linearMap_mem_iff (surjective L) (hs) : (∀ᵐ x, Lx ∈ s) ↔ ∀ᵐ y, y ∈ s$$
Lean4
/-- Given a linear map `L : E → F`, a property holds almost everywhere in `F` if and only if,
almost everywhere in `F`, it holds almost everywhere along the subspace spanned by the
image of `L`. This is an instance of a disintegration argument for additive Haar measures. -/
theorem ae_ae_add_linearMap_mem_iff [LocallyCompactSpace F] {s : Set F} (hs : MeasurableSet s) :
(∀ᵐ y ∂ν, ∀ᵐ x ∂μ, y + L x ∈ s) ↔ ∀ᵐ y ∂ν, y ∈ s :=
by
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
have : FiniteDimensional 𝕜 F := .of_locallyCompactSpace 𝕜
have : ProperSpace E := .of_locallyCompactSpace 𝕜
have : ProperSpace F := .of_locallyCompactSpace 𝕜
let M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
have M_cont : Continuous M := M.continuous_of_finiteDimensional
have hM : Function.Surjective M := by simp [M, ← LinearMap.range_eq_top (f := _), LinearMap.range_coprod]
have A : ∀ x, M x ∈ s ↔ x ∈ M ⁻¹' s := fun x ↦ Iff.rfl
simp_rw [← ae_comp_linearMap_mem_iff M (ν.prod μ) ν hM hs, A]
rw [Measure.ae_prod_mem_iff_ae_ae_mem]
· simp only [M, mem_preimage, LinearMap.coprod_apply, LinearMap.id_coe, id_eq]
· exact M_cont.measurable hs
