case inl
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : ε < 0
⊢ ε * ENNReal.toReal (↑↑μ {x | ε ≤ f x}) ≤ ∫ (x : α), f x ∂μ

case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
⊢ ε * ENNReal.toReal (↑↑μ {x | ε ≤ f x}) ≤ ∫ (x : α), f x ∂μ
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
⊢ ε * ENNReal.toReal (↑↑μ {x | ε ≤ f x}) ≤ ∫ (x : α), f x ∂μ
cases' lt_or_le ε 0 with hε hε
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
⊢ ε * ENNReal.toReal (↑↑μ {x | ε ≤ f x}) ≤ ∫ (x : α), f x ∂μ
rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun x => hf_nonneg x)
    hf_int.aestronglyMeasurable,
  ← ENNReal.toReal_ofReal hε, ← ENNReal.toReal_mul]
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
have : { x : α | (ENNReal.ofReal ε).toReal ≤ f x } =
    { x : α | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x } := by
  ext1 x
  rw [Set.mem_setOf_eq, Set.mem_setOf_eq, ← ENNReal.toReal_ofReal (hf_nonneg x)]
  exact ENNReal.toReal_le_toReal ENNReal.ofReal_ne_top ENNReal.ofReal_ne_top
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
rw [this]
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
have h_meas : AEMeasurable (fun x => ENNReal.ofReal (f x)) μ :=
  measurable_id'.ennreal_ofReal.comp_aemeasurable hf_int.aemeasurable
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
have h_mul_meas_le := @mul_meas_ge_le_lintegral₀ _ _ μ _ h_meas (ENNReal.ofReal ε)
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x} ≤
    ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ

α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x} ≠ ⊤

α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) ≠ ⊤
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ ENNReal.toReal (ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}) ≤
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
rw [ENNReal.toReal_le_toReal _ _]
no goals
case inl
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : ε < 0
⊢ ε * ENNReal.toReal (↑↑μ {x | ε ≤ f x}) ≤ ∫ (x : α), f x ∂μ
exact
  (mul_nonpos_of_nonpos_of_nonneg hε.le ENNReal.toReal_nonneg).trans (integral_nonneg hf_nonneg)
case h
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
x : α
⊢ x ∈ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} ↔ x ∈ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
⊢ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
ext1 x
case h
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
x : α
⊢ ENNReal.toReal (ENNReal.ofReal ε) ≤ ENNReal.toReal (ENNReal.ofReal (f x)) ↔
    ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x
case h
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
x : α
⊢ x ∈ {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} ↔ x ∈ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
rw [Set.mem_setOf_eq, Set.mem_setOf_eq, ← ENNReal.toReal_ofReal (hf_nonneg x)]
no goals
case h
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
x : α
⊢ ENNReal.toReal (ENNReal.ofReal ε) ≤ ENNReal.toReal (ENNReal.ofReal (f x)) ↔
    ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x
exact ENNReal.toReal_le_toReal ENNReal.ofReal_ne_top ENNReal.ofReal_ne_top
no goals
case inr
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x} ≤
    ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
exact h_mul_meas_le
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ 0 < ε → ¬↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} = ⊤
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x} ≠ ⊤
simp only [Ne.def, ENNReal.mul_eq_top, ENNReal.ofReal_eq_zero, not_le,
  ENNReal.ofReal_ne_top, false_and_iff, or_false_iff, not_and]
no goals
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ 0 < ε → ¬↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} = ⊤
exact fun _ => measure_ne_top _ _
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) ≠ ⊤
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) ≠ ⊤
have h_lt_top : (∫⁻ a, ‖f a‖₊ ∂μ) < ∞ := hf_int.hasFiniteIntegral
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ENNReal.ofReal (abs (f a)) ∂μ) < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) ≠ ⊤
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ↑‖f a‖₊ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) ≠ ⊤
simp_rw [← ofReal_norm_eq_coe_nnnorm, Real.norm_eq_abs] at h_lt_top
case h.e'_2.h.e'_4.h.h.e'_1
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ENNReal.ofReal (abs (f a)) ∂μ) < ⊤
x✝ : α
⊢ f x✝ = abs (f x✝)
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ENNReal.ofReal (abs (f a)) ∂μ) < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) ≠ ⊤
convert h_lt_top.ne
case h.e'_2.h.e'_4.h.h.e'_1
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ENNReal.ofReal (abs (f a)) ∂μ) < ⊤
x : α
⊢ f x = abs (f x)
case h.e'_2.h.e'_4.h.h.e'_1
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ENNReal.ofReal (abs (f a)) ∂μ) < ⊤
x✝ : α
⊢ f x✝ = abs (f x✝)
rename_i x
no goals
case h.e'_2.h.e'_4.h.h.e'_1
α : Type u_1
E : Type ?u.1501155
F : Type ?u.1501158
𝕜 : Type ?u.1501161
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1503852
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ
hf_nonneg : 0 ≤ f
hf_int : Integrable f
ε : ℝ
hε : 0 ≤ ε
this : {x | ENNReal.toReal (ENNReal.ofReal ε) ≤ f x} = {x | ENNReal.ofReal ε ≤ (fun x => ENNReal.ofReal (f x)) x}
h_meas : AEMeasurable fun x => ENNReal.ofReal (f x)
h_mul_meas_le :
  ENNReal.ofReal ε * ↑↑μ {x | ENNReal.ofReal ε ≤ ENNReal.ofReal (f x)} ≤ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ
h_lt_top : (∫⁻ (a : α), ENNReal.ofReal (abs (f a)) ∂μ) < ⊤
x : α
⊢ f x = abs (f x)
rw [abs_of_nonneg (hf_nonneg x)]