English
If κ is IsSFiniteKernel, then comapRight κ hf is IsSFiniteKernel.
Русский
Если κ — IsSFiniteKernel, то comapRight κ hf — IsSFiniteKernel.
LaTeX
$$$\\text{IsSFiniteKernel}(\\kappa\\, hf)$$$
Lean4
protected instance comapRight (κ : Kernel α β) [IsSFiniteKernel κ] (hf : MeasurableEmbedding f) :
IsSFiniteKernel (comapRight κ hf) :=
by
refine ⟨⟨fun n => comapRight (seq κ n) hf, inferInstance, ?_⟩⟩
ext1 a
rw [sum_apply]
simp_rw [comapRight_apply _ hf]
have : (Measure.sum fun n => Measure.comap f (seq κ n a)) = Measure.comap f (Measure.sum fun n => seq κ n a) :=
by
ext1 t ht
rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht, Measure.sum_apply _ ht,
Measure.sum_apply _ (hf.measurableSet_image.mpr ht)]
congr with n : 1
rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]
rw [this, measure_sum_seq]
