α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
⊢ (withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ withDensity μ fun x => ENNReal.ofReal (-f x)
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
⊢ (withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ withDensity μ fun x => ENNReal.ofReal (-f x)
set S : Set α := { x | f x < 0 }
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ withDensity μ fun x => ENNReal.ofReal (-f x)
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
⊢ (withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ withDensity μ fun x => ENNReal.ofReal (-f x)
have hS : MeasurableSet S := measurableSet_lt hf measurable_const
case refine'_1
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ↑↑(withDensity μ fun x => ENNReal.ofReal (f x)) S = 0

case refine'_2
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ↑↑(withDensity μ fun x => ENNReal.ofReal (-f x)) (Sᶜ) = 0
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (withDensity μ fun x => ENNReal.ofReal (f x)) ⟂ₘ withDensity μ fun x => ENNReal.ofReal (-f x)
refine' ⟨S, hS, _, _⟩
case refine'_1
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ S, ENNReal.ofReal (f x) = OfNat.ofNat 0 x
case refine'_1
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ↑↑(withDensity μ fun x => ENNReal.ofReal (f x)) S = 0
rw [withDensity_apply _ hS, lintegral_eq_zero_iff hf.ennreal_ofReal, EventuallyEq]
no goals
case refine'_1
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ S, ENNReal.ofReal (f x) = OfNat.ofNat 0 x
exact (ae_restrict_mem hS).mono fun x hx => ENNReal.ofReal_eq_zero.2 (le_of_lt hx)
case refine'_2
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (Sᶜ), ENNReal.ofReal (-f x) = OfNat.ofNat 0 x
case refine'_2
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ↑↑(withDensity μ fun x => ENNReal.ofReal (-f x)) (Sᶜ) = 0
rw [withDensity_apply _ hS.compl, lintegral_eq_zero_iff hf.neg.ennreal_ofReal, EventuallyEq]
no goals
case refine'_2
α : Type u_1
β : Type ?u.1769647
γ : Type ?u.1769650
δ : Type ?u.1769653
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (Sᶜ), ENNReal.ofReal (-f x) = OfNat.ofNat 0 x
exact
  (ae_restrict_mem hS.compl).mono fun x hx =>
    ENNReal.ofReal_eq_zero.2 (not_lt.1 <| mt neg_pos.1 hx)