α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
have htendsto :
    ∀ᵐ x ∂μ, Tendsto (fun M : ℕ => { x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f x) atTop (𝓝 0) :=
  univ_mem' (id fun x => tendsto_indicator_ge f x)
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
have hmeas : ∀ M : ℕ, AEStronglyMeasurable ({ x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f) μ := by
  intro M
  apply hf.1.indicator
  apply StronglyMeasurable.measurableSet_le stronglyMeasurable_const
    hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
have hbound : HasFiniteIntegral (fun x => ‖f x‖) μ := by
  rw [memℒp_one_iff_integrable] at hf
  exact hf.norm.2
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this : Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
rw [ENNReal.tendsto_atTop_zero] at this
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), n ≥ M → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ENNReal.ofReal ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
obtain ⟨M, hM⟩ := this (ENNReal.ofReal ε) (ENNReal.ofReal_pos.2 hε)
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), n ≥ M → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ENNReal.ofReal ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
simp only [true_and_iff, ge_iff_le, zero_tsub, zero_le, sub_zero, zero_add, coe_nnnorm,
  Set.mem_Icc] at hM
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
⊢ ∃ M, (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
refine' ⟨M, _⟩
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
x✝ : α
⊢ ↑‖Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x✝‖₊ = ENNReal.ofReal ‖Set.indicator {x | ↑M ≤ ‖f x‖₊} f x✝‖
case intro
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
convert hM M le_rfl
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
x✝ : α
⊢ ↑‖Set.indicator {x | ↑M ≤ ‖f x‖} f x✝‖₊ =
    ↑{ val := ‖Set.indicator {x | ↑M ≤ ‖f x‖₊} f x✝‖, property := (_ : 0 ≤ ‖Set.indicator {x | ↑M ≤ ‖f x‖₊} f x✝‖) }
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
x✝ : α
⊢ ↑‖Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x✝‖₊ = ENNReal.ofReal ‖Set.indicator {x | ↑M ≤ ‖f x‖₊} f x✝‖
simp only [coe_nnnorm, ENNReal.ofReal_eq_coe_nnreal (norm_nonneg _)]
no goals
case h.e'_3.h.e'_4.h
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
this :
  ∀ (ε : ℝ≥0∞),
    ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) ≤ ε
M : ℕ
hM : ∀ (n : ℕ), M ≤ n → (∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ∂μ) ≤ ENNReal.ofReal ε
x✝ : α
⊢ ↑‖Set.indicator {x | ↑M ≤ ‖f x‖} f x✝‖₊ =
    ↑{ val := ‖Set.indicator {x | ↑M ≤ ‖f x‖₊} f x✝‖, property := (_ : 0 ≤ ‖Set.indicator {x | ↑M ≤ ‖f x‖₊} f x✝‖) }
rfl
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
M : ℕ
⊢ AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
⊢ ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
intro M
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
M : ℕ
⊢ MeasurableSet {x | ↑M ≤ ↑‖f x‖₊}
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
M : ℕ
⊢ AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
apply hf.1.indicator
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
M : ℕ
⊢ MeasurableSet {x | ↑M ≤ ↑‖f x‖₊}
apply StronglyMeasurable.measurableSet_le stronglyMeasurable_const
  hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Integrable f
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
⊢ HasFiniteIntegral fun x => ‖f x‖
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
⊢ HasFiniteIntegral fun x => ‖f x‖
rw [memℒp_one_iff_integrable] at hf
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Integrable f
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
⊢ HasFiniteIntegral fun x => ‖f x‖
exact hf.norm.2
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
⊢ Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a - 0‖ ∂μ) atTop (𝓝 0)
refine' tendsto_lintegral_norm_of_dominated_convergence hmeas hbound _ htendsto
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
⊢ x ∈ {x | (fun a => ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x}
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖
refine' fun n => univ_mem' (id fun x => _)
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a => ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x}

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a => ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x}
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
⊢ x ∈ {x | (fun a => ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x}
by_cases hx : (n : ℝ) ≤ ‖f x‖
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a => ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x}
dsimp
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
rwa [Set.indicator_of_mem]
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a => ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f a‖ ≤ ‖f a‖) x}
dsimp
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ 0 ≤ ‖f x‖

case neg.h
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ ¬x ∈ {x | ↑n ≤ ‖f x‖₊}
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ ‖Set.indicator {x | ↑n ≤ ‖f x‖₊} f x‖ ≤ ‖f x‖
rw [Set.indicator_of_not_mem, norm_zero]
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ 0 ≤ ‖f x‖
exact norm_nonneg _
no goals
case neg.h
α : Type u_2
β : Type u_1
ι : Type ?u.20636
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable (Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f) μ
hbound : HasFiniteIntegral fun x => ‖f x‖
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ ¬x ∈ {x | ↑n ≤ ‖f x‖₊}
assumption