[GOAL]
x y : ℝ
hxy : x < y
⊢ Icc x y ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
rw [Icc_eq_closedBall]
[GOAL]
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
refine' closedBall_mem_vitaliFamily_of_dist_le_mul _ _ (by linarith)
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 < (y - x) / 2
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
rw [dist_comm, Real.dist_eq, abs_of_nonneg]
[GOAL]
x y : ℝ
hxy : x < y
⊢ (x + y) / 2 - x ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 ≤ (x + y) / 2 - x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ Tendsto (fun y => Icc x y) (𝓝[Ioi x] x) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
[PROOFSTEP]
refine' (VitaliFamily.tendsto_filterAt_iff _).2 ⟨_, _⟩
[GOAL]
case refine'_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_right hy
[GOAL]
case refine'_2
x : ℝ
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ⊆ Metric.closedBall x ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ⊆ Metric.closedBall x ε
[PROOFSTEP]
have : x ∈ Ico x (x + ε) := ⟨le_refl _, by linarith⟩
[GOAL]
x ε : ℝ
εpos : ε > 0
⊢ x < x + ε
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
⊢ ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ⊆ Metric.closedBall x ε
[PROOFSTEP]
filter_upwards [Icc_mem_nhdsWithin_Ioi this] with y hy
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε
[PROOFSTEP]
rw [closedBall_eq_Icc]
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Icc (x - ε) (x + ε)
[PROOFSTEP]
exact Icc_subset_Icc (by linarith) hy.2
[GOAL]
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ x - ε ≤ x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ Icc x y ∈ VitaliFamily.setsAt (vitaliFamily volume 1) y
[PROOFSTEP]
rw [Icc_eq_closedBall]
[GOAL]
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (vitaliFamily volume 1) y
[PROOFSTEP]
refine' closedBall_mem_vitaliFamily_of_dist_le_mul _ _ (by linarith)
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 < (y - x) / 2
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
rw [Real.dist_eq, abs_of_nonneg]
[GOAL]
x y : ℝ
hxy : x < y
⊢ y - (x + y) / 2 ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 ≤ y - (x + y) / 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ Tendsto (fun y => Icc y x) (𝓝[Iio x] x) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
[PROOFSTEP]
refine' (VitaliFamily.tendsto_filterAt_iff _).2 ⟨_, _⟩
[GOAL]
case refine'_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_left hy
[GOAL]
case refine'_2
x : ℝ
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
[PROOFSTEP]
have : x ∈ Ioc (x - ε) x := ⟨by linarith, le_refl _⟩
[GOAL]
x ε : ℝ
εpos : ε > 0
⊢ x - ε < x
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
[PROOFSTEP]
filter_upwards [Icc_mem_nhdsWithin_Iio this] with y hy
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε
[PROOFSTEP]
rw [closedBall_eq_Icc]
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)
[PROOFSTEP]
exact Icc_subset_Icc hy.1 (by linarith)
[GOAL]
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ x ≤ x + ε
[PROOFSTEP]
linarith
