Theorem: ProbabilityTheory.IsBernoulliSeq.aemeasurable (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 μ
a : α
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
classical
have : (PMF.bernoulli' p hX.le_one).toMeasure ≠ 0 := NeZero.ne _
rw [← hX.map a, Measure.map] at this
refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this
rw [Measure.mapₗ_ne_zero_iff hX'.measurable_mk]
haveI : Nonempty α := ⟨a⟩
exact hX.ne_zero
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 μ
a : α
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
have : (PMF.bernoulli' p hX.le_one).toMeasure ≠ 0 := NeZero.ne _
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 μ
a : α
this : (PMF.bernoulli' p ⋯).toMeasure ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ

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 μ
a : α
this : (PMF.bernoulli' p ⋯).toMeasure ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
rw [← hX.map a, Measure.map] at this
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 μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ

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 μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
Tactic:
refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this
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 μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hX')) μ ≠ 0

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 μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hX')) μ ≠ 0
Tactic:
rw [Measure.mapₗ_ne_zero_iff hX'.measurable_mk]
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 μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ μ ≠ 0

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 μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ μ ≠ 0
Tactic:
haveI : Nonempty α := ⟨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 μ
a : α
this✝ :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
this : Nonempty α
⊢ μ ≠ 0

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 μ
a : α
this✝ :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
this : Nonempty α
⊢ μ ≠ 0
Tactic:
exact hX.ne_zero
State after:
no goals