Theorem: ProbabilityTheory.IsBernoulliSeq.compl (LeanCamCombi/BernoulliSeq.lean)

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
⊢ iIndepFun inferInstance (fun a ω => a ∈ (X ω)ᶜ) μ
Tactic:
simp only [iIndepFun_iff, mem_compl_iff, MeasurableSpace.comap_not]
State after:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
⊢ ∀ (s : Finset α) {f' : α → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
⊢ ∀ (s : Finset α) {f' : α → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
Tactic:
exact (iIndepFun_iff _ _ _).1 hX.iIndepFun
State after:
no goals

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
a : α
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Tactic:
have : Measurable Not := fun _ _ ↦ trivial
State after:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
a : α
this : Measurable Not
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
a : α
this : Measurable Not
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Tactic:
refine' (this.aemeasurable.map_map_of_aemeasurable (hX.aemeasurable _)).symm.trans _
State after:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
a : α
this : Measurable Not
⊢ Measure.map Not (Measure.map (fun ω => a ∈ X ω) μ) = (PMF.bernoulli' (1 - p) ⋯).toMeasure

State before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
a : α
this : Measurable Not
⊢ Measure.map Not (Measure.map (fun ω => a ∈ X ω) μ) = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Tactic:
rw [hX.map, PMF.map_toMeasure _ this, PMF.map_not_bernoulli']
State after:
no goals