α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f' l g'
intro ε hε
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)
suffices
  (fun i => μ { x | ε ≤ dist (f' i x) (g' x) }) =ᶠ[l] fun i => μ { x | ε ≤ dist (f i x) (g x) } by
  rw [tendsto_congr' this]
  exact h_tendsto ε hε
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ ↑↑μ {x | ε ≤ dist (f' i x) (g' x)} = ↑↑μ {x | ε ≤ dist (f i x) (g x)}
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
filter_upwards [h_left] with i h_ae_eq
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ {x | ε ≤ dist (f' i x) (g' x)} =ᵐ[μ] {x | ε ≤ dist (f i x) (g x)}
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ ↑↑μ {x | ε ≤ dist (f' i x) (g' x)} = ↑↑μ {x | ε ≤ dist (f i x) (g x)}
refine' measure_congr _
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ setOf (fun x => ε ≤ dist (f' i x) (g' x)) x = setOf (fun x => ε ≤ dist (f i x) (g x)) x
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
⊢ {x | ε ≤ dist (f' i x) (g' x)} =ᵐ[μ] {x | ε ≤ dist (f i x) (g x)}
filter_upwards [h_ae_eq, h_right] with x hxf hxg
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ setOf (fun x => ε ≤ dist (f' i x) (g' x)) x ↔ setOf (fun x => ε ≤ dist (f i x) (g x)) x
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ setOf (fun x => ε ≤ dist (f' i x) (g' x)) x = setOf (fun x => ε ≤ dist (f i x) (g x)) x
rw [eq_iff_iff]
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ setOf (fun x => ε ≤ dist (f' i x) (g' x)) x ↔ setOf (fun x => ε ≤ dist (f i x) (g x)) x
change ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)
no goals
case h
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)
rw [hxg, hxf]
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)
rw [tendsto_congr' this]
no goals
α : Type u_2
ι : Type u_1
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => ↑↑μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => ↑↑μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
exact h_tendsto ε hε