English
Under independence of f and g, the push-forward of the product equals the monoidal convolution of pushes-forward of f and g.
Русский
При независимости f и g образ продукта равен конволюции образов f и g.
LaTeX
$$$\\mu\\text{ maps } f g \\Rightarrow \\mu\\text{ map }(f g) = (\\mu\\ map f) \\ast\\! (\\mu\\ map g)$$$
Lean4
theorem iCondIndepSets_iff (π : ι → Set (Set Ω)) (hπ : ∀ i s (_hs : s ∈ π i), MeasurableSet s) (μ : Measure Ω)
[IsFiniteMeasure μ] :
iCondIndepSets m' hm' π μ ↔
∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → f i ∈ π i), μ⟦⋂ i ∈ s, f i|m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦f i|m'⟧) :=
by
simp only [iCondIndepSets, Kernel.iIndepSets]
have h_eq' :
∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i) i (_hi : i ∈ s),
(fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (f i))) =ᵐ[μ] μ⟦f i|m'⟧ :=
fun s f H i hi ↦ condExpKernel_ae_eq_condExp hm' (hπ i (f i) (H i hi))
have h_eq :
∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i),
∀ᵐ ω ∂μ, ∀ i ∈ s, ENNReal.toReal (condExpKernel μ m' ω (f i)) = (μ⟦f i|m'⟧) ω :=
by
intro s f H
simp_rw [← Finset.mem_coe]
rw [ae_ball_iff (Finset.countable_toSet s)]
exact h_eq' s f H
have h_inter_eq :
∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i),
(fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (⋂ i ∈ s, f i))) =ᵐ[μ] μ⟦⋂ i ∈ s, f i|m'⟧ :=
by
refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_
exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H i hi))
refine ⟨fun h s f hf ↦ ?_, fun h s f hf ↦ ?_⟩ <;> specialize h s hf
· have h' := ae_eq_of_ae_eq_trim h
filter_upwards [h_eq s f hf, h_inter_eq s f hf, h'] with ω h_eq h_inter_eq h'
rw [← h_inter_eq, h', ENNReal.toReal_prod, Finset.prod_apply]
exact Finset.prod_congr rfl h_eq
· refine ((stronglyMeasurable_condExpKernel ?_).ae_eq_trim_iff hm' ?_).mpr ?_
· exact .biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (hf i hi))
· refine Measurable.stronglyMeasurable ?_
exact Finset.measurable_fun_prod s (fun i hi ↦ measurable_condExpKernel (hπ i _ (hf i hi)))
filter_upwards [h_eq s f hf, h_inter_eq s f hf, h] with ω h_eq h_inter_eq h
have h_ne_top : condExpKernel μ m' ω (⋂ i ∈ s, f i) ≠ ∞ := (measure_ne_top (condExpKernel μ m' ω) _)
have : (∏ i ∈ s, condExpKernel μ m' ω (f i)) ≠ ∞ :=
ENNReal.prod_ne_top fun _ _ ↦ measure_ne_top (condExpKernel μ m' ω) _
rw [← ENNReal.ofReal_toReal h_ne_top, h_inter_eq, h, Finset.prod_apply, ← ENNReal.ofReal_toReal this,
ENNReal.toReal_prod]
congr 1
exact Finset.prod_congr rfl (fun i hi ↦ (h_eq i hi).symm)
