[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
⊢ IsPiSystem (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
rintro _ ⟨s₁, hs₁, rfl⟩ _ ⟨s₂, hs₂, rfl⟩ hst
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ Set.pi univ C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ Set.pi univ C
hst : Set.Nonempty (Set.pi univ s₁ ∩ Set.pi univ s₂)
⊢ Set.pi univ s₁ ∩ Set.pi univ s₂ ∈ Set.pi univ '' Set.pi univ C
[PROOFSTEP]
rw [← pi_inter_distrib] at hst ⊢
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ Set.pi univ C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ Set.pi univ C
hst : Set.Nonempty (Set.pi univ fun i => s₁ i ∩ s₂ i)
⊢ (Set.pi univ fun i => s₁ i ∩ s₂ i) ∈ Set.pi univ '' Set.pi univ C
[PROOFSTEP]
rw [univ_pi_nonempty_iff] at hst
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ Set.pi univ C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ Set.pi univ C
hst : ∀ (i : ι), Set.Nonempty (s₁ i ∩ s₂ i)
⊢ (Set.pi univ fun i => s₁ i ∩ s₂ i) ∈ Set.pi univ '' Set.pi univ C
[PROOFSTEP]
exact mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
choose s h1s h2s using hC
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ (n : ℕ), s i n = univ
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
cases nonempty_encodable (ι → ℕ)
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ (n : ℕ), s i n = univ
val✝ : Encodable (ι → ℕ)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ (n : ℕ), s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ IsCountablySpanning (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
refine' ⟨fun n => Set.pi univ fun i => s i (e n i), fun n => mem_image_of_mem _ fun i _ => h1s i _, _⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ (n : ℕ), s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ ⋃ (n : ℕ), (fun n => Set.pi univ fun i => s i (e n i)) n = univ
[PROOFSTEP]
simp_rw [(surjective_decode_iget (ι → ℕ)).iUnion_comp fun x => Set.pi univ fun i => s i (x i), iUnion_univ_pi s, h2s,
  pi_univ]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ MeasurableSpace.pi = generateFrom (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
cases nonempty_encodable ι
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ MeasurableSpace.pi = generateFrom (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case intro.a
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ MeasurableSpace.pi ≤ generateFrom (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case intro.a
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
intro i
[GOAL]
case intro.a
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
rw [comap_generateFrom]
[GOAL]
case intro.a
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ generateFrom ((preimage fun b => b i) '' C i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
apply generateFrom_le
[GOAL]
case intro.a.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ (t : Set ((a : ι) → (fun i => α i) a)), t ∈ (preimage fun b => b i) '' C i → MeasurableSet t
[PROOFSTEP]
rintro _ ⟨s, hs, rfl⟩
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
[PROOFSTEP]
dsimp
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
[PROOFSTEP]
choose t h1t h2t using hC
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
[PROOFSTEP]
simp_rw [eval_preimage, ← h2t]
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i s))
[PROOFSTEP]
rw [← @iUnion_const _ ℕ _ s]
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i (⋃ (x : ℕ), s)))
[PROOFSTEP]
have :
  Set.pi univ (update (fun i' : ι => iUnion (t i')) i (⋃ _ : ℕ, s)) =
    Set.pi univ fun k => ⋃ j : ℕ, @update ι (fun i' => Set (α i')) _ (fun i' => t i' j) i s k :=
  by
  ext; simp_rw [mem_univ_pi]; apply forall_congr'; intro i'
  by_cases h : i' = i
  · subst h; simp
  · rw [← Ne.def] at h ; simp [h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
⊢ Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) ↔
    x✝ ∈ Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
[PROOFSTEP]
simp_rw [mem_univ_pi]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i_1
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι),
    x✝ a ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) a ↔ x✝ a ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s a
[PROOFSTEP]
intro i'
[GOAL]
case h.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
i' : ι
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
[PROOFSTEP]
by_cases h : i' = i
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : i' = i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
i' : ι
s : Set ((fun i => α i) i')
hs : s ∈ C i'
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i' (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i' s i'
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : ¬i' = i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
[PROOFSTEP]
rw [← Ne.def] at h
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : i' ≠ i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
[PROOFSTEP]
simp [h]
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i (⋃ (x : ℕ), s)))
[PROOFSTEP]
rw [this, ← iUnion_univ_pi]
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ MeasurableSet (⋃ (x : ι → ℕ), Set.pi univ fun i_1 => update (fun i' => t i' (x i_1)) i s i_1)
[PROOFSTEP]
apply MeasurableSet.iUnion
[GOAL]
case intro.a.h.intro.intro.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ ∀ (b : ι → ℕ), MeasurableSet (Set.pi univ fun i_1 => update (fun i' => t i' (b i_1)) i s i_1)
[PROOFSTEP]
intro n
[GOAL]
case intro.a.h.intro.intro.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ MeasurableSet (Set.pi univ fun i_1 => update (fun i' => t i' (n i_1)) i s i_1)
[PROOFSTEP]
apply measurableSet_generateFrom
[GOAL]
case intro.a.h.intro.intro.h.ht
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ (Set.pi univ fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) ∈ Set.pi univ '' Set.pi univ C
[PROOFSTEP]
apply mem_image_of_mem
[GOAL]
case intro.a.h.intro.intro.h.ht.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ (fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) ∈ Set.pi univ C
[PROOFSTEP]
intro j _
[GOAL]
case intro.a.h.intro.intro.h.ht.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ (fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) j ∈ C j
[PROOFSTEP]
dsimp only
[GOAL]
case intro.a.h.intro.intro.h.ht.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
n : ι → ℕ
j : ι
a✝ : j ∈ univ
s : Set ((fun i => α i) j)
hs : s ∈ C j
this :
  Set.pi univ (update (fun i' => iUnion (t i')) j (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j_1 : ℕ), update (fun i' => t i' j_1) j s k
⊢ update (fun i' => t i' (n j)) j s j ∈ C j
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
[PROOFSTEP]
rwa [update_same]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
[PROOFSTEP]
rw [update_noteq h]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ (n : ℕ), t i n = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ t j (n j) ∈ C j
[PROOFSTEP]
apply h1t
[GOAL]
case intro.a
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ generateFrom (Set.pi univ '' Set.pi univ C) ≤ MeasurableSpace.pi
[PROOFSTEP]
apply generateFrom_le
[GOAL]
case intro.a.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (t : Set ((i : ι) → α i)), t ∈ Set.pi univ '' Set.pi univ C → MeasurableSet t
[PROOFSTEP]
rintro _ ⟨s, hs, rfl⟩
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ MeasurableSet (Set.pi univ s)
[PROOFSTEP]
rw [univ_pi_eq_iInter]
[GOAL]
case intro.a.h.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ MeasurableSet (⋂ (i : ι), eval i ⁻¹' s i)
[PROOFSTEP]
apply MeasurableSet.iInter
[GOAL]
case intro.a.h.intro.intro.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)
[PROOFSTEP]
intro i
[GOAL]
case intro.a.h.intro.intro.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
i : ι
⊢ MeasurableSet (eval i ⁻¹' s i)
[PROOFSTEP]
apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))
[GOAL]
case intro.a.h.intro.intro.h.a
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
i : ι
⊢ MeasurableSet (s i)
[PROOFSTEP]
exact measurableSet_generateFrom (hs i (mem_univ i))
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
h : (i : ι) → MeasurableSpace (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = h i
h2C : ∀ (i : ι), IsCountablySpanning (C i)
⊢ generateFrom (Set.pi univ '' Set.pi univ C) = MeasurableSpace.pi
[PROOFSTEP]
rw [← funext hC, generateFrom_pi_eq h2C]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
hs : Set.Nonempty (Set.pi univ s)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
simp [hs, piPremeasure]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : IsEmpty ι
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
simp [piPremeasure]
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
cases' (pi univ s).eq_empty_or_nonempty with h h
[GOAL]
case inr.inl
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
[GOAL]
case inr.inl.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
⊢ ↑(m i) (s i) = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case inr.inl.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.pi univ s = ∅
i : ι
hi : s i = ∅
this : ∃ i, ↑(m i) (s i) = 0
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
simpa [h, Finset.card_univ, zero_pow (Fintype.card_pos_iff.mpr ‹_›), @eq_comm _ (0 : ℝ≥0∞), Finset.prod_eq_zero_iff,
  piPremeasure]
[GOAL]
case inr.inr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : Set.Nonempty (Set.pi univ s)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
simp [h, piPremeasure]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ piPremeasure m (Set.pi univ fun i => eval i '' s) = piPremeasure m s
[PROOFSTEP]
simp only [eval, piPremeasure_pi']
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ ∏ i : ι, ↑(m i) ((fun a => a i) '' s) = piPremeasure m s
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
cases' (pi univ s).eq_empty_or_nonempty with h h
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.pi univ s = ∅
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
case inr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.Nonempty (Set.pi univ s)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
simp [h]
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.Nonempty (Set.pi univ s)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
exact (boundedBy_le _).trans_eq (piPremeasure_pi h)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ n ≤ OuterMeasure.pi m ↔
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
rw [OuterMeasure.pi, le_boundedBy']
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s) ↔
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
intro h s hs
[GOAL]
case mp
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s
s : (i : ι) → Set (α i)
hs : Set.Nonempty (Set.pi univ s)
⊢ ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
[PROOFSTEP]
refine' (h _ hs).trans_eq (piPremeasure_pi hs)
[GOAL]
case mpr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s
[PROOFSTEP]
intro h s hs
[GOAL]
case mpr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
s : Set ((i : ι) → α i)
hs : Set.Nonempty s
⊢ ↑n s ≤ piPremeasure m s
[PROOFSTEP]
refine' le_trans (n.mono <| subset_pi_eval_image univ s) (h _ _)
[GOAL]
case mpr
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
s : Set ((i : ι) → α i)
hs : Set.Nonempty s
⊢ Set.Nonempty (Set.pi univ fun i => eval i '' s)
[PROOFSTEP]
simp [univ_pi_nonempty_iff, hs]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝ : (x : δ) → MeasurableSpace (π x)
l : List δ
μ : (i : δ) → Measure (π i)
⊢ Measure (TProd π l)
[PROOFSTEP]
induction' l with i l ih
[GOAL]
case nil
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
⊢ Measure (TProd π [])
[PROOFSTEP]
exact dirac PUnit.unit
[GOAL]
case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
i : δ
l : List δ
ih : Measure (TProd π l)
⊢ Measure (TProd π (i :: l))
[PROOFSTEP]
have := (μ i).prod (α := π i) ih
[GOAL]
case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
i : δ
l : List δ
ih : Measure (TProd π l)
this : Measure (π i × TProd π l)
⊢ Measure (TProd π (i :: l))
[PROOFSTEP]
exact this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
l : List δ
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod l μ)
[PROOFSTEP]
induction l with
| nil => rw [tprod_nil]; infer_instance
| cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ ih _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
l : List δ
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod l μ)
[PROOFSTEP]
induction l with
| nil => rw [tprod_nil]; infer_instance
| cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ ih _
[GOAL]
case nil
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod [] μ)
[PROOFSTEP]

| nil => rw [tprod_nil]; infer_instance
[GOAL]
case nil
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (Measure.tprod [] μ)
[PROOFSTEP]
rw [tprod_nil]
[GOAL]
case nil
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (dirac PUnit.unit)
[PROOFSTEP]
infer_instance
[GOAL]
case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod l μ)
⊢ SigmaFinite (Measure.tprod (i :: l) μ)
[PROOFSTEP]

| cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ ih _
[GOAL]
case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod l μ)
⊢ SigmaFinite (Measure.tprod (i :: l) μ)
[PROOFSTEP]
rw [tprod_cons]
[GOAL]
case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod l μ)
⊢ SigmaFinite (Measure.prod (μ i) (Measure.tprod l μ))
[PROOFSTEP]
exact @prod.instSigmaFinite _ _ _ _ _ _ ih _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
l : List δ
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
⊢ ↑↑(Measure.tprod l μ) (Set.tprod l s) = List.prod (List.map (fun i => ↑↑(μ i) (s i)) l)
[PROOFSTEP]
induction' l with i l ih
[GOAL]
case nil
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
⊢ ↑↑(Measure.tprod [] μ) (Set.tprod [] s) = List.prod (List.map (fun i => ↑↑(μ i) (s i)) [])
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
π : δ → Type u_5
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (π i)
i : δ
l : List δ
ih : ↑↑(Measure.tprod l μ) (Set.tprod l s) = List.prod (List.map (fun i => ↑↑(μ i) (s i)) l)
⊢ ↑↑(Measure.tprod (i :: l) μ) (Set.tprod (i :: l) s) = List.prod (List.map (fun i => ↑↑(μ i) (s i)) (i :: l))
[PROOFSTEP]
rw [tprod_cons, Set.tprod, prod_prod, map_cons, prod_cons, ih]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(pi' μ) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [pi']
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(map (TProd.elim' (_ : ∀ (x : ι), x ∈ sortedUniv ι)) (Measure.tprod (sortedUniv ι) μ)) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
simp only [TProd.elim']
  -- Porting note: new step
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(map (fun v i => TProd.elim v (_ : i ∈ sortedUniv ι)) (Measure.tprod (sortedUniv ι) μ)) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
erw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
  MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ← List.prod_toFinset,
  sortedUniv_toFinset]
[GOAL]
case _hl
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ Nodup (sortedUniv ι)
[PROOFSTEP]
exact sortedUniv_nodup ι
[GOAL]
case hnd
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ Nodup (sortedUniv ι)
[PROOFSTEP]
exact sortedUniv_nodup ι
[GOAL]
case hnd
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ Nodup (sortedUniv ι)
[PROOFSTEP]
exact sortedUniv_nodup ι
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurableSpace.pi ≤ OuterMeasure.caratheodory (OuterMeasure.pi fun i => ↑(μ i))
[PROOFSTEP]
refine' iSup_le _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun a => inst✝ a) i) ≤
      OuterMeasure.caratheodory (OuterMeasure.pi fun i => ↑(μ i))
[PROOFSTEP]
intro i s hs
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s
[PROOFSTEP]
rw [MeasurableSpace.comap] at hs
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s
[PROOFSTEP]
rcases hs with ⟨s, hs, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
[PROOFSTEP]
apply boundedBy_caratheodory
[GOAL]
case intro.intro.hs
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (fun i => ↑(μ i)) (t ∩ (fun b => b i) ⁻¹' s) +
        piPremeasure (fun i => ↑(μ i)) (t \ (fun b => b i) ⁻¹' s) ≤
      piPremeasure (fun i => ↑(μ i)) t
[PROOFSTEP]
intro t
[GOAL]
case intro.intro.hs
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i => ↑(μ i)) (t ∩ (fun b => b i) ⁻¹' s) +
      piPremeasure (fun i => ↑(μ i)) (t \ (fun b => b i) ⁻¹' s) ≤
    piPremeasure (fun i => ↑(μ i)) t
[PROOFSTEP]
simp_rw [piPremeasure]
[GOAL]
case intro.intro.hs
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∏ x : ι, ↑↑(μ x) (eval x '' (t ∩ (fun b => b i) ⁻¹' s)) + ∏ x : ι, ↑↑(μ x) (eval x '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ∏ x : ι, ↑↑(μ x) (eval x '' t)
[PROOFSTEP]
refine' Finset.prod_add_prod_le' (Finset.mem_univ i) _ _ _
[GOAL]
case intro.intro.hs.refine'_1
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ↑↑(μ i) (eval i '' (t ∩ (fun b => b i) ⁻¹' s)) + ↑↑(μ i) (eval i '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ↑↑(μ i) (eval i '' t)
[PROOFSTEP]
simp [image_inter_preimage, image_diff_preimage, measure_inter_add_diff _ hs, le_refl]
[GOAL]
case intro.intro.hs.refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → ↑↑(μ j) (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
[PROOFSTEP]
rintro j - _
[GOAL]
case intro.intro.hs.refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ ↑↑(μ j) (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
[PROOFSTEP]
apply mono'
[GOAL]
case intro.intro.hs.refine'_2.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ eval j '' (t ∩ (fun b => b i) ⁻¹' s) ⊆ eval j '' t
[PROOFSTEP]
apply image_subset
[GOAL]
case intro.intro.hs.refine'_2.h.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t ∩ (fun b => b i) ⁻¹' s ⊆ t
[PROOFSTEP]
apply inter_subset_left
[GOAL]
case intro.intro.hs.refine'_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → ↑↑(μ j) (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
[PROOFSTEP]
rintro j - _
[GOAL]
case intro.intro.hs.refine'_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ ↑↑(μ j) (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
[PROOFSTEP]
apply mono'
[GOAL]
case intro.intro.hs.refine'_3.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ eval j '' (t \ (fun b => b i) ⁻¹' s) ⊆ eval j '' t
[PROOFSTEP]
apply image_subset
[GOAL]
case intro.intro.hs.refine'_3.h.h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t \ (fun b => b i) ⁻¹' s ⊆ t
[PROOFSTEP]
apply diff_subset
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) ≤ ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑(OuterMeasure.pi fun i => ↑(μ i)) (Set.pi univ fun i => s i) ≤ ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
apply OuterMeasure.pi_pi_le
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i : ι, ↑↑(μ i) (s i) ≤ ↑↑(Measure.pi μ) (Set.pi univ s)
[PROOFSTEP]
haveI : Encodable ι := Fintype.toEncodable ι
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ ∏ i : ι, ↑↑(μ i) (s i) ≤ ↑↑(Measure.pi μ) (Set.pi univ s)
[PROOFSTEP]
simp_rw [← pi'_pi μ s, Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ ↑↑(pi' μ) (Set.pi univ s) ≤ ↑(OuterMeasure.pi fun i => ↑(μ i)) (Set.pi univ fun i => s i)
[PROOFSTEP]
suffices (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i => (μ i).toOuterMeasure by exact this _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this✝ : Encodable ι
this : ↑(pi' μ) ≤ OuterMeasure.pi fun i => ↑(μ i)
⊢ ↑↑(pi' μ) (Set.pi univ s) ≤ ↑(OuterMeasure.pi fun i => ↑(μ i)) (Set.pi univ fun i => s i)
[PROOFSTEP]
exact this _
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ ↑(pi' μ) ≤ OuterMeasure.pi fun i => ↑(μ i)
[PROOFSTEP]
clear hs s
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ ↑(pi' μ) ≤ OuterMeasure.pi fun i => ↑(μ i)
[PROOFSTEP]
rw [OuterMeasure.le_pi]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑↑(pi' μ) (Set.pi univ s) ≤ ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
intro s _
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
s : (i : ι) → Set (α i)
a✝ : Set.Nonempty (Set.pi univ s)
⊢ ↑↑(pi' μ) (Set.pi univ s) ≤ ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
exact (pi'_pi μ s).le
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
⊢ FiniteSpanningSetsIn (Measure.pi μ) (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
haveI := fun i => (hμ i).sigmaFinite
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ FiniteSpanningSetsIn (Measure.pi μ) (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
haveI := Fintype.toEncodable ι
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ FiniteSpanningSetsIn (Measure.pi μ) (Set.pi univ '' Set.pi univ C)
[PROOFSTEP]
refine' ⟨fun n => Set.pi univ fun i => (hμ i).set ((@decode (ι → ℕ) _ n).iget i), fun n => _, fun n => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
⊢ (fun n => Set.pi univ fun i => FiniteSpanningSetsIn.set (hμ i) (Option.iget (decode n) i)) n ∈
    Set.pi univ '' Set.pi univ C
[PROOFSTEP]
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
⊢ ↑↑(Measure.pi μ) ((fun n => Set.pi univ fun i => FiniteSpanningSetsIn.set (hμ i) (Option.iget (decode n) i)) n) < ⊤
[PROOFSTEP]
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
[GOAL]
case refine'_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ ⋃ (i : ℕ), (fun n => Set.pi univ fun i => FiniteSpanningSetsIn.set (hμ i) (Option.iget (decode n) i)) i = univ
[PROOFSTEP]
let e : ℕ → ι → ℕ := fun n => (@decode (ι → ℕ) _ n).iget
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ (fun n => Set.pi univ fun i => FiniteSpanningSetsIn.set (hμ i) (Option.iget (decode n) i)) n ∈
    Set.pi univ '' Set.pi univ C
[PROOFSTEP]
refine' mem_image_of_mem _ fun i _ => (hμ i).set_mem _
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ ↑↑(Measure.pi μ) ((fun n => Set.pi univ fun i => FiniteSpanningSetsIn.set (hμ i) (Option.iget (decode n) i)) n) < ⊤
[PROOFSTEP]
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 _).ne
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
n : ℕ
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ ∏ i : ι, ↑↑(μ i) (toMeasurable (μ i) (FiniteSpanningSetsIn.set (hμ i) (e n i))) =
    ∏ i : ι, ↑↑(μ i) (FiniteSpanningSetsIn.set (hμ i) (e n i))
[PROOFSTEP]
simp only [measure_toMeasurable]
[GOAL]
case refine'_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun n => Option.iget (decode n)
⊢ ⋃ (i : ℕ), (fun n => Set.pi univ fun i => FiniteSpanningSetsIn.set (hμ i) (Option.iget (decode n) i)) i = univ
[PROOFSTEP]
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]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
i : ι
⊢ MeasurableSpace (α i)
[PROOFSTEP]
apply_assumption
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
⊢ Measure.pi μ = μν
[PROOFSTEP]
have h4C : ∀ (i) (s : Set (α i)), s ∈ C i → MeasurableSet s := by intro i s hs; rw [← hC];
  exact measurableSet_generateFrom hs
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
⊢ ∀ (i : ι) (s : Set (α i)), s ∈ C i → MeasurableSet s
[PROOFSTEP]
intro i s hs
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
i : ι
s : Set (α i)
hs : s ∈ C i
⊢ MeasurableSet s
[PROOFSTEP]
rw [← hC]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
i : ι
s : Set (α i)
hs : s ∈ C i
⊢ MeasurableSet s
[PROOFSTEP]
exact measurableSet_generateFrom hs
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
h4C : ∀ (i : ι) (s : Set (α i)), s ∈ C i → MeasurableSet s
⊢ Measure.pi μ = μν
[PROOFSTEP]
refine'
  (FiniteSpanningSetsIn.pi h3C).ext (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm
    (IsPiSystem.pi h2C) _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
h4C : ∀ (i : ι) (s : Set (α i)), s ∈ C i → MeasurableSet s
⊢ ∀ (s : Set ((i : ι) → α i)), (s ∈ Set.pi univ '' Set.pi univ fun i => C i) → ↑↑(Measure.pi μ) s = ↑↑μν s
[PROOFSTEP]
rintro _ ⟨s, hs, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
h4C : ∀ (i : ι) (s : Set (α i)), s ∈ C i → MeasurableSet s
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ fun i => C i
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) = ↑↑μν (Set.pi univ s)
[PROOFSTEP]
rw [mem_univ_pi] at hs
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
h4C : ∀ (i : ι) (s : Set (α i)), s ∈ C i → MeasurableSet s
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), s i ∈ C i
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) = ↑↑μν (Set.pi univ s)
[PROOFSTEP]
haveI := fun i => (h3C i).sigmaFinite
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → FiniteSpanningSetsIn (μ i) (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
h4C : ∀ (i : ι) (s : Set (α i)), s ∈ C i → MeasurableSet s
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), s i ∈ C i
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) = ↑↑μν (Set.pi univ s)
[PROOFSTEP]
simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs i)]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
haveI : Encodable ι := Fintype.toEncodable ι
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
this : Encodable ι
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [← pi'_eq_pi, pi'_pi]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ ↑↑(Measure.pi μ) univ = ∏ i : ι, ↑↑(μ i) univ
[PROOFSTEP]
rw [← pi_univ, pi_pi μ]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ ↑↑(Measure.pi μ) (Metric.ball x r) = ∏ i : ι, ↑↑(μ i) (Metric.ball (x i) r)
[PROOFSTEP]
rw [ball_pi _ hr, pi_pi]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ ↑↑(Measure.pi μ) (Metric.closedBall x r) = ∏ i : ι, ↑↑(μ i) (Metric.closedBall (x i) r)
[PROOFSTEP]
rw [closedBall_pi _ hr, pi_pi]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝³ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
inst✝² : (i : ι) → MeasurableSpace (α✝ i)
μ✝ : (i : ι) → Measure (α✝ i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ✝ i)
α : Type u_4
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
⊢ Measure.pi μ = dirac x
[PROOFSTEP]
haveI : ∀ a, SigmaFinite (μ a) := isEmptyElim
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝³ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
inst✝² : (i : ι) → MeasurableSpace (α✝ i)
μ✝ : (i : ι) → Measure (α✝ i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ✝ i)
α : Type u_4
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
⊢ Measure.pi μ = dirac x
[PROOFSTEP]
refine' pi_eq fun s _ => _
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝³ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
inst✝² : (i : ι) → MeasurableSpace (α✝ i)
μ✝ : (i : ι) → Measure (α✝ i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ✝ i)
α : Type u_4
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ ↑↑(dirac x) (Set.pi univ s) = ∏ i : α, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [Fintype.prod_empty, dirac_apply_of_mem]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝³ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
inst✝² : (i : ι) → MeasurableSpace (α✝ i)
μ✝ : (i : ι) → Measure (α✝ i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ✝ i)
α : Type u_4
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : optParam ((a : α) → β a) fun a => isEmptyElim a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ x ∈ Set.pi univ s
[PROOFSTEP]
exact isEmptyElim (α := α)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0
[PROOFSTEP]
rcases exists_measurable_superset_of_null hs with ⟨t, hst, _, hμt⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0
[PROOFSTEP]
suffices : Measure.pi μ (eval i ⁻¹' t) = 0
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
this : ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' s) = 0
case this
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
[PROOFSTEP]
exact measure_mono_null (preimage_mono hst) this
[GOAL]
case this
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : ↑↑(μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
[PROOFSTEP]
clear! s
[GOAL]
case this
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(Measure.pi μ) (eval i ⁻¹' t) = 0
[PROOFSTEP]
rw [← univ_pi_update_univ, pi_pi]
[GOAL]
case this
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ∏ i_1 : ι, ↑↑(μ i_1) (update (fun j => univ) i t i_1) = 0
[PROOFSTEP]
apply Finset.prod_eq_zero (Finset.mem_univ i)
[GOAL]
case this
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
t : Set (α i)
left✝ : MeasurableSet t
hμt : ↑↑(μ i) t = 0
⊢ ↑↑(μ i) (update (fun j => univ) i t i) = 0
[PROOFSTEP]
simp [hμt]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (Set.pi univ fun i => Iio (f i)) =ᶠ[ae (Measure.pi μ)] Iic f
[PROOFSTEP]
rw [← pi_univ_Iic]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (Set.pi univ fun i => Iio (f i)) =ᶠ[ae (Measure.pi μ)] Set.pi univ fun i => Iic (f i)
[PROOFSTEP]
exact pi_Iio_ae_eq_pi_Iic
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (Set.pi univ fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] Ici f
[PROOFSTEP]
rw [← pi_univ_Ici]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (Set.pi univ fun i => Ioi (f i)) =ᶠ[ae (Measure.pi μ)] Set.pi univ fun i => Ici (f i)
[PROOFSTEP]
exact pi_Ioi_ae_eq_pi_Ici
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi univ fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g
[PROOFSTEP]
rw [← pi_univ_Icc]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi univ fun i => Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Set.pi univ fun i => Icc (f i) (g i)
[PROOFSTEP]
exact pi_Ioo_ae_eq_pi_Icc
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi univ fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g
[PROOFSTEP]
rw [← pi_univ_Icc]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi univ fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Set.pi univ fun i => Icc (f i) (g i)
[PROOFSTEP]
exact pi_Ioc_ae_eq_pi_Icc
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi univ fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g
[PROOFSTEP]
rw [← pi_univ_Icc]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi univ fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Set.pi univ fun i => Icc (f i) (g i)
[PROOFSTEP]
exact pi_Ico_ae_eq_pi_Icc
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
⊢ IsLocallyFiniteMeasure (Measure.pi μ)
[PROOFSTEP]
refine' ⟨fun x => _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
⊢ FiniteAtFilter (Measure.pi μ) (𝓝 x)
[PROOFSTEP]
choose s hxs ho hμ using fun i => (μ i).exists_isOpen_measure_lt_top (x i)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
s : (i : ι) → Set (α i)
hxs : ∀ (i : ι), x i ∈ s i
ho : ∀ (i : ι), IsOpen (s i)
hμ : ∀ (i : ι), ↑↑(μ i) (s i) < ⊤
⊢ FiniteAtFilter (Measure.pi μ) (𝓝 x)
[PROOFSTEP]
refine' ⟨pi univ s, set_pi_mem_nhds finite_univ fun i _ => IsOpen.mem_nhds (ho i) (hxs i), _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
s : (i : ι) → Set (α i)
hxs : ∀ (i : ι), x i ∈ s i
ho : ∀ (i : ι), IsOpen (s i)
hμ : ∀ (i : ι), ↑↑(μ i) (s i) < ⊤
⊢ ↑↑(Measure.pi μ) (Set.pi univ s) < ⊤
[PROOFSTEP]
rw [pi_pi]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
s : (i : ι) → Set (α i)
hxs : ∀ (i : ι), x i ∈ s i
ho : ∀ (i : ι), IsOpen (s i)
hμ : ∀ (i : ι), ↑↑(μ i) (s i) < ⊤
⊢ ∏ i : ι, ↑↑(μ i) (s i) < ⊤
[PROOFSTEP]
exact ENNReal.prod_lt_top fun i _ => (hμ i).ne
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulLeftInvariant (μ i)
⊢ IsMulLeftInvariant (Measure.pi μ)
[PROOFSTEP]
refine' ⟨fun v => (pi_eq fun s hs => _).symm⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulLeftInvariant (μ i)
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(map (fun x => v * x) (Measure.pi μ)) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [map_apply (measurable_const_mul _) (MeasurableSet.univ_pi hs),
  show (· * ·) v ⁻¹' univ.pi s = univ.pi fun i => (· * ·) (v i) ⁻¹' s i by rfl, pi_pi]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulLeftInvariant (μ i)
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun x x_1 => x * x_1) v ⁻¹' Set.pi univ s = Set.pi univ fun i => (fun x x_1 => x * x_1) (v i) ⁻¹' s i
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulLeftInvariant (μ i)
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i : ι, ↑↑(μ i) ((fun x x_1 => x * x_1) (v i) ⁻¹' s i) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
simp_rw [measure_preimage_mul]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulRightInvariant (μ i)
⊢ IsMulRightInvariant (Measure.pi μ)
[PROOFSTEP]
refine' ⟨fun v => (pi_eq fun s hs => _).symm⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulRightInvariant (μ i)
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(map (fun x => x * v) (Measure.pi μ)) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [map_apply (measurable_mul_const _) (MeasurableSet.univ_pi hs),
  show (· * v) ⁻¹' univ.pi s = univ.pi fun i => (· * v i) ⁻¹' s i by rfl, pi_pi]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulRightInvariant (μ i)
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun x => x * v) ⁻¹' Set.pi univ s = Set.pi univ fun i => (fun x => x * v i) ⁻¹' s i
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), IsMulRightInvariant (μ i)
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i : ι, ↑↑(μ i) ((fun x => x * v i) ⁻¹' s i) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
simp_rw [measure_preimage_mul_right]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), IsInvInvariant (μ i)
⊢ IsInvInvariant (Measure.pi μ)
[PROOFSTEP]
refine' ⟨(Measure.pi_eq fun s hs => _).symm⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), IsInvInvariant (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(Measure.inv (Measure.pi μ)) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
have A : Inv.inv ⁻¹' pi univ s = Set.pi univ fun i => Inv.inv ⁻¹' s i := by ext; simp
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), IsInvInvariant (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Inv.inv ⁻¹' Set.pi univ s = Set.pi univ fun i => Inv.inv ⁻¹' s i
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), IsInvInvariant (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ Inv.inv ⁻¹' Set.pi univ s ↔ x✝ ∈ Set.pi univ fun i => Inv.inv ⁻¹' s i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), IsInvInvariant (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
A : Inv.inv ⁻¹' Set.pi univ s = Set.pi univ fun i => Inv.inv ⁻¹' s i
⊢ ↑↑(Measure.inv (Measure.pi μ)) (Set.pi univ s) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi, measure_preimage_inv]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
⊢ IsOpenPosMeasure (Measure.pi μ)
[PROOFSTEP]
constructor
[GOAL]
case open_pos
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
⊢ ∀ (U : Set ((i : ι) → α i)), IsOpen U → Set.Nonempty U → ↑↑(Measure.pi μ) U ≠ 0
[PROOFSTEP]
rintro U U_open ⟨a, ha⟩
[GOAL]
case open_pos.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
U : Set ((i : ι) → α i)
U_open : IsOpen U
a : (i : ι) → α i
ha : a ∈ U
⊢ ↑↑(Measure.pi μ) U ≠ 0
[PROOFSTEP]
obtain ⟨s, ⟨hs, hsU⟩⟩ := isOpen_pi_iff'.1 U_open a ha
[GOAL]
case open_pos.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
U : Set ((i : ι) → α i)
U_open : IsOpen U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi univ s ⊆ U
⊢ ↑↑(Measure.pi μ) U ≠ 0
[PROOFSTEP]
refine' ne_of_gt (lt_of_lt_of_le _ (measure_mono hsU))
[GOAL]
case open_pos.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
U : Set ((i : ι) → α i)
U_open : IsOpen U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi univ s ⊆ U
⊢ 0 < ↑↑(Measure.pi μ) (Set.pi univ s)
[PROOFSTEP]
simp only [pi_pi]
[GOAL]
case open_pos.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
U : Set ((i : ι) → α i)
U_open : IsOpen U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi univ s ⊆ U
⊢ 0 < ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [CanonicallyOrderedCommSemiring.prod_pos]
[GOAL]
case open_pos.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
U : Set ((i : ι) → α i)
U_open : IsOpen U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi univ s ⊆ U
⊢ ∀ (i : ι), i ∈ Finset.univ → 0 < ↑↑(μ i) (s i)
[PROOFSTEP]
intro i _
[GOAL]
case open_pos.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsOpenPosMeasure (μ i)
U : Set ((i : ι) → α i)
U_open : IsOpen U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi univ s ⊆ U
i : ι
a✝ : i ∈ Finset.univ
⊢ 0 < ↑↑(μ i) (s i)
[PROOFSTEP]
apply (hs i).1.measure_pos (μ i) ⟨a i, (hs i).2⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
⊢ IsFiniteMeasureOnCompacts (Measure.pi μ)
[PROOFSTEP]
constructor
[GOAL]
case lt_top_of_isCompact
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
⊢ ∀ ⦃K : Set ((i : ι) → α i)⦄, IsCompact K → ↑↑(Measure.pi μ) K < ⊤
[PROOFSTEP]
intro K hK
[GOAL]
case lt_top_of_isCompact
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ↑↑(Measure.pi μ) K < ⊤
[PROOFSTEP]
suffices Measure.pi μ (Set.univ.pi fun j => Function.eval j '' K) < ⊤ by
  exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
this : ↑↑(Measure.pi μ) (Set.pi univ fun j => eval j '' K) < ⊤
⊢ ↑↑(Measure.pi μ) K < ⊤
[PROOFSTEP]
exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this
[GOAL]
case lt_top_of_isCompact
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ↑↑(Measure.pi μ) (Set.pi univ fun j => eval j '' K) < ⊤
[PROOFSTEP]
rw [Measure.pi_pi]
[GOAL]
case lt_top_of_isCompact
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ∏ i : ι, ↑↑(μ i) (eval i '' K) < ⊤
[PROOFSTEP]
refine' WithTop.prod_lt_top _
[GOAL]
case lt_top_of_isCompact
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ∀ (i : ι), i ∈ Finset.univ → ↑↑(μ i) (eval i '' K) ≠ ⊤
[PROOFSTEP]
exact fun i _ => ne_of_lt (IsCompact.measure_lt_top (IsCompact.image hK (continuous_apply i)))
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝³ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
⊢ MeasurePreserving ↑(MeasurableEquiv.piEquivPiSubtypeProd α p)
[PROOFSTEP]
set e := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝³ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
⊢ MeasurePreserving ↑(MeasurableEquiv.piEquivPiSubtypeProd α p)
[PROOFSTEP]
refine' MeasurePreserving.symm e _
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝³ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
⊢ MeasurePreserving ↑e
[PROOFSTEP]
refine' ⟨e.measurable, (pi_eq fun s _ => _).symm⟩
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝³ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ ↑↑(Measure.map (↑e) (Measure.prod (Measure.pi fun i => μ ↑i) (Measure.pi fun i => μ ↑i))) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
have : e ⁻¹' pi univ s = (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i :=
  Equiv.preimage_piEquivPiSubtypeProd_symm_pi p s
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝³ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
this : ↑e ⁻¹' Set.pi univ s = (Set.pi univ fun i => s ↑i) ×ˢ Set.pi univ fun i => s ↑i
⊢ ↑↑(Measure.map (↑e) (Measure.prod (Measure.pi fun i => μ ↑i) (Measure.pi fun i => μ ↑i))) (Set.pi univ s) =
    ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
rw [e.map_apply, this, prod_prod, pi_pi, pi_pi]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝³ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst✝ : DecidablePred p
e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
this : ↑e ⁻¹' Set.pi univ s = (Set.pi univ fun i => s ↑i) ×ˢ Set.pi univ fun i => s ↑i
⊢ (∏ i : Subtype p, ↑↑(μ ↑i) (s ↑i)) * ∏ i : { i // ¬p i }, ↑↑(μ ↑i) (s ↑i) = ∏ i : ι, ↑↑(μ i) (s i)
[PROOFSTEP]
exact Fintype.prod_subtype_mul_prod_subtype p fun i => μ i (s i)
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinSuccAboveEquiv α i)
[PROOFSTEP]
set e := (MeasurableEquiv.piFinSuccAboveEquiv α i).symm
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (Fin.succAbove i j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinSuccAboveEquiv α i)
[PROOFSTEP]
refine' MeasurePreserving.symm e _
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (Fin.succAbove i j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
⊢ MeasurePreserving ↑e
[PROOFSTEP]
refine' ⟨e.measurable, (pi_eq fun s _ => _).symm⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (Fin.succAbove i j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ↑↑(Measure.map (↑e) (Measure.prod (μ i) (Measure.pi fun j => μ (Fin.succAbove i j)))) (Set.pi univ s) =
    ∏ i : Fin (n + 1), ↑↑(μ i) (s i)
[PROOFSTEP]
rw [e.map_apply, i.prod_univ_succAbove _, ← pi_pi, ← prod_prod]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (Fin.succAbove i j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ↑↑(Measure.prod (μ i) (Measure.pi fun j => μ (Fin.succAbove i j))) (↑e ⁻¹' Set.pi univ s) =
    ↑↑(Measure.prod (μ i) (Measure.pi fun i_1 => μ (Fin.succAbove i i_1)))
      (s i ×ˢ Set.pi univ fun i_1 => s (Fin.succAbove i i_1))
[PROOFSTEP]
congr 1 with ⟨x, f⟩
[GOAL]
case e_a.h.mk
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (Fin.succAbove i j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAboveEquiv α i)
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
x : α i
f : (j : Fin n) → α (Fin.succAbove i j)
⊢ (x, f) ∈ ↑e ⁻¹' Set.pi univ s ↔ (x, f) ∈ s i ×ˢ Set.pi univ fun i_1 => s (Fin.succAbove i i_1)
[PROOFSTEP]
simp [i.forall_iff_succAbove]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
⊢ MeasurePreserving ↑(MeasurableEquiv.funUnique α β)
[PROOFSTEP]
set e := MeasurableEquiv.funUnique α β
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
⊢ MeasurePreserving ↑e
[PROOFSTEP]
have : (piPremeasure fun _ : α => μ.toOuterMeasure) = Measure.map e.symm μ :=
  by
  ext1 s
  rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply]
  congr 1; exact e.toEquiv.image_eq_preimage s
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
⊢ (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
[PROOFSTEP]
ext1 s
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ piPremeasure (fun x => ↑μ) s = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ) s
[PROOFSTEP]
rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ ↑↑μ (eval default '' s) = ↑↑μ (↑(MeasurableEquiv.symm e) ⁻¹' s)
[PROOFSTEP]
congr 1
[GOAL]
case h.e_a
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
s : Set (α → β)
⊢ eval default '' s = ↑(MeasurableEquiv.symm e) ⁻¹' s
[PROOFSTEP]
exact e.toEquiv.image_eq_preimage s
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
this : (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
⊢ MeasurePreserving ↑e
[PROOFSTEP]
simp only [Measure.pi, OuterMeasure.pi, this, boundedBy_measure, toOuterMeasure_toMeasure]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
β : Type u
m : MeasurableSpace β
μ : Measure β
α : Type v
inst✝ : Unique α
e : (α → β) ≃ᵐ β := MeasurableEquiv.funUnique α β
this : (piPremeasure fun x => ↑μ) = ↑↑(Measure.map (↑(MeasurableEquiv.symm e)) μ)
⊢ MeasurePreserving ↑(MeasurableEquiv.funUnique α β)
[PROOFSTEP]
exact (e.symm.measurable.measurePreserving _).symm e.symm
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
⊢ MeasurePreserving ↑(MeasurableEquiv.piFinTwo α)
[PROOFSTEP]
refine' ⟨MeasurableEquiv.measurable _, (Measure.prod_eq fun s t _ _ => _).symm⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(Measure.map (↑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = ↑↑(μ 0) s * ↑↑(μ 1) t
[PROOFSTEP]
rw [MeasurableEquiv.map_apply, MeasurableEquiv.piFinTwo_apply, Fin.preimage_apply_01_prod, Measure.pi_pi,
  Fin.prod_univ_two]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
s : Set (α 0)
t : Set (α 1)
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * ↑↑(μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) =
    ↑↑(μ 0) s * ↑↑(μ 1) t
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : ι → Type u_3
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Type u
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ MeasurePreserving ↑MeasurableEquiv.finTwoArrow
[PROOFSTEP]
simpa only [Matrix.vec_single_eq_const, Matrix.vecCons_const] using measurePreserving_finTwoArrow_vec μ μ
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurePreserving ↑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)
[PROOFSTEP]
set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving ↑e
[PROOFSTEP]
refine' ⟨e.measurable, _⟩
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : ι✝ → Type u_3
inst✝¹ : Fintype ι✝
m✝ : (i : ι✝) → OuterMeasure (α✝ i)
ι : Type u
α : ι → Type v
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Measure.map (↑e) (Measure.pi μ) = Measure.dirac ()
[PROOFSTEP]
rw [Measure.pi_of_empty, Measure.map_dirac e.measurable]