Theorem: ProbabilityTheory.IsBernoulliSeq.meas (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 μ
inst✝ : Fintype α
s : Finset α
⊢ μ {ω | {a | a ∈ X ω} = ↑s} = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)
Tactic:
simp_rw [ext_iff, setOf_forall]
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 μ
inst✝ : Fintype α
s : Finset α
⊢ μ (⋂ i, {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}) = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)

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 μ
inst✝ : Fintype α
s : Finset α
⊢ μ (⋂ i, {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}) = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)
Tactic:
rw [hX.iIndepFun.meas_iInter, ← s.prod_mul_prod_compl, Finset.prod_eq_pow_card,
  Finset.prod_eq_pow_card, Finset.card_compl]
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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ sᶜ, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p

α : 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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ s, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p

α : 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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ (i : α), MeasurableSet {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}

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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ (i : α), MeasurableSet {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}
Tactic:
rintro a
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 μ
inst✝ : Fintype α
s : Finset α
a : α
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}

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 μ
inst✝ : Fintype α
s : Finset α
a : α
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Tactic:
by_cases a ∈ s
State after:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}

case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}

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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ sᶜ, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Tactic:
rintro a hi
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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ sᶜ
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p

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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ sᶜ
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Tactic:
rw [Finset.mem_compl] at hi
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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∉ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p

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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∉ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
Tactic:
simp only [hi, ← compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe,
  iff_false_iff, hX.nullMeasurableSet, hX.meas_apply]
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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ s, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p
Tactic:
rintro a hi
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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p

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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p
Tactic:
simp only [hi, mem_setOf_eq, Finset.mem_coe, iff_true_iff, hX.meas_apply]
State after:
no goals

State before:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Tactic:
simp only [mem_setOf_eq, Finset.mem_coe, iff_true_iff, *]
State after:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ X x}

State before:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ X x}
Tactic:
exact ⟨{True}, trivial, by ext; simp⟩
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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ (fun ω => a ∈ X ω) ⁻¹' {True} = {x | a ∈ X x}
Tactic:
ext
State after:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {True} ↔ x✝ ∈ {x | a ∈ X x}

State before:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {True} ↔ x✝ ∈ {x | a ∈ X x}
Tactic:
simp
State after:
no goals

State before:
case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Tactic:
simp only [mem_setOf_eq, Finset.mem_coe, iff_false_iff, *]
State after:
case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∉ X x}

State before:
case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∉ X x}
Tactic:
exact ⟨{False}, trivial, by ext; simp⟩
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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ (fun ω => a ∈ X ω) ⁻¹' {False} = {x | a ∉ X x}
Tactic:
ext
State after:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {False} ↔ x✝ ∈ {x | a ∉ X x}

State before:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {False} ↔ x✝ ∈ {x | a ∉ X x}
Tactic:
simp
State after:
no goals