English
Under SigmaFinite assumptions, the equality for pi_pi_aux holds expressing pi(μ) on the product set as a finite product over i.
Русский
При допущении сигма-ограниченности выполняется равенство pi_pi_aux для произведения множества.
LaTeX
$$pi_pi_aux(μ)(s) = ∏_i μ_i(s_i)$$
Lean4
theorem pi_pi_aux [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) (hs : ∀ i, MeasurableSet (s i)) :
Measure.pi μ (pi univ s) = ∏ i, μ i (s i) :=
by
refine le_antisymm ?_ ?_
· rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
apply OuterMeasure.pi_pi_le
· haveI : Encodable ι := Fintype.toEncodable ι
simp_rw [← pi'_pi μ s, Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
suffices (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i => (μ i).toOuterMeasure by exact this _
clear hs s
rw [OuterMeasure.le_pi]
intro s _
exact (pi'_pi μ s).le
