α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
⊢ ∃ M, 0 ≤ M ∧ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
⊢ ∃ M, 0 ≤ M ∧ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
have hf_mk : Memℒp (hf.1.mk f) 1 μ := (memℒp_congr_ae hf.1.ae_eq_mk).mp hf
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
⊢ ∃ M, 0 ≤ M ∧ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
⊢ ∃ M, 0 ≤ M ∧ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
obtain ⟨M, hM_pos, hfM⟩ :=
  hf_mk.integral_indicator_norm_ge_nonneg_le_of_meas μ hf.1.stronglyMeasurable_mk hε
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) =
    ∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
⊢ ∃ M, 0 ≤ M ∧ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) ≤ ENNReal.ofReal ε
refine' ⟨M, hM_pos, (le_of_eq _).trans hfM⟩
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
⊢ (fun x => ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊) =ᵐ[μ] fun x =>
    ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
          (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
⊢ (∫⁻ (x : α), ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ ∂μ) =
    ∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ
refine' lintegral_congr_ae _
case h
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
x : α
hx : f x = AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x
⊢ ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ =
    ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
          (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊
case intro.intro
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
⊢ (fun x => ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊) =ᵐ[μ] fun x =>
    ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
          (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊
filter_upwards [hf.1.ae_eq_mk] with x hx
no goals
case h
α : Type u_2
β : Type u_1
ι : Type ?u.89388
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : Memℒp f 1
ε : ℝ
hε : 0 < ε
hf_mk : Memℒp (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) 1
M : ℝ
hM_pos : 0 ≤ M
hfM :
  (∫⁻ (x : α),
      ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
            (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊ ∂μ) ≤
    ENNReal.ofReal ε
x : α
hx : f x = AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x
⊢ ↑‖Set.indicator {x | M ≤ ↑‖f x‖₊} f x‖₊ =
    ↑‖Set.indicator {x | M ≤ ↑‖AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ) x‖₊}
          (AEStronglyMeasurable.mk f (_ : AEStronglyMeasurable f μ)) x‖₊
simp only [Set.indicator_apply, coe_nnnorm, Set.mem_setOf_eq, ENNReal.coe_eq_coe, hx.symm]