English
If g is surjective, independence of the f ∘ g family implies independence of f.
Русский
Если g сюръективна, независимость семейства f ∘ g влечет за собой независимость f.
LaTeX
$$$ \\text{Function.Surjective}(g) \\rightarrow \\operatorname{iIndepFun} (\\lambda i \\mapsto f (g i)) μ \\rightarrow \\operatorname{iIndepFun} f μ$$$
Lean4
theorem of_precomp {g : ι' → ι} (hg : g.Surjective) (h : iIndepFun (m := fun i ↦ m (g i)) (fun i ↦ f (g i)) μ) :
iIndepFun f μ := by
have : IsProbabilityMeasure μ := h.isProbabilityMeasure
nontriviality ι
have := hg.nontrivial
classical
rw [iIndepFun_iff] at h ⊢
intro t s hs
have A (x) : g (Function.invFun g x) = x := Function.rightInverse_invFun hg x
have :
∀ i ∈ Finset.image (Function.invFun g) t,
@MeasurableSet _ (MeasurableSpace.comap (f <| g i) (m <| g i)) (s <| g i) :=
by
intro i hi
obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hi
simpa [A] using (A j).symm ▸ hs j hj
have eq : ∏ i ∈ Finset.image (Function.invFun g) t, μ (s (g i)) = ∏ i ∈ t, μ (s i) :=
by
rw [Finset.prod_image (fun x hx y hy h => ?_), Finset.prod_congr rfl (fun x _ => by rw [A])]
rw [← A x, ← A y, h]
simpa [A, eq] using h (t.image (Function.invFun g)) (f' := fun i ↦ s (g i)) this
