English
The product measure π μ has finite spanning sets in the rectangle set pi univ '' pi univ C, given that each coordinate μ_i has finite spanning sets in C_i.
Русский
Произведение меры π μ имеет конечные порождающие множества в прямоугольниках, если каждая координата μ_i имеет конечные порождающие множества в C_i.
LaTeX
$$pi μ (pi univ '' pi univ C) ∈ ...$$
Lean4
/-- `Measure.pi μ` has finite spanning sets in rectangles of finite spanning sets. -/
def pi {C : ∀ i, Set (Set (α i))} (hμ : ∀ i, (μ i).FiniteSpanningSetsIn (C i)) :
(Measure.pi μ).FiniteSpanningSetsIn (pi univ '' pi univ C) :=
by
haveI := fun i => (hμ i).sigmaFinite
haveI := Fintype.toEncodable ι
refine ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).iget i), fun n => ?_, fun n => ?_, ?_⟩ <;>
-- TODO (kmill) If this let comes before the refine, while the noncomputability checker
-- correctly sees this definition is computable, the Lean VM fails to see the binding is
-- computationally irrelevant. The `noncomputable section` doesn't help because all it does
-- is insert `noncomputable` for you when necessary.
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
· refine mem_image_of_mem _ fun i _ => (hμ i).set_mem _
·
calc
Measure.pi μ (Set.pi univ fun i => (hμ i).set (e n i)) ≤
Measure.pi μ (Set.pi univ fun i => toMeasurable (μ i) ((hμ i).set (e n i))) :=
measure_mono (pi_mono fun i _ => subset_toMeasurable _ _)
_ = ∏ i, μ i (toMeasurable (μ i) ((hμ i).set (e n i))) := (pi_pi_aux μ _ fun i => measurableSet_toMeasurable _ _)
_ = ∏ i, μ i ((hμ i).set (e n i)) := by simp only [measure_toMeasurable]
_ < ∞ := ENNReal.prod_lt_top fun i _ => (hμ i).finite _
·
simp_rw [(surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => (hμ i).set (x i),
iUnion_univ_pi fun i => (hμ i).set, (hμ _).spanning, Set.pi_univ]
