[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)
