case pos
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f
⊢ IsFiniteMeasure (map f μ)

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f
⊢ IsFiniteMeasure (map f μ)
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
⊢ IsFiniteMeasure (map f μ)
by_cases hf : AEMeasurable f μ
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f
⊢ ↑↑(map f μ) univ < ⊤
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f
⊢ IsFiniteMeasure (map f μ)
constructor
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f
⊢ ↑↑μ (f ⁻¹' univ) < ⊤
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f
⊢ ↑↑(map f μ) univ < ⊤
rw [map_apply_of_aemeasurable hf MeasurableSet.univ]
no goals
case pos.measure_univ_lt_top
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f
⊢ ↑↑μ (f ⁻¹' univ) < ⊤
exact measure_lt_top μ _
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f
⊢ IsFiniteMeasure 0
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f
⊢ IsFiniteMeasure (map f μ)
rw [map_of_not_aemeasurable hf]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.617578
δ : Type ?u.617581
ι : Type ?u.617584
R : Type ?u.617587
R' : Type ?u.617590
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f
⊢ IsFiniteMeasure 0
exact MeasureTheory.isFiniteMeasureZero