α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
⊢ UnifIntegrable f p μ
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UnifIntegrable f p μ
set g : ι → α → β := fun i => (hf i).choose
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
⊢ ∃ C,
    0 < C ∧
      ∀ (i : ι),
        snorm
            (Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
              (Exists.choose (_ : AEStronglyMeasurable (f i) μ)))
            p μ ≤
          ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
⊢ UnifIntegrable f p μ
refine'
  (unifIntegrable_of' μ hp hp' (fun i => (Exists.choose_spec <| hf i).1) fun ε hε => _).ae_eq
    fun i => (Exists.choose_spec <| hf i).2.symm
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C,
    0 < C ∧
      ∀ (i : ι),
        snorm
            (Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
              (Exists.choose (_ : AEStronglyMeasurable (f i) μ)))
            p μ ≤
          ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
⊢ ∃ C,
    0 < C ∧
      ∀ (i : ι),
        snorm
            (Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
              (Exists.choose (_ : AEStronglyMeasurable (f i) μ)))
            p μ ≤
          ENNReal.ofReal ε
obtain ⟨C, hC⟩ := h ε hε
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ ‖Set.indicator {x | max C 1 ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
        (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x‖ ≤
    ‖Set.indicator {x | C ≤ ‖g i x‖₊} (g i) x‖
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C,
    0 < C ∧
      ∀ (i : ι),
        snorm
            (Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
              (Exists.choose (_ : AEStronglyMeasurable (f i) μ)))
            p μ ≤
          ENNReal.ofReal ε
refine' ⟨max C 1, lt_max_of_lt_right one_pos, fun i => le_trans (snorm_mono fun x => _) (hCg i)⟩
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ Set.indicator {x | max C 1 ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (fun a => ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) a‖) x ≤
    Set.indicator {x | C ≤ ‖g i x‖₊} (fun a => ‖g i a‖) x
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ ‖Set.indicator {x | max C 1 ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
        (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x‖ ≤
    ‖Set.indicator {x | C ≤ ‖g i x‖₊} (g i) x‖
rw [norm_indicator_eq_indicator_norm, norm_indicator_eq_indicator_norm]
no goals
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ Set.indicator {x | max C 1 ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (fun a => ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) a‖) x ≤
    Set.indicator {x | C ≤ ‖g i x‖₊} (fun a => ‖g i a‖) x
exact Set.indicator_le_indicator_of_subset
  (fun x hx => Set.mem_setOf_eq ▸ le_trans (le_max_left _ _) hx) (fun _ => norm_nonneg _) _
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
intro i
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Set.indicator {x | C ≤ ‖g i x‖₊} (g i) =ᵐ[μ] Set.indicator {x | C ≤ ‖f i x‖₊} (f i)
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
refine' le_trans (le_of_eq <| snorm_congr_ae _) (hC i)
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
⊢ Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x =
    Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Set.indicator {x | C ≤ ‖g i x‖₊} (g i) =ᵐ[μ] Set.indicator {x | C ≤ ‖f i x‖₊} (f i)
filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x =
    Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x

case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : ¬x ∈ {x | C ≤ ‖f i x‖₊}
⊢ Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x =
    Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
⊢ Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x =
    Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x
by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ x ∈ {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x =
    Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x
rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
no goals
case pos.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ x ∈ {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
rwa [Set.mem_setOf, hx] at hfx
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : ¬x ∈ {x | C ≤ ‖f i x‖₊}
⊢ ¬x ∈ {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : ¬x ∈ {x | C ≤ ‖f i x‖₊}
⊢ Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x =
    Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x
rw [Set.indicator_of_not_mem hfx, Set.indicator_of_not_mem]
no goals
case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f✝ : ℕ → α → β
g✝ : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
hfx : ¬x ∈ {x | C ≤ ‖f i x‖₊}
⊢ ¬x ∈ {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
rwa [Set.mem_setOf, hx] at hfx