case mp
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (indicator s f) → AEMeasurable f

case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f → AEMeasurable (indicator s f)
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (indicator s f) ↔ AEMeasurable f
constructor
case mp
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (indicator s f)
⊢ AEMeasurable f
case mp
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (indicator s f) → AEMeasurable f
intro h
no goals
case mp
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (indicator s f)
⊢ AEMeasurable f
exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
⊢ AEMeasurable (indicator s f)
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f → AEMeasurable (indicator s f)
intro h
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
⊢ indicator s f =ᶠ[ae μ] indicator s (AEMeasurable.mk f h)
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
⊢ AEMeasurable (indicator s f)
refine' ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, _⟩
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.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)
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f
⊢ indicator s f =ᶠ[ae μ] indicator s (AEMeasurable.mk f h)
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)
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.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)
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.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)
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
no goals
case mpr
ι : Type ?u.4760219
α : Type u_1
β : Type u_2
γ : Type ?u.4760228
δ : Type ?u.4760231
R : Type ?u.4760234
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.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)
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B