-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.integral_indicator_norm_ge_le (hf : MemLp f 1 μ) (hmeas : StronglyMeasurable f)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ M : ℝ, (∫⁻ x, ‖{ x | M ≤ ‖f x‖₊ }.indicator f x‖₊ ∂μ) ≤ ENNReal.ofReal ε

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ 0 ≤ ‖f x‖

Tactic:
exact norm_nonneg _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
⊢ HasFiniteIntegral (fun x => ‖f x‖) μ

Tactic:
rw [memLp_one_iff_integrable] at hf

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
⊢ HasFiniteIntegral (fun x => ‖f x‖) μ

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M, ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε
⊢ ∫⁻ (x : α), ↑‖{x | ↑M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ) atTop (𝓝 0)

Tactic:
refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
n : ℕ
x : α
⊢ x ∈ {x | (fun a => ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖) x}

Tactic:
by_cases hx : (n : ℝ) ≤ ‖f x‖

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a => ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖) x}

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a => ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖) x}

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
M : ℕ
⊢ AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ

Tactic:
apply hf.1.indicator

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
M : ℕ
⊢ MeasurableSet {x | ↑M ≤ ↑‖f x‖₊}

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
M : ℕ
⊢ MeasurableSet {x | ↑M ≤ ↑‖f x‖₊}

Tactic:
apply StronglyMeasurable.measurableSet_le stronglyMeasurable_const
  hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable

Result:
no goals

Proof state:
case h.e'_3.h.e'_4.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x => ‖f x‖) μ
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε
M : ℕ
hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε
x✝ : α
⊢ ↑‖{x | ↑M ≤ ‖f x‖}.indicator f x✝‖₊ = ↑⟨‖{x | ↑M ≤ ‖f x‖₊}.indicator f x✝‖, ⋯⟩

Tactic:
rfl

Result:
no goals