case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
⊢ ↑↑(withDensity μ f) s = 0 → ↑↑μ ({x | f x ≠ 0} ∩ s) = 0

case mpr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
⊢ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0 → ↑↑(withDensity μ f) s = 0
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
⊢ ↑↑(withDensity μ f) s = 0 ↔ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
constructor
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
⊢ ↑↑(withDensity μ f) s = 0 → ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
intro hs
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
⊢ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
let t := toMeasurable (μ.withDensity f) s
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
⊢ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑(withDensity μ f) t = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = OfNat.ofNat 0 a)} = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0

case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ∀ᵐ (x : α) ∂Measure.restrict μ (toMeasurable (withDensity μ f) s), f x = OfNat.ofNat 0 x
⊢ MeasurableSet {x | f x = OfNat.ofNat 0 x}
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑(withDensity μ f) t = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
rw [withDensity_apply f (measurableSet_toMeasurable _ s), lintegral_eq_zero_iff hf,
  EventuallyEq, ae_restrict_iff, ae_iff] at A
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ∀ᵐ (x : α) ∂Measure.restrict μ (toMeasurable (withDensity μ f) s), f x = OfNat.ofNat 0 x
⊢ MeasurableSet {x | f x = OfNat.ofNat 0 x}

case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = OfNat.ofNat 0 a)} = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = OfNat.ofNat 0 a)} = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0

case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ∀ᵐ (x : α) ∂Measure.restrict μ (toMeasurable (withDensity μ f) s), f x = OfNat.ofNat 0 x
⊢ MeasurableSet {x | f x = OfNat.ofNat 0 x}
swap
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)} = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = OfNat.ofNat 0 a)} = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
simp only [Pi.zero_apply, mem_setOf_eq, Filter.mem_mk] at A
case h.e'_2.h.e'_3
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)} = 0
⊢ {x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s = {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)}
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)} = 0
⊢ ↑↑μ ({x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s) = 0
convert A using 2
case h.e'_2.h.e'_3.h
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)} = 0
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s ↔ x ∈ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)}
case h.e'_2.h.e'_3
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)} = 0
⊢ {x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s = {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)}
ext x
no goals
case h.e'_2.h.e'_3.h
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ↑↑μ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)} = 0
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ toMeasurable (withDensity μ f) s ↔ x ∈ {a | ¬(a ∈ toMeasurable (withDensity μ f) s → f a = 0)}
simp only [and_comm, exists_prop, mem_inter_iff, iff_self_iff, mem_setOf_eq, mem_compl_iff,
  not_forall]
no goals
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
⊢ ↑↑(withDensity μ f) t = 0
rw [measure_toMeasurable, hs]
no goals
case mp
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑(withDensity μ f) s = 0
t : Set α := toMeasurable (withDensity μ f) s
A : ∀ᵐ (x : α) ∂Measure.restrict μ (toMeasurable (withDensity μ f) s), f x = OfNat.ofNat 0 x
⊢ MeasurableSet {x | f x = OfNat.ofNat 0 x}
exact hf (measurableSet_singleton 0)
case mpr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
⊢ ↑↑(withDensity μ f) s = 0
case mpr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
⊢ ↑↑μ ({x | f x ≠ 0} ∩ s) = 0 → ↑↑(withDensity μ f) s = 0
intro hs
case mpr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ ↑↑(withDensity μ f) s = 0
case mpr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
⊢ ↑↑(withDensity μ f) s = 0
let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑(withDensity μ f) t = 0

α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑(withDensity μ f) {x | f x = 0} = 0
case mpr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑(withDensity μ f) s = 0
apply measure_mono_null A (measure_union_null _ _)
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
⊢ x ∈ t ∪ {x | f x = 0}
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ s ⊆ t ∪ {x | f x = 0}
intro x hx
case inl
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x = 0
⊢ x ∈ t ∪ {x | f x = 0}

case inr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t ∪ {x | f x = 0}
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
⊢ x ∈ t ∪ {x | f x = 0}
rcases eq_or_ne (f x) 0 with (fx | fx)
no goals
case inl
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x = 0
⊢ x ∈ t ∪ {x | f x = 0}
simp only [fx, mem_union, mem_setOf_eq, eq_self_iff_true, or_true_iff]
case inr.h
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t
case inr
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t ∪ {x | f x = 0}
left
case inr.h.a
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ {x | f x ≠ 0} ∩ s
case inr.h
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t
apply subset_toMeasurable _ _
no goals
case inr.h.a
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ {x | f x ≠ 0} ∩ s
exact ⟨fx, hx⟩
case a
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑μ t = 0
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑(withDensity μ f) t = 0
apply withDensity_absolutelyContinuous
no goals
case a
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑μ t = 0
rwa [measure_toMeasurable]
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
M : MeasurableSet {x | f x = 0}
⊢ ↑↑(withDensity μ f) {x | f x = 0} = 0
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ ↑↑(withDensity μ f) {x | f x = 0} = 0
have M : MeasurableSet { x : α | f x = 0 } := hf (measurableSet_singleton _)
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
M : MeasurableSet {x | f x = 0}
⊢ f =ᶠ[ae (Measure.restrict μ {x | f x = 0})] 0
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
M : MeasurableSet {x | f x = 0}
⊢ ↑↑(withDensity μ f) {x | f x = 0} = 0
rw [withDensity_apply _ M, lintegral_eq_zero_iff hf]
case h
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
M : MeasurableSet {x | f x = 0}
⊢ ∀ (a : α), f a = 0 → f a = OfNat.ofNat 0 a
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
M : MeasurableSet {x | f x = 0}
⊢ f =ᶠ[ae (Measure.restrict μ {x | f x = 0})] 0
filter_upwards [ae_restrict_mem M]
no goals
case h
α : Type u_1
β : Type ?u.1772759
γ : Type ?u.1772762
δ : Type ?u.1772765
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
s : Set α
hf : Measurable f
hs : ↑↑μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
M : MeasurableSet {x | f x = 0}
⊢ ∀ (a : α), f a = 0 → f a = OfNat.ofNat 0 a
simp only [imp_self, Pi.zero_apply, imp_true_iff]