[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
⊢ AEMeasurable f
[PROOFSTEP]
nontriviality α
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
✝ : Nontrivial α
⊢ AEMeasurable f
[PROOFSTEP]
inhabit α
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f
[PROOFSTEP]
exact ⟨fun _ => f default, measurable_const, rfl⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
⊢ AEMeasurable f
[PROOFSTEP]
nontriviality β
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
⊢ AEMeasurable f
[PROOFSTEP]
inhabit β
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ AEMeasurable f
[PROOFSTEP]
set s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ (h i).mk f x}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ AEMeasurable f
[PROOFSTEP]
have hsμ : ∀ i, μ i (s i) = 0 := by
  intro i
  rw [measure_toMeasurable]
  exact (h i).ae_eq_mk
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ ∀ (i : ι), ↑↑(μ i) (s i) = 0
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
⊢ ↑↑(μ i) (s i) = 0
[PROOFSTEP]
rw [measure_toMeasurable]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
⊢ ↑↑(μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x} = 0
[PROOFSTEP]
exact (h i).ae_eq_mk
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
⊢ AEMeasurable f
[PROOFSTEP]
have hsm : MeasurableSet (⋂ i, s i) := MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
⊢ AEMeasurable f
[PROOFSTEP]
have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
  intro i x hx
  contrapose! hx
  exact subset_toMeasurable _ _ hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
⊢ ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
[PROOFSTEP]
intro i x hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
i : ι
x : α
hx : ¬x ∈ s i
⊢ f x = mk f (_ : AEMeasurable f) x
[PROOFSTEP]
contrapose! hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
i : ι
x : α
hx : f x ≠ mk f (_ : AEMeasurable f) x
⊢ x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
[PROOFSTEP]
exact subset_toMeasurable _ _ hx
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
⊢ AEMeasurable f
[PROOFSTEP]
set g : α → β := (⋂ i, s i).piecewise (const α default) f
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ AEMeasurable f
[PROOFSTEP]
refine' ⟨g, measurable_of_restrict_of_restrict_compl hsm _ _, ae_sum_iff.mpr fun i => _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i) g)
[PROOFSTEP]
rw [restrict_piecewise]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i) (const α default))
[PROOFSTEP]
simp only [Set.restrict, const]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable fun x => default
[PROOFSTEP]
exact measurable_const
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋂ (i : ι), s i)ᶜ g)
[PROOFSTEP]
rw [restrict_piecewise_compl, compl_iInter]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
⊢ Measurable (Set.restrict (⋃ (i : ι), (s i)ᶜ) f)
[PROOFSTEP]
intro t ht
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (Set.restrict (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
[PROOFSTEP]
refine'
  ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ,
    MeasurableSet.iUnion fun i => (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, _⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ Subtype.val ⁻¹' ⋃ (i : ι), mk f (_ : AEMeasurable f) ⁻¹' t ∩ (s i)ᶜ = Set.restrict (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case refine'_2.h.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : x ∈ ⋃ (i : ι), (s i)ᶜ
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' ⋃ (i : ι), mk f (_ : AEMeasurable f) ⁻¹' t ∩ (s i)ᶜ ↔
    { val := x, property := hx } ∈ Set.restrict (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t
[PROOFSTEP]
simp only [mem_preimage, mem_iUnion, Subtype.coe_mk, Set.restrict, mem_inter_iff, mem_compl_iff] at hx ⊢
[GOAL]
case refine'_2.h.mk
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ (∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) ↔ f x ∈ t
[PROOFSTEP]
constructor
[GOAL]
case refine'_2.h.mk.mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ (∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) → f x ∈ t
[PROOFSTEP]
rintro ⟨i, hxt, hxs⟩
[GOAL]
case refine'_2.h.mk.mp.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
i : ι
hxt : mk f (_ : AEMeasurable f) x ∈ t
hxs : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t
[PROOFSTEP]
rwa [hs _ _ hxs]
[GOAL]
case refine'_2.h.mk.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ i, ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t → ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
[PROOFSTEP]
rcases hx with ⟨i, hi⟩
[GOAL]
case refine'_2.h.mk.mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ f x ∈ t → ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
[PROOFSTEP]
rw [hs _ _ hi]
[GOAL]
case refine'_2.h.mk.mpr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
⊢ mk f (_ : AEMeasurable f) x ∈ t →
    ∃ i, mk f (_ : AEMeasurable f) x ∈ t ∧ ¬x ∈ toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
[PROOFSTEP]
exact fun h => ⟨i, h, hi⟩
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x
[PROOFSTEP]
refine' measure_mono_null (fun x (hx : f x ≠ g x) => _) (hsμ i)
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : f x ≠ g x
⊢ x ∈ s i
[PROOFSTEP]
contrapose! hx
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : ¬x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
⊢ f x = piecewise (⋂ (i : ι), s i) (const α default) f x
[PROOFSTEP]
refine' (piecewise_eq_of_not_mem _ _ _ _).symm
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f
✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsm : MeasurableSet (⋂ (i : ι), s i)
hs : ∀ (i : ι) (x : α), ¬x ∈ s i → f x = mk f (_ : AEMeasurable f) x
g : α → β := piecewise (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : ¬x ∈ (fun i => toMeasurable (μ i) {x | f x ≠ mk f (_ : AEMeasurable f) x}) i
⊢ ¬x ∈ ⋂ (i : ι), s i
[PROOFSTEP]
exact fun h => hx (mem_iInter.1 h i)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
⊢ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
[PROOFSTEP]
rw [← sum_cond, aemeasurable_sum_measure_iff, Bool.forall_bool, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
⊢ AEMeasurable f ∧ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
s t : Set α
⊢ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
[PROOFSTEP]
simp only [union_eq_iUnion, aemeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ Measure.map g (Measure.map f μ) = Measure.map (g ∘ f) μ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
[PROOFSTEP]
let g' := hg.mk g
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
[PROOFSTEP]
have A : map g (map f μ) = map g' (map f μ) :=
  by
  apply MeasureTheory.Measure.map_congr
  exact hg.ae_eq_mk
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
[PROOFSTEP]
apply MeasureTheory.Measure.map_congr
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ g =ᶠ[ae (Measure.map f μ)] g'
[PROOFSTEP]
exact hg.ae_eq_mk
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
[PROOFSTEP]
have B : map (g ∘ f) μ = map (g' ∘ f) μ :=
  by
  apply MeasureTheory.Measure.map_congr
  exact ae_of_ae_map hf hg.ae_eq_mk
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
[PROOFSTEP]
apply MeasureTheory.Measure.map_congr
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ g ∘ f =ᶠ[ae μ] g' ∘ f
[PROOFSTEP]
exact ae_of_ae_map hf hg.ae_eq_mk
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
B : Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
[PROOFSTEP]
simp only [A, B, hs, hg.measurable_mk.aemeasurable.comp_aemeasurable hf, hg.measurable_mk, hg.measurable_mk hs, hf,
  map_apply, map_apply_of_aemeasurable]
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
B : Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
⊢ ↑↑μ (f ⁻¹' (mk g hg ⁻¹' s)) = ↑↑μ (mk g hg ∘ f ⁻¹' s)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
[PROOFSTEP]
let s : Set α := toMeasurable μ {x | f x = H.mk f x ∧ f x ∈ t}ᶜ
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
[PROOFSTEP]
let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
[PROOFSTEP]
refine' ⟨g, _, _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ Measurable g
[PROOFSTEP]
exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ range g ⊆ t
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case refine'_2.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
⊢ g x ∈ t
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t
[PROOFSTEP]
simpa [hx] using h₀.some_mem
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬x ∈ s
⊢ g x ∈ t
[PROOFSTEP]
simp only [hx, piecewise_eq_of_not_mem, not_false_iff]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬x ∈ s
⊢ mk f H x ∈ t
[PROOFSTEP]
contrapose! hx
[GOAL]
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬mk f H x ∈ t
⊢ x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
[PROOFSTEP]
apply subset_toMeasurable
[GOAL]
case neg.a
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
x : α
hx : ¬mk f H x ∈ t
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
[PROOFSTEP]
simp (config := { contextual := true }) only [hx, mem_compl_iff, mem_setOf_eq, not_and, not_false_iff, imp_true_iff]
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ f =ᶠ[ae μ] g
[PROOFSTEP]
have A : μ (toMeasurable μ {x | f x = H.mk f x ∧ f x ∈ t}ᶜ) = 0 :=
  by
  rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
  exact H.ae_eq_mk.and ht
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
[PROOFSTEP]
rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
⊢ {x | f x = mk f H x ∧ f x ∈ t} ∈ ae μ
[PROOFSTEP]
exact H.ae_eq_mk.and ht
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
⊢ f =ᶠ[ae μ] g
[PROOFSTEP]
filter_upwards [compl_mem_ae_iff.2 A] with x hx
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : x ∈ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ)ᶜ
⊢ f x = piecewise (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) (fun x => Set.Nonempty.some h₀) (mk f H) x
[PROOFSTEP]
rw [mem_compl_iff] at hx
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : ¬x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = piecewise (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) (fun x => Set.Nonempty.some h₀) (mk f H) x
[PROOFSTEP]
simp only [hx, piecewise_eq_of_not_mem, not_false_iff]
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : ¬x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = mk f H x
[PROOFSTEP]
contrapose! hx
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
[PROOFSTEP]
apply subset_toMeasurable
[GOAL]
case h.a
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
H : AEMeasurable f
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : Set.Nonempty t
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := piecewise s (fun x => Set.Nonempty.some h₀) (mk f H)
A : ↑↑μ (toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ) = 0
x : α
hx : f x ≠ mk f H x
⊢ x ∈ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
[PROOFSTEP]
simp only [hx, mem_compl_iff, mem_setOf_eq, false_and_iff, not_false_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f✝ g : α → β✝
μ ν : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
[PROOFSTEP]
obtain ⟨G, hG_meas, hG_mem, hG_ae_eq⟩ := hf.exists_ae_eq_range_subset f_nn ⟨0, le_rfl⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f✝ g : α → β✝
μ ν : Measure α
β : Type u_7
inst✝¹ : Preorder β
inst✝ : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
G : α → β
hG_meas : Measurable G
hG_mem : range G ⊆ Preorder.toLE.1 0
hG_ae_eq : f =ᶠ[ae μ] G
⊢ ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
[PROOFSTEP]
exact ⟨G, hG_meas, fun x => hG_mem (mem_range_self x), hG_ae_eq⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ AEMeasurable (codRestrict f s hfs)
[PROOFSTEP]
nontriviality α
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs)
[PROOFSTEP]
inhabit α
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs)
[PROOFSTEP]
obtain ⟨g, g_meas, hg, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ s ∧ f =ᵐ[μ] g :=
  h.exists_ae_eq_range_subset (eventually_of_forall hfs) ⟨_, hfs default⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ AEMeasurable (codRestrict f s hfs)
[PROOFSTEP]
refine' ⟨codRestrict g s fun x => hg (mem_range_self _), Measurable.subtype_mk g_meas, _⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
⊢ codRestrict f s hfs =ᶠ[ae μ] codRestrict g s (_ : ∀ (x : α), g x ∈ s)
[PROOFSTEP]
filter_upwards [fg] with x hx
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
h : AEMeasurable f
s : Set β
hfs : ∀ (x : α), f x ∈ s
✝ : Nontrivial α
inhabited_h : Inhabited α
g : α → β
g_meas : Measurable g
hg : range g ⊆ s
fg : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ codRestrict f s hfs x = codRestrict g s (_ : ∀ (x : α), g x ∈ s) x
[PROOFSTEP]
simpa [Subtype.ext_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
⊢ AEMeasurable f
[PROOFSTEP]
rcases eq_or_ne μ 0 with (rfl | hμ)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
ν : Measure α
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f
[PROOFSTEP]
exact aemeasurable_zero_measure
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f
[PROOFSTEP]
haveI := ae_neBot.2 hμ
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : NeBot (ae μ)
⊢ AEMeasurable f
[PROOFSTEP]
rcases h.exists with ⟨x, hx⟩
[GOAL]
case inr.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : NeBot (ae μ)
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f
[PROOFSTEP]
exact ⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : LinearOrder α
f : α → β
a b : α
⊢ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
[PROOFSTEP]
rw [uIoc_eq_union, aemeasurable_union_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable g ↔ AEMeasurable (g ∘ f)
[PROOFSTEP]
refine' ⟨fun H => H.comp_measurable hf.measurable, _⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable (g ∘ f) → AEMeasurable g
[PROOFSTEP]
rintro ⟨g₁, hgm₁, heq⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEMeasurable g
[PROOFSTEP]
rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ ν : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable g
[PROOFSTEP]
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
⊢ AEMeasurable (g ∘ f) ↔ AEMeasurable f
[PROOFSTEP]
refine' ⟨fun H => _, hg.measurable.comp_aemeasurable⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f)
⊢ AEMeasurable f
[PROOFSTEP]
suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
  rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f)
this : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ AEMeasurable f
[PROOFSTEP]
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : Measure α
H : AEMeasurable (g ∘ f)
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
[PROOFSTEP]
exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g : α → β
μ✝ ν : Measure α
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
⊢ AEMeasurable f ↔ AEMeasurable (f ∘ Subtype.val)
[PROOFSTEP]
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
⊢ AEMeasurable g
[PROOFSTEP]
haveI : Nonempty α := ⟨x⟩
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
⊢ AEMeasurable g
[PROOFSTEP]
obtain ⟨u, hu_tendsto⟩ := exists_seq_tendsto (atTop : Filter α)
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ AEMeasurable g
[PROOFSTEP]
have Ioi_eq_iUnion : Ioi x = ⋃ n : ℕ, Ioc x (u n) :=
  by
  rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
  exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ Ioi x = ⋃ (n : ℕ), Ioc x (u n)
[PROOFSTEP]
rw [iUnion_Ioc_eq_Ioi_self_iff.mpr _]
[GOAL]
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
⊢ ∀ (x_1 : α), x < x_1 → ∃ i, x_1 ≤ u i
[PROOFSTEP]
exact fun y _ => (hu_tendsto.eventually (eventually_ge_atTop y)).exists
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ AEMeasurable g
[PROOFSTEP]
rw [Ioi_eq_iUnion, aemeasurable_iUnion_iff]
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
⊢ ∀ (i : ℕ), AEMeasurable g
[PROOFSTEP]
intro n
[GOAL]
case intro
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
⊢ AEMeasurable g
[PROOFSTEP]
cases' lt_or_le x (u n) with h h
[GOAL]
case intro.inl
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : x < u n
⊢ AEMeasurable g
[PROOFSTEP]
exact g_meas (u n) h
[GOAL]
case intro.inr
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g
[PROOFSTEP]
rw [Ioc_eq_empty (not_lt.mpr h), Measure.restrict_empty]
[GOAL]
case intro.inr
ι : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
f g✝ : α → β✝
μ ν : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : IsCountablyGenerated atTop
x : α
g : α → β
g_meas : ∀ (t : α), t > x → AEMeasurable g
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ (n : ℕ), Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g
[PROOFSTEP]
exact aemeasurable_zero_measure
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (indicator s f) ↔ AEMeasurable f
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (indicator s f) → AEMeasurable f
[PROOFSTEP]
intro h
[GOAL]
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (indicator s f)
⊢ AEMeasurable f
[PROOFSTEP]
exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f → AEMeasurable (indicator s f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
⊢ AEMeasurable (indicator s f)
[PROOFSTEP]
refine' ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, _⟩
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
⊢ indicator s f =ᶠ[ae μ] indicator s (AEMeasurable.mk f h)
[PROOFSTEP]
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
  (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
A : indicator s f =ᶠ[ae (Measure.restrict μ s)] indicator s (AEMeasurable.mk f h)
⊢ indicator s f =ᶠ[ae μ] indicator s (AEMeasurable.mk f h)
[PROOFSTEP]
have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
  (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
[GOAL]
case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
A : indicator s f =ᶠ[ae (Measure.restrict μ s)] indicator s (AEMeasurable.mk f h)
B : indicator s f =ᶠ[ae (Measure.restrict μ sᶜ)] indicator s (AEMeasurable.mk f h)
⊢ indicator s f =ᶠ[ae μ] indicator s (AEMeasurable.mk f h)
[PROOFSTEP]
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s : Set α
hs : NullMeasurableSet s
⊢ AEMeasurable (indicator s f) ↔ AEMeasurable f
[PROOFSTEP]
rcases hs with ⟨t, ht, hst⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : Measure α
inst✝ : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ AEMeasurable (indicator s f) ↔ AEMeasurable f
[PROOFSTEP]
rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht, restrict_congr_set hst]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ restrict (map f μ) s = restrict (map (AEMeasurable.mk f hf) μ) s
[PROOFSTEP]
congr 1
[GOAL]
case e_μ
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ map f μ = map (AEMeasurable.mk f hf) μ
[PROOFSTEP]
apply Measure.map_congr hf.ae_eq_mk
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ map f (restrict μ (AEMeasurable.mk f hf ⁻¹' s)) = map f (restrict μ (f ⁻¹' s))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ restrict μ (AEMeasurable.mk f hf ⁻¹' s) = restrict μ (f ⁻¹' s)
[PROOFSTEP]
ext1 t ht
[GOAL]
case h.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (AEMeasurable.mk f hf ⁻¹' s)) t = ↑↑(restrict μ (f ⁻¹' s)) t
[PROOFSTEP]
simp only [ht, Measure.restrict_apply]
[GOAL]
case h.h
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (t ∩ AEMeasurable.mk f hf ⁻¹' s) = ↑↑μ (t ∩ f ⁻¹' s)
[PROOFSTEP]
apply measure_congr
[GOAL]
case h.h.H
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s
[PROOFSTEP]
apply (EventuallyEq.refl _ _).inter (hf.ae_eq_mk.symm.preimage s)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
R : Type u_6
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ ↑↑(map f μ) s ≤ ↑↑(map f ν) s
[PROOFSTEP]
simpa [hf, hs, hf.mono_measure h] using Measure.le_iff'.1 h (f ⁻¹' s)


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => ↑↑(f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun μ => ↑↑μ s) (MeasurableSpace.map f inst✝)
[PROOFSTEP]
rw [MeasurableSpace.map_comp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => ↑↑(f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ => ↑↑μ s) ∘ f) inst✝
[PROOFSTEP]
exact h s hs
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
⊢ MeasurableAdd₂ (Measure α)
[PROOFSTEP]
refine' ⟨Measure.measurable_of_measurable_coe _ fun s hs => _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(b.fst + b.snd) s
[PROOFSTEP]
simp_rw [Measure.coe_add, Pi.add_apply]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b.fst s + ↑↑b.snd s
[PROOFSTEP]
refine' Measurable.add _ _
[GOAL]
case refine'_1
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b.fst s
[PROOFSTEP]
exact (Measure.measurable_coe hs).comp measurable_fst
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b.snd s
[PROOFSTEP]
exact (Measure.measurable_coe hs).comp measurable_snd
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable fun μ => map f μ
[PROOFSTEP]
refine' measurable_of_measurable_coe _ fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(map f b) s
[PROOFSTEP]
simp_rw [map_apply hf hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b (f ⁻¹' s)
[PROOFSTEP]
exact measurable_coe (hf hs)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable dirac
[PROOFSTEP]
refine' measurable_of_measurable_coe _ fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(dirac b) s
[PROOFSTEP]
simp_rw [dirac_apply' _ hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => indicator s 1 b
[PROOFSTEP]
exact measurable_one.indicator hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ => ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ =>
    ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n),
        x * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {x})
[PROOFSTEP]
refine' measurable_iSup fun n => Finset.measurable_sum _ fun i _ => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => i * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
[PROOFSTEP]
refine' Measurable.const_mul _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
[PROOFSTEP]
exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
⊢ (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) ∅ (_ : MeasurableSet ∅) = 0
[PROOFSTEP]
simp only [measure_empty, lintegral_const, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
⊢ ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
        ∑' (i : ℕ), (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (f i) (_ : MeasurableSet (f i))
[PROOFSTEP]
intro f hf h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
⊢ (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
    ∑' (i : ℕ), (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (f i) (_ : MeasurableSet (f i))
[PROOFSTEP]
simp_rw [measure_iUnion h hf]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
⊢ ∫⁻ (μ : Measure α), ∑' (i : ℕ), ↑↑μ (f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), ↑↑μ (f i) ∂m
[PROOFSTEP]
apply lintegral_tsum
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
⊢ ∀ (i : ℕ), AEMeasurable fun a => ↑↑a (f i)
[PROOFSTEP]
intro i
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
i : ℕ
⊢ AEMeasurable fun a => ↑↑a (f i)
[PROOFSTEP]
exact (measurable_coe (hf i)).aemeasurable
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ join 0 = 0
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ ↑↑(join 0) s = ↑↑0 s
[PROOFSTEP]
simp only [hs, join_apply, lintegral_zero_measure, coe_zero, Pi.zero_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(join b) s
[PROOFSTEP]
simp only [join_apply hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (μ : Measure α), ↑↑μ s ∂b
[PROOFSTEP]
exact measurable_lintegral (measurable_coe hs)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α), f x ∂join m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
[PROOFSTEP]
simp_rw [lintegral_eq_iSup_eapprox_lintegral hf, SimpleFunc.lintegral,
  join_apply (SimpleFunc.measurableSet_preimage _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n),
        x * ∫⁻ (μ : Measure α), ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α),
      ⨆ (n : ℕ), ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n), x * ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
[PROOFSTEP]
suffices
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ n r, Measurable (f n r)) →
      Monotone (fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ n, ∑ r in s n, r * ∫⁻ μ, f n r μ ∂m = ∫⁻ μ, ⨆ n, ∑ r in s n, r * f n r μ ∂m
  by
  refine'
    this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' { r })) _ _
  · exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
  · exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
⊢ ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n),
        x * ∫⁻ (μ : Measure α), ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α),
      ⨆ (n : ℕ), ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n), x * ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
[PROOFSTEP]
refine'
  this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' { r })) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
⊢ ∀ (n : ℕ) (r : ℝ≥0∞), Measurable ((fun n r μ => ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {r})) n r)
[PROOFSTEP]
exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
⊢ Monotone fun n μ =>
    ∑ r in (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) n,
      r * (fun n r μ => ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {r})) n r μ
[PROOFSTEP]
exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
[PROOFSTEP]
intro s f hf hm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
[PROOFSTEP]
rw [lintegral_iSup _ hm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ => ∑ r in s n, r * f n r μ
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ => ∑ r in s n, r * f n r μ
[PROOFSTEP]
exact fun n => Finset.measurable_sum _ fun r _ => (hf _ _).const_mul _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ (fun n => ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) = fun n => ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
[PROOFSTEP]
funext n
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
n : ℕ
⊢ ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
[PROOFSTEP]
rw [lintegral_finset_sum (s n)]
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
n : ℕ
⊢ ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b in s n, ∫⁻ (a : Measure α), b * f n b a ∂m
[PROOFSTEP]
simp_rw [lintegral_const_mul _ (hf _ _)]
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
n : ℕ
⊢ ∀ (b : ℝ≥0∞), b ∈ s n → Measurable fun a => b * f n b a
[PROOFSTEP]
exact fun r _ => (hf _ _).const_mul _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
⊢ bind 0 f = 0
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
⊢ bind m 0 = 0
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(bind m 0) s = ↑↑0 s
[PROOFSTEP]
simp only [bind, hs, join_apply, coe_zero, Pi.zero_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), ↑↑μ s ∂map 0 m = 0
[PROOFSTEP]
rw [lintegral_map (measurable_coe hs) measurable_zero]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ↑↑(OfNat.ofNat 0 a) s ∂m = 0
[PROOFSTEP]
simp only [Pi.zero_apply, coe_zero, lintegral_const, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : Measurable f
⊢ ↑↑(bind m f) s = ∫⁻ (a : α), ↑↑(f a) s ∂m
[PROOFSTEP]
rw [bind, join_apply hs, lintegral_map (measurable_coe hs) hf]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
⊢ bind (bind m f) g = bind m fun a => bind (f a) g
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ↑↑(bind (bind m f) g) s = ↑↑(bind m fun a => bind (f a) g) s
[PROOFSTEP]
erw [bind_apply hs hg, bind_apply hs ((measurable_bind' hg).comp hf), lintegral_bind hf ((measurable_coe hs).comp hg)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => ↑↑μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
conv_rhs => enter [2, a]; erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
| ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
enter [2, a]; erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
| ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
enter [2, a]; erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
| ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
enter [2, a]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
a : α
| ↑↑(((fun m => bind m g) ∘ f) a) s
[PROOFSTEP]
erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
⊢ bind (dirac a) f = f a
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(bind (dirac a) f) s = ↑↑(f a) s
[PROOFSTEP]
erw [bind_apply hs hf, lintegral_dirac' a ((measurable_coe hs).comp hf)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((fun μ => ↑↑μ s) ∘ f) a = ↑↑(f a) s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
⊢ bind m dirac = m
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(bind m dirac) s = ↑↑m s
[PROOFSTEP]
simp only [bind_apply hs measurable_dirac, dirac_apply' _ hs, lintegral_indicator 1 hs, Pi.one_apply, lintegral_one,
  restrict_apply, MeasurableSet.univ, univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure α)
⊢ join μ = bind μ id
[PROOFSTEP]
rw [bind, map_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
⊢ join (map (map f) μ) = map f (join μ)
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ↑↑(join (map (map f) μ)) s = ↑↑(map f (join μ)) s
[PROOFSTEP]
rw [join_apply hs, map_apply hf hs, join_apply (hf hs), lintegral_map (measurable_coe hs) (measurable_map f hf)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), ↑↑(map f a) s ∂μ = ∫⁻ (μ : Measure α), ↑↑μ (f ⁻¹' s) ∂μ
[PROOFSTEP]
simp_rw [map_apply hf hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join (map join μ) = join (join μ)
[PROOFSTEP]
show bind μ join = join (join μ)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = join (join μ)
[PROOFSTEP]
rw [join_eq_bind, join_eq_bind, bind_bind measurable_id measurable_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = bind μ fun a => bind (id a) id
[PROOFSTEP]
apply congr_arg (bind μ)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join = fun a => bind (id a) id
[PROOFSTEP]
funext ν
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ join ν = bind (id ν) id
[PROOFSTEP]
exact join_eq_bind ν