-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero (hf : MemLp f ∞ μ)
    (hmeas : StronglyMeasurable f) :
    ∃ M : ℝ, eLpNormEssSup ({ x | M ≤ ‖f x‖₊ }.indicator f) μ = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ eLpNormEssSup ({x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}.indicator f) μ = 0

Tactic:
rw [eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ eLpNormEssSup f (μ.restrict {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}) = 0

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ MeasurableSet {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal

Tactic:
rw [ENNReal.toReal_lt_toReal hbdd.ne]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ < eLpNormEssSup f μ + 1

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ + 1 ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ + 1 ≠ ⊤

Tactic:
exact (ENNReal.add_lt_top.2 ⟨hbdd, ENNReal.one_lt_top⟩).ne

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}

Tactic:
intro x hx

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ x ∈ {x | eLpNormEssSup f μ < ↑‖f x‖₊}

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Tactic:
have hle := coe_nnnorm_ae_le_eLpNormEssSup f μ

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
hle : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ x ∈ {x | eLpNormEssSup f μ < ↑‖f x‖₊}

Tactic:
rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
  ENNReal.coe_toReal, coe_nnnorm]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ (eLpNormEssSup f μ).toReal < ‖f x‖

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
hle : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Tactic:
simp_rw [ae_iff, not_le] at hle

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
hle : μ {a | eLpNormEssSup f μ < ‖f a‖ₑ} = 0
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
⊢ ∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0

Tactic:
have hbdd : eLpNormEssSup f μ < ∞ := hf.eLpNorm_lt_top

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ ∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ (eLpNormEssSup f μ).toReal < ‖f x‖

Tactic:
refine lt_of_lt_of_le ?_ hx

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
x : α
hx : x ∈ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
⊢ eLpNormEssSup f μ < eLpNormEssSup f μ + 1

Tactic:
exact ENNReal.lt_add_right hbdd.ne one_ne_zero

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : μ.restrict {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊} = 0
⊢ eLpNormEssSup f (μ.restrict {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}) = 0

Tactic:
rw [this, eLpNormEssSup_measure_zero]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ MeasurableSet {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}

Tactic:
exact measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ μ.restrict {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊} = 0

Tactic:
simp only [coe_nnnorm, eLpNorm_exponent_top, Measure.restrict_eq_zero]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} = 0