α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ ↑↑μ {a | f a = ⊤} = 0
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, f x < ⊤
simp_rw [ae_iff, ENNReal.not_lt_top]
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
⊢ False
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ ↑↑μ {a | f a = ⊤} = 0
by_contra h
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
⊢ ⊤ ≤ ∫⁻ (x : α), f x ∂μ
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
⊢ False
apply h2f.lt_top.not_le
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
this : indicator (f ⁻¹' {⊤}) ⊤ ≤ f
⊢ ⊤ ≤ ∫⁻ (x : α), f x ∂μ
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
⊢ ⊤ ≤ ∫⁻ (x : α), f x ∂μ
have : (f ⁻¹' {∞}).indicator ⊤ ≤ f := by
  intro x
  by_cases hx : x ∈ f ⁻¹' {∞} <;> [simpa [indicator_of_mem hx]; simp [indicator_of_not_mem hx]]
case h.e'_3
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
this : indicator (f ⁻¹' {⊤}) ⊤ ≤ f
⊢ ⊤ = ∫⁻ (a : α), indicator (f ⁻¹' {⊤}) ⊤ a ∂μ
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
this : indicator (f ⁻¹' {⊤}) ⊤ ≤ f
⊢ ⊤ ≤ ∫⁻ (x : α), f x ∂μ
convert lintegral_mono this
case h.e'_3
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
this : indicator (f ⁻¹' {⊤}) ⊤ ≤ f
⊢ ⊤ = ∫⁻ (a : α) in f ⁻¹' {⊤}, ⊤ a ∂μ
case h.e'_3
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
this : indicator (f ⁻¹' {⊤}) ⊤ ≤ f
⊢ ⊤ = ∫⁻ (a : α), indicator (f ⁻¹' {⊤}) ⊤ a ∂μ
rw [lintegral_indicator _ (hf (measurableSet_singleton ∞))]
no goals
case h.e'_3
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
this : indicator (f ⁻¹' {⊤}) ⊤ ≤ f
⊢ ⊤ = ∫⁻ (a : α) in f ⁻¹' {⊤}, ⊤ a ∂μ
simp [ENNReal.top_mul', preimage, h]
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
x : α
⊢ indicator (f ⁻¹' {⊤}) ⊤ x ≤ f x
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
⊢ indicator (f ⁻¹' {⊤}) ⊤ ≤ f
intro x
no goals
α : Type u_1
β : Type ?u.1736279
γ : Type ?u.1736282
δ : Type ?u.1736285
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
h2f : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ¬↑↑μ {a | f a = ⊤} = 0
x : α
⊢ indicator (f ⁻¹' {⊤}) ⊤ x ≤ f x
by_cases hx : x ∈ f ⁻¹' {∞} <;> [simpa [indicator_of_mem hx]; simp [indicator_of_not_mem hx]]