[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : IndepSet t t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
rw [IndepSet_iff] at h_indep
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
specialize
  h_indep t t (measurableSet_generateFrom (Set.mem_singleton t)) (measurableSet_generateFrom (Set.mem_singleton t))
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
by_cases h0 : μ t = 0
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
exact Or.inl h0
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
by_cases h_top : μ t = ∞
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
exact Or.inr (Or.inr h_top)
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
rw [← one_mul (μ (t ∩ t)), Set.inter_self, ENNReal.mul_eq_mul_right h0 h_top] at h_indep
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : 1 = ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
[PROOFSTEP]
exact Or.inr (Or.inl h_indep.symm)
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
[PROOFSTEP]
have h_0_1_top := measure_eq_zero_or_one_or_top_of_indepSet_self h_indep
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t
h_0_1_top : ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1
[PROOFSTEP]
simpa [measure_ne_top μ] using h_0_1_top
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ Indep (⨆ (n : ι) (_ : n ∈ t), s n) (limsup s f)
[PROOFSTEP]
refine' indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ limsup s f ≤ ⨆ (n : ι) (_ : n ∈ tᶜ), s n
[PROOFSTEP]
refine' limsSup_le_of_le (by isBoundedDefault) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map s f)
[PROOFSTEP]
isBoundedDefault
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ ∀ᶠ (n : MeasurableSpace Ω) in map s f, n ≤ ⨆ (n : ι) (_ : n ∈ tᶜ), s n
[PROOFSTEP]
simp only [Set.mem_compl_iff, eventually_map]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ ∀ᶠ (a : ι) in f, s a ≤ ⨆ (n : ι) (_ : ¬n ∈ t), s n
[PROOFSTEP]
exact eventually_of_mem (hf t ht) le_iSup₂
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ Indep (⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n) (limsup s f)
[PROOFSTEP]
refine' indep_iSup_of_directed_le _ _ _ _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ ∀ (i : α), Indep (⨆ (n : ι) (_ : n ∈ ns i), s n) (limsup s f)
[PROOFSTEP]
exact fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ ∀ (i : α), ⨆ (n : ι) (_ : n ∈ ns i), s n ≤ m0
[PROOFSTEP]
exact fun a => iSup₂_le fun n _ => h_le n
[GOAL]
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ limsup s f ≤ m0
[PROOFSTEP]
exact limsup_le_iSup.trans (iSup_le h_le)
[GOAL]
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n
[PROOFSTEP]
intro a b
[GOAL]
case refine'_4
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b : α
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z)
[PROOFSTEP]
obtain ⟨c, hc⟩ := hns a b
[GOAL]
case refine'_4.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) z)
[PROOFSTEP]
refine' ⟨c, _, _⟩
[GOAL]
case refine'_4.intro.refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
⊢ (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) a) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) c)
[PROOFSTEP]
refine' iSup_mono fun n => iSup_mono' fun hn => ⟨_, le_rfl⟩
[GOAL]
case refine'_4.intro.refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
⊢ (fun x x_1 => x ≤ x_1) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) b) ((fun a => ⨆ (n : ι) (_ : n ∈ ns a), s n) c)
[PROOFSTEP]
refine' iSup_mono fun n => iSup_mono' fun hn => ⟨_, le_rfl⟩
[GOAL]
case refine'_4.intro.refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
n : ι
hn : n ∈ ns a
⊢ n ∈ ns c
[PROOFSTEP]
exact hc.1 hn
[GOAL]
case refine'_4.intro.refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
a b c : α
hc : (fun x x_1 => x ≤ x_1) (ns a) (ns c) ∧ (fun x x_1 => x ≤ x_1) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c
[PROOFSTEP]
exact hc.2 hn
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ Indep (⨆ (n : ι), s n) (limsup s f)
[PROOFSTEP]
suffices (⨆ a, ⨆ n ∈ ns a, s n) = ⨆ n, s n by
  rw [← this]
  exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
this : ⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n = ⨆ (n : ι), s n
⊢ Indep (⨆ (n : ι), s n) (limsup s f)
[PROOFSTEP]
rw [← this]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
this : ⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n = ⨆ (n : ι), s n
⊢ Indep (⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n) (limsup s f)
[PROOFSTEP]
exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ ⨆ (a : α) (n : ι) (_ : n ∈ ns a), s n = ⨆ (n : ι), s n
[PROOFSTEP]
rw [iSup_comm]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ ⨆ (j : ι) (i : α) (_ : j ∈ ns i), s j = ⨆ (n : ι), s n
[PROOFSTEP]
refine' iSup_congr fun n => _
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = s n
[PROOFSTEP]
have h : ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ _ : ∃ i, n ∈ ns i, s n := by rw [iSup_exists]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
[PROOFSTEP]
rw [iSup_exists]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
h : ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = s n
[PROOFSTEP]
haveI : Nonempty (∃ i : α, n ∈ ns i) := ⟨hns_univ n⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
α : Type u_3
p : Set ι → Prop
f : Filter ι
ns : α → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x x_1 => x ≤ x_1) ns
hnsp : ∀ (a : α), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
h : ⨆ (i : α) (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
this : Nonempty (∃ i, n ∈ ns i)
⊢ ⨆ (i : α) (_ : n ∈ ns i), s n = s n
[PROOFSTEP]
rw [h, iSup_const]
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
⊢ Indep (limsup s atTop) (limsup s atTop)
[PROOFSTEP]
let ns : ι → Set ι := Set.Iic
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
⊢ Indep (limsup s atTop) (limsup s atTop)
[PROOFSTEP]
have hnsp : ∀ i, BddAbove (ns i) := fun i => bddAbove_Iic
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Indep (limsup s atTop) (limsup s atTop)
[PROOFSTEP]
refine' indep_limsup_self h_le h_indep _ _ hnsp _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop
[PROOFSTEP]
simp only [mem_atTop_sets, ge_iff_le, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}) → ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
[PROOFSTEP]
rintro t ⟨a, ha⟩
[GOAL]
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b, a < b := exists_gt a
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
⊢ ∃ a, ∀ (b : ι), a ≤ b → ¬b ∈ t
[PROOFSTEP]
refine' ⟨b, fun c hc hct => _⟩
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ False
[PROOFSTEP]
suffices : ∀ i ∈ t, i < c
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → i < c
⊢ False
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
[PROOFSTEP]
exact lt_irrefl c (this c hct)
[GOAL]
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → i < c
[PROOFSTEP]
exact fun i hi => (ha hi).trans_lt (hb.trans_le hc)
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a
[PROOFSTEP]
exact Monotone.directed_le fun i j hij k hki => le_trans hki hij
[GOAL]
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
[PROOFSTEP]
exact fun n => ⟨n, le_rfl⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
⊢ Indep (limsup s atBot) (limsup s atBot)
[PROOFSTEP]
let ns : ι → Set ι := Set.Ici
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
⊢ Indep (limsup s atBot) (limsup s atBot)
[PROOFSTEP]
have hnsp : ∀ i, BddBelow (ns i) := fun i => bddBelow_Ici
[GOAL]
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Indep (limsup s atBot) (limsup s atBot)
[PROOFSTEP]
refine' indep_limsup_self h_le h_indep _ _ hnsp _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot
[PROOFSTEP]
simp only [mem_atBot_sets, ge_iff_le, Set.mem_compl_iff, BddBelow, lowerBounds, Set.Nonempty]
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}) → ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
[PROOFSTEP]
rintro t ⟨a, ha⟩
[GOAL]
case refine'_1.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
⊢ ∃ a, ∀ (b : ι), b ≤ a → ¬b ∈ t
[PROOFSTEP]
refine' ⟨b, fun c hc hct => _⟩
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ False
[PROOFSTEP]
suffices : ∀ i ∈ t, c < i
[GOAL]
case refine'_1.intro.intro
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
this : ∀ (i : ι), i ∈ t → c < i
⊢ False
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
[PROOFSTEP]
exact lt_irrefl c (this c hct)
[GOAL]
case this
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
c : ι
hc : c ≤ b
hct : c ∈ t
⊢ ∀ (i : ι), i ∈ t → c < i
[PROOFSTEP]
exact fun i hi => hc.trans_lt (hb.trans_le (ha hi))
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun a => ns a
[PROOFSTEP]
exact directed_of_inf fun i j hij k hki => hij.trans hki
[GOAL]
case refine'_3
Ω : Type u_1
ι : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
s : ι → MeasurableSpace Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
[PROOFSTEP]
exact fun n => ⟨n, le_rfl⟩


[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁷ : TopologicalSpace Ω
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : PolishSpace Ω
inst✝⁴ : BorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
inst✝ : MeasurableSpace β
⊢ IsMarkovKernel (condDistrib Y X μ)
[PROOFSTEP]
rw [condDistrib]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁷ : TopologicalSpace Ω
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : PolishSpace Ω
inst✝⁴ : BorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
inst✝ : MeasurableSpace β
⊢ IsMarkovKernel (Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ ((∀ᵐ (a : β) ∂Measure.map X μ, Integrable fun ω => f (a, ω)) ∧
      Integrable fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂↑(condDistrib Y X μ) a) ↔
    Integrable f
[PROOFSTEP]
rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prod_mk₀ hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂↑(condDistrib Y X μ) x) (Measure.map X μ)
[PROOFSTEP]
rw [← Measure.fst_map_prod_mk₀ hY, condDistrib]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂↑(Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ)) x)
    (Measure.fst (Measure.map (fun a => (X a, Y a)) μ))
[PROOFSTEP]
exact hf.integral_condKernel
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ Integrable fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)
[PROOFSTEP]
refine' integrable_toReal_of_lintegral_ne_top _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ AEMeasurable fun a => ↑↑(↑(condDistrib Y X μ) (X a)) s
[PROOFSTEP]
exact Measurable.comp_aemeasurable (kernel.measurable_coe _ hs) hX
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ↑↑(↑(condDistrib Y X μ) (X x)) s ∂μ ≠ ⊤
[PROOFSTEP]
refine' ne_of_lt _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : AEMeasurable X
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ↑↑(↑(condDistrib Y X μ) (X x)) s ∂μ < ⊤
[PROOFSTEP]
calc
  ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
  _ = μ univ := lintegral_one
  _ < ∞ := measure_lt_top _ _
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ ∀ᵐ (b : β) ∂Measure.map X μ, Integrable fun ω => f (b, ω)
[PROOFSTEP]
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ ∀ᵐ (b : β) ∂Measure.fst (Measure.map (fun a => (X a, Y a)) μ), Integrable fun ω => f (b, ω)
[PROOFSTEP]
exact hf_int.condKernel_ae
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂↑(condDistrib Y X μ) x
[PROOFSTEP]
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂↑(Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ)) x
[PROOFSTEP]
exact hf_int.integral_norm_condKernel
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ‖∫ (y : Ω), f (x, y) ∂↑(condDistrib Y X μ) x‖
[PROOFSTEP]
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hY : AEMeasurable Y
hf_int : Integrable f
⊢ Integrable fun x => ‖∫ (y : Ω), f (x, y) ∂↑(Measure.condKernel (Measure.map (fun a => (X a, Y a)) μ)) x‖
[PROOFSTEP]
exact hf_int.norm_integral_condKernel
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (X ⁻¹' t ∩ Y ⁻¹' s)
[PROOFSTEP]
conv_lhs => arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ
[PROOFSTEP]
arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ
[PROOFSTEP]
arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| ∫⁻ (a : α) in X ⁻¹' t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ
[PROOFSTEP]
arg 2
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
| fun a => ↑↑(↑(condDistrib Y X μ) (X a)) s
[PROOFSTEP]
change (fun a => ((condDistrib Y X μ) a) s) ∘ X
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
ht : MeasurableSet t
⊢ lintegral (Measure.restrict μ (X ⁻¹' t)) ((fun a => ↑↑(↑(condDistrib Y X μ) a) s) ∘ X) = ↑↑μ (X ⁻¹' t ∩ Y ⁻¹' s)
[PROOFSTEP]
rw [lintegral_comp (kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht, ←
  Measure.fst_map_prod_mk₀ hY, set_lintegral_condKernel_eq_measure_prod _ ht hs,
  Measure.map_apply_of_aemeasurable (hX.aemeasurable.prod_mk hY) (ht.prod hs), mk_preimage_prod]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in t, ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (t ∩ Y ⁻¹' s)
[PROOFSTEP]
obtain ⟨t', ht', rfl⟩ := ht
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : AEMeasurable Y
hs : MeasurableSet s
t' : Set β
ht' : MeasurableSet t'
⊢ ∫⁻ (a : α) in X ⁻¹' t', ↑↑(↑(condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (X ⁻¹' t' ∩ Y ⁻¹' s)
[PROOFSTEP]
rw [set_lintegral_preimage_condDistrib hX hY hs ht']
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ (fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)) =ᵐ[μ]
    μ[indicator (Y ⁻¹' s) fun ω => 1|MeasurableSpace.comap X mβ]
[PROOFSTEP]
refine' ae_eq_condexp_of_forall_set_integral_eq hX.comap_le _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ Integrable (indicator (Y ⁻¹' s) fun ω => 1)
[PROOFSTEP]
exact (integrable_const _).indicator (hY hs)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 → ↑↑μ s_1 < ⊤ → IntegrableOn (fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)) s_1
[PROOFSTEP]
exact fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ →
        ∫ (x : α) in s_1, ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X x)) s) ∂μ =
          ∫ (x : α) in s_1, indicator (Y ⁻¹' s) (fun ω => 1) x ∂μ
[PROOFSTEP]
intro t ht _
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : ↑↑μ t < ⊤
⊢ ∫ (x : α) in t, ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X x)) s) ∂μ =
    ∫ (x : α) in t, indicator (Y ⁻¹' s) (fun ω => 1) x ∂μ
[PROOFSTEP]
rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
    (eventually_of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
  integral_indicator_const _ (hY hs), Measure.restrict_apply (hY hs), smul_eq_mul, mul_one, inter_comm,
  set_lintegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)) μ
[PROOFSTEP]
refine' (Measurable.stronglyMeasurable _).aeStronglyMeasurable'
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PolishSpace Ω
inst✝³ : BorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ Measurable fun a => ENNReal.toReal (↑↑(↑(condDistrib Y X μ) (X a)) s)
[PROOFSTEP]
exact @Measurable.ennreal_toReal _ (mβ.comap X) _ (measurable_condDistrib hs)
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
⊢ μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)
[PROOFSTEP]
have hf_int' : Integrable (fun a => f (X a, Y a)) μ :=
  (integrable_map_measure hf_int.1 (hX.aemeasurable.prod_mk hY)).mp hf_int
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
⊢ μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)
[PROOFSTEP]
refine' (ae_eq_condexp_of_forall_set_integral_eq hX.comap_le hf_int' (fun s _ _ => _) _ _).symm
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s✝ : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ IntegrableOn (fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)) s
[PROOFSTEP]
exact (hf_int.integral_condDistrib hX.aemeasurable hY).integrableOn
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s < ⊤ → ∫ (x : α) in s, ∫ (y : Ω), f (X x, y) ∂↑(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in s, f (X x, Y x) ∂μ
[PROOFSTEP]
rintro s ⟨t, ht, rfl⟩ _
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (x : α) in X ⁻¹' t, ∫ (y : Ω), f (X x, y) ∂↑(condDistrib Y X μ) (X x) ∂μ = ∫ (x : α) in X ⁻¹' t, f (X x, Y x) ∂μ
[PROOFSTEP]
change ∫ a in X ⁻¹' t, ((fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x') ∘ X) a ∂μ = ∫ a in X ⁻¹' t, f (X a, Y a) ∂μ
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (a : α) in X ⁻¹' t, ((fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x') ∘ X) a ∂μ =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (a : α) in X ⁻¹' t, ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
[PROOFSTEP]
rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂↑(condDistrib Y X μ) y ∂Measure.map X (Measure.restrict μ (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x')
    (Measure.map X (Measure.restrict μ (X ⁻¹' t)))
[PROOFSTEP]
swap
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x')
    (Measure.map X (Measure.restrict μ (X ⁻¹' t)))
[PROOFSTEP]
rw [← Measure.restrict_map hX ht]
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ AEStronglyMeasurable (fun x' => ∫ (y : Ω), f (x', y) ∂↑(condDistrib Y X μ) x') (Measure.restrict (Measure.map X μ) t)
[PROOFSTEP]
exact (hf_int.1.integral_condDistrib_map hY).restrict
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t✝ : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
t : Set β
ht : MeasurableSet t
a✝ : ↑↑μ (X ⁻¹' t) < ⊤
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂↑(condDistrib Y X μ) y ∂Measure.map X (Measure.restrict μ (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
[PROOFSTEP]
rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prod_mk₀ hY, condDistrib,
  set_integral_condKernel_univ_right ht hf_int.integrableOn,
  set_integral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prod_mk hY), mk_preimage_prod, preimage_univ,
  inter_univ]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf_int : Integrable f
hf_int' : Integrable fun a => f (X a, Y a)
⊢ AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => ∫ (y : Ω), f (X a, y) ∂↑(condDistrib Y X μ) (X a)) μ
[PROOFSTEP]
exact aestronglyMeasurable'_integral_condDistrib hX.aemeasurable hY hf_int.1
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)
hf_int : Integrable fun a => f (X a, Y a)
⊢ Integrable f
[PROOFSTEP]
rwa [integrable_map_measure hf (hX.aemeasurable.prod_mk hY)]
[GOAL]
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁸ : TopologicalSpace Ω
inst✝⁷ : MeasurableSpace Ω
inst✝⁶ : PolishSpace Ω
inst✝⁵ : BorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y
hf : StronglyMeasurable f
hf_int : Integrable fun a => f (X a, Y a)
⊢ Integrable f
[PROOFSTEP]
rwa [integrable_map_measure hf.aestronglyMeasurable (hX.aemeasurable.prod_mk hY)]
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
[PROOFSTEP]
refine' ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, _⟩
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ (fun x => f x.snd) =ᵐ[Measure.map (fun ω => (X ω, ω)) μ] fun x => AEStronglyMeasurable.mk f hf x.snd
[PROOFSTEP]
suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω => (X ω, ω)) μ
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
h : Measure.QuasiMeasurePreserving Prod.snd
⊢ (fun x => f x.snd) =ᵐ[Measure.map (fun ω => (X ω, ω)) μ] fun x => AEStronglyMeasurable.mk f hf x.snd
[PROOFSTEP]
exact Measure.QuasiMeasurePreserving.ae_eq h hf.ae_eq_mk
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ Measure.QuasiMeasurePreserving Prod.snd
[PROOFSTEP]
refine' ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => _⟩
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(Measure.map Prod.snd (Measure.map (fun ω => (X ω, ω)) μ)) s = 0
[PROOFSTEP]
rw [Measure.map_apply _ hs]
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ Measurable Prod.snd
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ Measurable Prod.snd
[PROOFSTEP]
exact measurable_snd
[GOAL]
case h
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
by_cases hX : AEMeasurable X μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
rw [Measure.map_apply_of_aemeasurable]
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ ↑↑μ ((fun ω => (X ω, ω)) ⁻¹' (Prod.snd ⁻¹' s)) = 0
[PROOFSTEP]
rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id']
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ ↑↑μ s = 0
[PROOFSTEP]
exact hμs
[GOAL]
case pos.hf
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ AEMeasurable fun ω => (X ω, ω)
[PROOFSTEP]
exact hX.prod_mk aemeasurable_id
[GOAL]
case pos.hs
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable X
⊢ MeasurableSet (Prod.snd ⁻¹' s)
[PROOFSTEP]
exact measurable_snd hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : ¬AEMeasurable X
⊢ ↑↑(Measure.map (fun ω => (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
rw [Measure.map_of_not_aemeasurable]
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : ¬AEMeasurable X
⊢ ↑↑0 (Prod.snd ⁻¹' s) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : ¬AEMeasurable X
⊢ ¬AEMeasurable fun ω => (X ω, ω)
[PROOFSTEP]
contrapose! hX
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F✝ : Type u_4
inst✝⁷ : TopologicalSpace Ω✝
inst✝⁶ : MeasurableSpace Ω✝
inst✝⁵ : PolishSpace Ω✝
inst✝⁴ : BorelSpace Ω✝
inst✝³ : Nonempty Ω✝
inst✝² : NormedAddCommGroup F✝
mα : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s✝ : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F✝
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : ↑↑μ s = 0
hX : AEMeasurable fun ω => (X ω, ω)
⊢ AEMeasurable X
[PROOFSTEP]
exact measurable_fst.comp_aemeasurable hX
[GOAL]
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
by_cases hX : AEMeasurable X μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
have hf := hf_int.1.comp_snd_map_prod_mk X (mΩ := mΩ) (mβ := mβ)
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
refine' ⟨hf, _⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ HasFiniteIntegral fun x => f x.snd
[PROOFSTEP]
rw [HasFiniteIntegral, lintegral_map' hf.ennnorm (hX.prod_mk aemeasurable_id)]
[GOAL]
case pos
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable X
hf : AEStronglyMeasurable (fun x => f x.snd) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ↑‖f (X a, a).snd‖₊ ∂μ < ⊤
[PROOFSTEP]
exact hf_int.2
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : ¬AEMeasurable X
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
rw [Measure.map_of_not_aemeasurable]
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : ¬AEMeasurable X
⊢ Integrable fun x => f x.snd
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : ¬AEMeasurable X
⊢ ¬AEMeasurable fun ω => (X ω, ω)
[PROOFSTEP]
contrapose! hX
[GOAL]
case neg
α : Type u_1
β : Type u_2
Ω✝ : Type u_3
F : Type u_4
inst✝⁶ : TopologicalSpace Ω✝
inst✝⁵ : MeasurableSpace Ω✝
inst✝⁴ : PolishSpace Ω✝
inst✝³ : BorelSpace Ω✝
inst✝² : Nonempty Ω✝
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ✝ : Measure α
inst✝ : IsFiniteMeasure μ✝
X✝ : α → β
Y : α → Ω✝
mβ : MeasurableSpace β
s : Set Ω✝
t : Set β
f✝ : β × Ω✝ → F
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f
hX : AEMeasurable fun ω => (X ω, ω)
⊢ AEMeasurable X
[PROOFSTEP]
exact measurable_fst.comp_aemeasurable hX