α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (g i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
⊢ UnifIntegrable g p μ
intro ε hε
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (g i)) p μ ≤ ENNReal.ofReal ε
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (g i)) p μ ≤ ENNReal.ofReal ε
obtain ⟨δ, hδ_pos, hfδ⟩ := hf hε
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
n : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ Set.indicator s (g n) =ᵐ[μ] Set.indicator s (f n)
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ x,
    ∀ (i : ι) (s : Set α),
      MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (g i)) p μ ≤ ENNReal.ofReal ε
refine' ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| snorm_congr_ae _).trans (hfδ n s hs hμs)⟩
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
n : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
hx : f n x = g n x
⊢ Set.indicator s (g n) x = Set.indicator s (f n) x
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
n : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
⊢ Set.indicator s (g n) =ᵐ[μ] Set.indicator s (f n)
filter_upwards [hfg n] with x hx
no goals
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s (f i)) p μ ≤ ENNReal.ofReal ε
n : ι
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≤ ENNReal.ofReal δ
x : α
hx : f n x = g n x
⊢ Set.indicator s (g n) x = Set.indicator s (f n) x
simp_rw [Set.indicator_apply, hx]