case intro
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
⊢ UniformIntegrable f p μ
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
⊢ UniformIntegrable f p μ
cases nonempty_fintype ι
case intro
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
case intro
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
⊢ UniformIntegrable f p μ
refine' ⟨fun n => (hf n).1, unifIntegrable_finite μ hp_one hp_top hf, _⟩
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C

case neg
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
case intro
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
by_cases hι : Nonempty ι
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
choose _ hf using hf
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
set C := (Finset.univ.image fun i : ι => snorm (f i) p μ).max'
  ⟨snorm (f hι.some) p μ, Finset.mem_image.2 ⟨hι.some, Finset.mem_univ _, rfl⟩⟩
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
⊢ snorm (f i) p μ ≤ ↑(ENNReal.toNNReal C)
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
refine' ⟨C.toNNReal, fun i => _⟩
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
⊢ snorm (f i) p μ ≤ C

case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
⊢ C ≠ ⊤
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
⊢ snorm (f i) p μ ≤ ↑(ENNReal.toNNReal C)
rw [ENNReal.coe_toNNReal]
no goals
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
⊢ snorm (f i) p μ ≤ C
exact Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
y : ℝ≥0∞
hy : y ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ
⊢ y < ⊤
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
⊢ C ≠ ⊤
refine' ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => _)
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
y : ℝ≥0∞
hy : ∃ a, a ∈ Finset.univ ∧ snorm (f a) p μ = y
⊢ y < ⊤
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
y : ℝ≥0∞
hy : y ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ
⊢ y < ⊤
rw [Finset.mem_image] at hy
case pos.intro.intro
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i✝ i : ι
⊢ snorm (f i) p μ < ⊤
case pos
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i : ι
y : ℝ≥0∞
hy : ∃ a, a ∈ Finset.univ ∧ snorm (f a) p μ = y
⊢ y < ⊤
obtain ⟨i, -, rfl⟩ := hy
no goals
case pos.intro.intro
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), snorm (f i) p μ < ⊤
C : ℝ≥0∞ :=
  Finset.max' (Finset.image (fun i => snorm (f i) p μ) Finset.univ)
    (_ : ∃ x, x ∈ Finset.image (fun i => snorm (f i) p μ) Finset.univ)
i✝ i : ι
⊢ snorm (f i) p μ < ⊤
exact hf i
no goals
case neg
α : Type u_3
β : Type u_2
ι : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
hf : ∀ (i : ι), Memℒp (f i) p
val✝ : Fintype ι
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (f i) p μ ≤ ↑C
exact ⟨0, fun i => False.elim <| hι <| Nonempty.intro i⟩