α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
set g : ι → α → β := fun i => (hfu.1 i).choose
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfu.1 i).1
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have hgunif : UniformIntegrable g p μ := hfu.ae_eq fun i => (Exists.choose_spec <| hfu.1 i).2
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨C, hC⟩ := hgunif.spec' hp hp' hgmeas hε
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Set.indicator {x | C ≤ ‖f i x‖₊} (f i) =ᵐ[μ] Set.indicator {x | C ≤ ‖g i x‖₊} (g i)
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
refine' ⟨C, fun i => 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
⊢ Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x =
    Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Set.indicator {x | C ≤ ‖f i x‖₊} (f i) =ᵐ[μ] Set.indicator {x | C ≤ ‖g i x‖₊} (g i)
filter_upwards [(Exists.choose_spec <| hfu.1 i).2] with x hx
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 ≤ ‖f i x‖₊} (f i) x =
    Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 ≤ ‖f i x‖₊} (f i) x =
    Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (f i) μ)) x
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (_ : AEStronglyMeasurable (f i) μ) x
⊢ Set.indicator {x | C ≤ ‖f i x‖₊} (f i) x =
    Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 ≤ ‖f i x‖₊} (f i) x =
    Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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 ≤ ‖f i x‖₊} (f i) x =
    Set.indicator {x | C ≤ ‖Exists.choose (_ : AEStronglyMeasurable (f i) μ) x‖₊}
      (Exists.choose (_ : AEStronglyMeasurable (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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ⊤
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖g i x‖₊} (g 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