α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
have hfi := integrable_toReal_of_lintegral_ne_top hfm hf
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
haveI := isFiniteMeasure_withDensity hf
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
⊢ MeasurableSet i → ↑(withDensityᵥ μ fun x => ENNReal.toReal (f x)) i = ↑(toSignedMeasure (withDensity μ f)) i
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
ext i
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ fun x => ENNReal.toReal (f x)) i = ↑(toSignedMeasure (withDensity μ f)) i
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
⊢ MeasurableSet i → ↑(withDensityᵥ μ fun x => ENNReal.toReal (f x)) i = ↑(toSignedMeasure (withDensity μ f)) i
intro hi
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂restrict μ i, f x < ⊤
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ fun x => ENNReal.toReal (f x)) i = ↑(toSignedMeasure (withDensity μ f)) i
rw [withDensityᵥ_apply hfi hi, toSignedMeasure_apply_measurable hi, withDensity_apply _ hi,
  integral_toReal hfm.restrict]
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in i, f x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂restrict μ i, f x < ⊤
refine' ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf _)
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in i, f x ∂μ) ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in i, f x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
conv_rhs => rw [← set_lintegral_univ]
no goals
case h
α : Type u_1
β : Type ?u.66433
m : MeasurableSpace α
μ ν : Measure α
E : Type ?u.66452
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (x : α) in i, f x ∂μ) ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ
exact lintegral_mono_set (Set.subset_univ _)