[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (thickening ε s)
[PROOFSTEP]
rw [← ball_mul_one]
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)
[PROOFSTEP]
exact hs.mul_left
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (thickening ε s)
[PROOFSTEP]
rw [← ball_mul_one]
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)
[PROOFSTEP]
exact hs.mul_left
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (cthickening ε s)
[PROOFSTEP]
rw [cthickening_eq_iInter_thickening'']
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (⋂ (ε_1 : ℝ) (_ : max 0 ε < ε_1), thickening ε_1 s)
[PROOFSTEP]
exact isUpperSet_iInter₂ fun δ _ => hs.thickening' _
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (cthickening ε s)
[PROOFSTEP]
rw [cthickening_eq_iInter_thickening'']
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (⋂ (ε_1 : ℝ) (_ : max 0 ε < ε_1), thickening ε_1 s)
[PROOFSTEP]
exact isLowerSet_iInter₂ fun δ _ => hs.thickening' _
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
⊢ y ∈ interior s
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
⊢ y ∈ interior s
[PROOFSTEP]
obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h
[GOAL]
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
⊢ y ∈ interior s
[PROOFSTEP]
obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : dist x z < ε
⊢ y ∈ interior s
[PROOFSTEP]
rw [dist_pi_lt_iff hε] at hxz
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ y ∈ interior s
[PROOFSTEP]
have hyz : ∀ i, z i < y i :=
  by
  refine' fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans _)
  rw [← Real.norm_eq_abs, ← dist_eq_norm']
  exact (hxz _).le
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), z i < y i
[PROOFSTEP]
refine' fun i => (hxy _).trans_le' (sub_le_iff_le_add'.1 <| (le_abs_self _).trans _)
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ |z i - x i| ≤ ε
[PROOFSTEP]
rw [← Real.norm_eq_abs, ← dist_eq_norm']
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε
[PROOFSTEP]
exact (hxz _).le
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz : ∀ (i : ι), z i < y i
⊢ y ∈ interior s
[PROOFSTEP]
obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
⊢ y ∈ interior s
[PROOFSTEP]
refine' mem_interior.2 ⟨ball y δ, _, isOpen_ball, mem_ball_self hδ⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
⊢ ball y δ ⊆ s
[PROOFSTEP]
rintro w hw
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
hw : w ∈ ball y δ
⊢ w ∈ s
[PROOFSTEP]
refine' hs (fun i => _) hz
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
hw : w ∈ ball y δ
i : ι
⊢ z i ≤ w i
[PROOFSTEP]
simp_rw [ball_pi _ hδ, Real.ball_eq_Ioo] at hw
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), x i + ε < y i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), z i < y i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), z i + δ < y i
w : ι → ℝ
i : ι
hw : w ∈ pi univ fun b => Ioo (y b - δ) (y b + δ)
⊢ z i ≤ w i
[PROOFSTEP]
exact ((lt_sub_iff_add_lt.2 <| hyz _).trans (hw _ <| mem_univ _).1).le
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
⊢ y ∈ interior s
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
⊢ y ∈ interior s
[PROOFSTEP]
obtain ⟨ε, hε, hxy⟩ := Pi.exists_forall_pos_add_lt h
[GOAL]
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
⊢ y ∈ interior s
[PROOFSTEP]
obtain ⟨z, hz, hxz⟩ := Metric.mem_closure_iff.1 hx _ hε
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : dist x z < ε
⊢ y ∈ interior s
[PROOFSTEP]
rw [dist_pi_lt_iff hε] at hxz
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ y ∈ interior s
[PROOFSTEP]
have hyz : ∀ i, y i < z i :=
  by
  refine' fun i => (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans _)
  rw [← Real.norm_eq_abs, ← dist_eq_norm]
  exact (hxz _).le
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
⊢ ∀ (i : ι), y i < z i
[PROOFSTEP]
refine' fun i => (lt_sub_iff_add_lt.2 <| hxy _).trans_le (sub_le_comm.1 <| (le_abs_self _).trans _)
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ |x i - z i| ≤ ε
[PROOFSTEP]
rw [← Real.norm_eq_abs, ← dist_eq_norm]
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε
[PROOFSTEP]
exact (hxz _).le
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz : ∀ (i : ι), y i < z i
⊢ y ∈ interior s
[PROOFSTEP]
obtain ⟨δ, hδ, hyz⟩ := Pi.exists_forall_pos_add_lt hyz
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
⊢ y ∈ interior s
[PROOFSTEP]
refine' mem_interior.2 ⟨ball y δ, _, isOpen_ball, mem_ball_self hδ⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
⊢ ball y δ ⊆ s
[PROOFSTEP]
rintro w hw
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
hw : w ∈ ball y δ
⊢ w ∈ s
[PROOFSTEP]
refine' hs (fun i => _) hz
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
hw : w ∈ ball y δ
i : ι
⊢ w i ≤ z i
[PROOFSTEP]
simp_rw [ball_pi _ hδ, Real.ball_eq_Ioo] at hw
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ✝ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
hyz✝ : ∀ (i : ι), y i < z i
δ : ℝ
hδ : 0 < δ
hyz : ∀ (i : ι), y i + δ < z i
w : ι → ℝ
i : ι
hw : w ∈ pi univ fun b => Ioo (y b - δ) (y b + δ)
⊢ w i ≤ z i
[PROOFSTEP]
exact ((hw _ <| mem_univ _).2.trans <| hyz _).le
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
[PROOFSTEP]
refine' ⟨x + const _ (3 / 4 * δ), closedBall_subset_closedBall' _, _⟩
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x + const ι (3 / 4 * δ)) x ≤ δ
[PROOFSTEP]
rw [dist_self_add_left]
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖const ι (3 / 4 * δ)‖ ≤ δ
[PROOFSTEP]
refine' (add_le_add_left (pi_norm_const_le <| 3 / 4 * δ) _).trans_eq _
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ
[PROOFSTEP]
simp [Real.norm_of_nonneg, hδ.le, zero_le_three]
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + |3| / |4| * |δ| = δ
[PROOFSTEP]
simp [abs_of_pos, abs_of_pos hδ]
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + 3 / 4 * δ = δ
[PROOFSTEP]
ring
[GOAL]
case refine'_2
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
[PROOFSTEP]
obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
⊢ closedBall (x + const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
[PROOFSTEP]
refine' fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => _
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : z ∈ closedBall (x + const ι (3 / 4 * δ)) (δ / 4)
i : ι
⊢ y i < z i
[PROOFSTEP]
rw [mem_closedBall, dist_eq_norm'] at hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ y i < z i
[PROOFSTEP]
rw [dist_eq_norm] at hxy
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : ‖x - y‖ < δ / 4
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ y i < z i
[PROOFSTEP]
replace hxy := (norm_le_pi_norm _ i).trans hxy.le
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
hz : ‖x + const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
⊢ y i < z i
[PROOFSTEP]
replace hz := (norm_le_pi_norm _ i).trans hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
hz : ‖(x + const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4
⊢ y i < z i
[PROOFSTEP]
dsimp at hxy hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : |x i - y i| ≤ δ / 4
hz : |x i + 3 / 4 * δ - z i| ≤ δ / 4
⊢ y i < z i
[PROOFSTEP]
rw [abs_sub_le_iff] at hxy hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsUpperSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
hz : x i + 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i + 3 / 4 * δ) ≤ δ / 4
⊢ y i < z i
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
[PROOFSTEP]
refine' ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' _, _⟩
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ
[PROOFSTEP]
rw [dist_self_sub_left]
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖const ι (3 / 4 * δ)‖ ≤ δ
[PROOFSTEP]
refine' (add_le_add_left (pi_norm_const_le <| 3 / 4 * δ) _).trans_eq _
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + ‖3 / 4 * δ‖ = δ
[PROOFSTEP]
simp [abs_of_pos, abs_of_pos hδ]
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ δ / 4 + 3 / 4 * δ = δ
[PROOFSTEP]
ring
[GOAL]
case refine'_2
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
[PROOFSTEP]
obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
⊢ closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
[PROOFSTEP]
refine' fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => _
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : z ∈ closedBall (x - const ι (3 / 4 * δ)) (δ / 4)
i : ι
⊢ z i < y i
[PROOFSTEP]
rw [mem_closedBall, dist_eq_norm'] at hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : dist x y < δ / 4
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i
[PROOFSTEP]
rw [dist_eq_norm] at hxy
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
hxy : ‖x - y‖ < δ / 4
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
⊢ z i < y i
[PROOFSTEP]
replace hxy := (norm_le_pi_norm _ i).trans hxy.le
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
⊢ z i < y i
[PROOFSTEP]
replace hz := (norm_le_pi_norm _ i).trans hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : ‖(x - y) i‖ ≤ δ / 4
hz : ‖(x - const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4
⊢ z i < y i
[PROOFSTEP]
dsimp at hxy hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : |x i - y i| ≤ δ / 4
hz : |x i - 3 / 4 * δ - z i| ≤ δ / 4
⊢ z i < y i
[PROOFSTEP]
rw [abs_sub_le_iff] at hxy hz
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x y✝ : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
y : ι → ℝ
hy : y ∈ s
z : ι → ℝ
i : ι
hxy : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4
hz : x i - 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i - 3 / 4 * δ) ≤ δ / 4
⊢ z i < y i
[PROOFSTEP]
linarith


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u ~[l] v
⊢ v =O[l] u
[PROOFSTEP]
convert h.isLittleO.right_isBigO_add
[GOAL]
case h.e'_8.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u ~[l] v
x✝ : α
⊢ u x✝ = (u - v) x✝ + v x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
⊢ u ~[l] u
[PROOFSTEP]
rw [IsEquivalent, sub_self]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
⊢ 0 =o[l] u
[PROOFSTEP]
exact isLittleO_zero _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =ᶠ[l] 0
[PROOFSTEP]
rw [IsEquivalent, sub_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
⊢ u =o[l] 0 ↔ u =ᶠ[l] 0
[PROOFSTEP]
exact isLittleO_zero_right_iff
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =O[l] 0
[PROOFSTEP]
refine' ⟨IsEquivalent.isBigO, fun h ↦ _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u =O[l] 0
⊢ u ~[l] 0
[PROOFSTEP]
rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u =O[l] 0
⊢ ∃ s, s ∈ l ∧ Set.EqOn u 0 s
[PROOFSTEP]
exact ⟨{x : α | u x = 0}, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ u ~[l] const α c ↔ Tendsto u l (𝓝 c)
[PROOFSTEP]
simp_rw [IsEquivalent, const, isLittleO_const_iff h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun x => c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun x => c) l (𝓝 0) → Tendsto u l (𝓝 c)
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto u l (𝓝 c) → Tendsto (u - fun x => c) l (𝓝 0)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)
[PROOFSTEP]
have := h.sub (tendsto_const_nhds (a := -c))
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
this : Tendsto (fun x => (u - fun x => c) x - -c) l (𝓝 (0 - -c))
⊢ Tendsto u l (𝓝 c)
[PROOFSTEP]
simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x => c) l (𝓝 0)
this : Tendsto (fun x => u x) l (𝓝 c)
⊢ Tendsto u l (𝓝 c)
[PROOFSTEP]
exact this
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x => c) l (𝓝 0)
[PROOFSTEP]
have := h.sub (tendsto_const_nhds (a := c))
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
this : Tendsto (fun x => u x - c) l (𝓝 (c - c))
⊢ Tendsto (u - fun x => c) l (𝓝 0)
[PROOFSTEP]
rwa [sub_self] at this
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
hu : u ~[l] const α c
⊢ Tendsto u l (𝓝 c)
[PROOFSTEP]
rcases em <| c = 0 with rfl | h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)
[PROOFSTEP]
exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)
[PROOFSTEP]
exact (isEquivalent_const_iff_tendsto h).mp hu
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
⊢ Tendsto v l (𝓝 c)
[PROOFSTEP]
by_cases h : c = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)
[PROOFSTEP]
subst c
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
⊢ Tendsto v l (𝓝 0)
[PROOFSTEP]
rw [← isLittleO_one_iff ℝ] at hu ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hu : u =o[l] fun _x => 1
⊢ v =o[l] fun _x => 1
[PROOFSTEP]
simpa using (huv.symm.isLittleO.trans hu).add hu
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)
[PROOFSTEP]
rw [← isEquivalent_const_iff_tendsto h] at hu ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c
[PROOFSTEP]
exact huv.symm.trans hu
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hwv : w =o[l] v
⊢ u + w ~[l] v
[PROOFSTEP]
simpa only [IsEquivalent, add_sub_right_comm] using huv.add hwv
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hwv : w =o[l] v
⊢ u - w ~[l] v
[PROOFSTEP]
simpa only [sub_eq_add_neg] using huv.add_isLittleO hwv.neg_left
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x => -u x) ~[l] fun x => -v x
[PROOFSTEP]
rw [IsEquivalent]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ ((fun x => -u x) - fun x => -v x) =o[l] fun x => -v x
[PROOFSTEP]
convert huv.isLittleO.neg_left.neg_right
[GOAL]
case h.e'_7.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
x✝ : α
⊢ ((fun x => -u x) - fun x => -v x) x✝ = -(u - v) x✝
[PROOFSTEP]
simp [neg_add_eq_sub]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ u ~[l] v ↔ ∃ φ x, u =ᶠ[l] φ * v
[PROOFSTEP]
rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ (∃ φ _hφ, u - v =ᶠ[l] φ * v) ↔ ∃ φ x, u =ᶠ[l] φ * v
[PROOFSTEP]
constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine' ⟨φ + 1, _, _⟩; refine' ⟨φ - 1, _, _⟩]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ (∃ φ _hφ, u - v =ᶠ[l] φ * v) ↔ ∃ φ x, u =ᶠ[l] φ * v
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ (∃ φ _hφ, u - v =ᶠ[l] φ * v) → ∃ φ x, u =ᶠ[l] φ * v
[PROOFSTEP]
rintro ⟨φ, hφ, h⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ (∃ φ x, u =ᶠ[l] φ * v) → ∃ φ _hφ, u - v =ᶠ[l] φ * v
[PROOFSTEP]
rintro ⟨φ, hφ, h⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ ∃ φ x, u =ᶠ[l] φ * v
[PROOFSTEP]
refine' ⟨φ + 1, _, _⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ _hφ, u - v =ᶠ[l] φ * v
[PROOFSTEP]
refine' ⟨φ - 1, _, _⟩
[GOAL]
case mp.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 1)
[PROOFSTEP]
conv in 𝓝 _ => rw [← zero_add (1 : β)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
| 𝓝 1
[PROOFSTEP]
rw [← zero_add (1 : β)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
| 𝓝 1
[PROOFSTEP]
rw [← zero_add (1 : β)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
| 𝓝 1
[PROOFSTEP]
rw [← zero_add (1 : β)]
[GOAL]
case mp.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 (0 + 1))
[PROOFSTEP]
exact hφ.add tendsto_const_nhds
[GOAL]
case mp.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v
[PROOFSTEP]
convert h.add (EventuallyEq.refl l v)
[GOAL]
case h.e'_4.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
x✝ : α
⊢ u x✝ = (u - v) x✝ + v x✝
[PROOFSTEP]
simp [add_mul]
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
x✝ : α
⊢ ((φ + 1) * v) x✝ = (φ * v) x✝ + v x✝
[PROOFSTEP]
simp [add_mul]
[GOAL]
case mpr.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)
[PROOFSTEP]
conv in 𝓝 _ => rw [← sub_self (1 : β)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
| 𝓝 0
[PROOFSTEP]
rw [← sub_self (1 : β)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
| 𝓝 0
[PROOFSTEP]
rw [← sub_self (1 : β)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
| 𝓝 0
[PROOFSTEP]
rw [← sub_self (1 : β)]
[GOAL]
case mpr.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (1 - 1))
[PROOFSTEP]
exact hφ.sub tendsto_const_nhds
[GOAL]
case mpr.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
[PROOFSTEP]
convert h.sub (EventuallyEq.refl l v)
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((φ - 1) * v) x✝ = (φ * v) x✝ - v x✝
[PROOFSTEP]
simp [sub_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
huv : Tendsto (u / v) l (𝓝 1)
⊢ u ~[l] v
[PROOFSTEP]
rw [isEquivalent_iff_exists_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
huv : Tendsto (u / v) l (𝓝 1)
⊢ ∃ φ x, u =ᶠ[l] φ * v
[PROOFSTEP]
refine' ⟨u / v, huv, hz.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v ↔ Tendsto (u / v) l (𝓝 1)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v → Tendsto (u / v) l (𝓝 1)
[PROOFSTEP]
intro hequiv
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
⊢ Tendsto (u / v) l (𝓝 1)
[PROOFSTEP]
have := hequiv.isLittleO.tendsto_div_nhds_zero
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => (u - v) x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
[PROOFSTEP]
simp only [Pi.sub_apply, sub_div] at this
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
[PROOFSTEP]
have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
  (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
⊢ Tendsto (u / v) l (𝓝 1)
[PROOFSTEP]
convert this.add key
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1
[PROOFSTEP]
norm_num
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v
[PROOFSTEP]
exact isEquivalent_of_tendsto_one (hz.mono fun x hnvz hz ↦ (hnvz hz).elim)
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
⊢ (fun x => a x • u x) ~[l] fun x => b x • v x
[PROOFSTEP]
rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩
[GOAL]
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ (fun x => a x • u x) ~[l] fun x => b x • v x
[PROOFSTEP]
have : ((fun x ↦ a x • u x) - (fun x ↦ b x • v x)) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x) := by
  -- Porting note: `convert` has become too strong, so we need to specify `using 1`.
  convert (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).sub (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
  ext
  rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
[PROOFSTEP]
convert (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).sub (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
[GOAL]
case h.e'_5
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ (fun x => b x • (φ x • u x - v x)) = fun x => (φ * b) x • u x - b x • v x
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
x✝ : α
⊢ b x✝ • (φ x✝ • u x✝ - v x✝) = (φ * b) x✝ • u x✝ - b x✝ • v x✝
[PROOFSTEP]
rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
[GOAL]
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
⊢ (fun x => a x • u x) ~[l] fun x => b x • v x
[PROOFSTEP]
refine' (isLittleO_congr this.symm <| EventuallyEq.rfl).mp ((isBigO_refl b l).smul_isLittleO _)
[GOAL]
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
⊢ (fun x => φ x • u x - v x) =o[l] fun x => v x
[PROOFSTEP]
rcases huv.isBigO.exists_pos with ⟨C, hC, hCuv⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : IsBigOWith C l u v
⊢ (fun x => φ x • u x - v x) =o[l] fun x => v x
[PROOFSTEP]
rw [IsEquivalent] at *
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : (a - b) =o[l] b
huv : (u - v) =o[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : IsBigOWith C l u v
⊢ (fun x => φ x • u x - v x) =o[l] fun x => v x
[PROOFSTEP]
rw [isLittleO_iff] at *
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : IsBigOWith C l u v
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
rw [IsBigOWith] at hCuv
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
simp only [Metric.tendsto_nhds, dist_eq_norm] at hφ
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
intro c hc
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
specialize hφ (c / 2 / C) (div_pos (div_pos hc zero_lt_two) hC)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
specialize huv (div_pos hc zero_lt_two)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
refine' hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ _)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
have key :=
  calc
    ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ := by gcongr
    _ ≤ c / 2 / C * (C * ‖v x‖) := by gcongr
    _ = c / 2 * ‖v x‖ := by
      field_simp [hC.ne.symm]
      ring
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ c / 2 / C * ‖u x‖ ≤ c / 2 / C * (C * ‖v x‖)
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ c / 2 / C * (C * ‖v x‖) = c / 2 * ‖v x‖
[PROOFSTEP]
field_simp [hC.ne.symm]
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ c * (C * ‖v x‖) * 2 = c * ‖v x‖ * (2 * C)
[PROOFSTEP]
ring
[GOAL]
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
[PROOFSTEP]
calc
  ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by simp [sub_smul, sub_add]
  _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := (norm_add_le _ _)
  _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
  _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
  _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
  _ = c * ‖v x‖ := by ring
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖((fun x => φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖
[PROOFSTEP]
simp [sub_smul, sub_add]
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
[PROOFSTEP]
rw [norm_smul]
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ c / 2 * ‖v x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖
[PROOFSTEP]
gcongr
[GOAL]
case bc
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖u x - v x‖ ≤ c / 2 * ‖v x‖
[PROOFSTEP]
exact huvx
[GOAL]
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x => a x • u x) - fun x => b x • v x) =ᶠ[l] fun x => b x • (φ x • u x - v x)
C : ℝ
hC : 0 < C
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ = c * ‖v x‖
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x => (u x)⁻¹) ~[l] fun x => (v x)⁻¹
[PROOFSTEP]
rw [isEquivalent_iff_exists_eq_mul] at *
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
huv : ∃ φ x, u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
[PROOFSTEP]
rcases huv with ⟨φ, hφ, h⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
[PROOFSTEP]
rw [← inv_one]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
[PROOFSTEP]
refine' ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by norm_num), _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ 1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ (fun x => (u x)⁻¹) =ᶠ[l] (fun x => (φ x)⁻¹) * fun x => (v x)⁻¹
[PROOFSTEP]
convert h.inv
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((fun x => (φ x)⁻¹) * fun x => (v x)⁻¹) x✝ = ((φ * v) x✝)⁻¹
[PROOFSTEP]
simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
htu : t ~[l] u
hvw : v ~[l] w
⊢ (fun x => t x / v x) ~[l] fun x => u x / w x
[PROOFSTEP]
simpa only [div_eq_mul_inv] using htu.mul hvw.inv
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ Tendsto v l atBot
[PROOFSTEP]
convert tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ v = Neg.neg ∘ fun x => -v x
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝¹ : NormedLinearOrderedField β
u v : α → β
l : Filter α
inst✝ : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
x✝ : α
⊢ v x✝ = (Neg.neg ∘ fun x => -v x) x✝
[PROOFSTEP]
simp


[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
rcases exists_extension_of_le_sublinear ⟨p, f⟩ (fun x => ‖f‖ * ‖x‖)
    (fun c hc x => by simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm])
    (fun x y => by
      -- Porting note: placeholder filled here
      rw [← left_distrib]
      exact mul_le_mul_of_nonneg_left (norm_add_le x y) (@norm_nonneg _ _ f))
    fun x => le_trans (le_abs_self _) (f.le_op_norm _) with
  ⟨g, g_eq, g_le⟩
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
c : ℝ
hc : 0 < c
x : E
⊢ (fun x => ‖f‖ * ‖x‖) (c • x) = c * (fun x => ‖f‖ * ‖x‖) x
[PROOFSTEP]
simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ (fun x => ‖f‖ * ‖x‖) x + (fun x => ‖f‖ * ‖x‖) y
[PROOFSTEP]
rw [← left_distrib]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ ‖f‖ * (‖x‖ + ‖y‖)
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (norm_add_le x y) (@norm_nonneg _ _ f)
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
set g' := g.mkContinuous ‖f‖ fun x => abs_le.2 ⟨neg_le.1 <| g.map_neg x ▸ norm_neg x ▸ g_le (-x), g_le x⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
refine' ⟨g', g_eq, _⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
⊢ ‖g'‖ = ‖f‖
[PROOFSTEP]
apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
⊢ ‖f‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖
[PROOFSTEP]
refine' f.op_norm_le_bound (norm_nonneg _) fun x => _
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
x : { x // x ∈ p }
⊢ ‖↑f x‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖ * ‖x‖
[PROOFSTEP]
dsimp at g_eq
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
x : { x // x ∈ p }
⊢ ‖↑f x‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖ * ‖x‖
[PROOFSTEP]
rw [← g_eq]
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
x : { x // x ∈ p }
⊢ ‖↑g ↑x‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖ * ‖x‖
[PROOFSTEP]
apply g'.le_op_norm
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
letI : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
letI : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower _ _ _
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
letI : NormedSpace ℝ F :=
  NormedSpace.restrictScalars _ 𝕜
    _
      -- Let `fr: p →L[ℝ] ℝ` be the real part of `f`.
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
let fr :=
  reClm.comp
    (f.restrictScalars ℝ)
      -- Use the real version to get a norm-preserving extension of `fr`, which
        -- we'll call `g : F →L[ℝ] ℝ`.
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
rcases Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr with
  ⟨g, ⟨hextends, hnormeq⟩⟩
    -- Now `g` can be extended to the `F →L[𝕜] 𝕜` we need.
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
refine'
  ⟨g.extendTo𝕜, _⟩
    -- It is an extension of `f`.
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ (∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x) ∧ ‖ContinuousLinearMap.extendTo𝕜 g‖ = ‖f‖
[PROOFSTEP]
have h : ∀ x : p, g.extendTo𝕜 x = f x := by
  intro x
  rw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends]
  have : (fr x : 𝕜) - I * ↑(fr (I • x)) = (re (f x) : 𝕜) - (I : 𝕜) * re (f ((I : 𝕜) • x)) := by rfl
  rw [this]
  apply ext
  ·
    simp only [add_zero, Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul,
      ofReal_re, eq_self_iff_true, sub_zero, mul_neg, ofReal_neg, mul_re, mul_zero, sub_neg_eq_add,
      ContinuousLinearMap.map_smul]
  ·
    simp only [Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul, ofReal_re,
      mul_neg, mul_im, zero_add, ofReal_neg, mul_re, sub_neg_eq_add, ContinuousLinearMap.map_smul]
      -- And we derive the equality of the norms by bounding on both sides.
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
⊢ ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
[PROOFSTEP]
rw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
⊢ ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑f x
[PROOFSTEP]
have : (fr x : 𝕜) - I * ↑(fr (I • x)) = (re (f x) : 𝕜) - (I : 𝕜) * re (f ((I : 𝕜) • x)) := by rfl
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
⊢ ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
this : ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))
⊢ ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑f x
[PROOFSTEP]
rw [this]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
this : ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))
⊢ ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x))) = ↑f x
[PROOFSTEP]
apply ext
[GOAL]
case hre
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
this : ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))
⊢ ↑re (↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))) = ↑re (↑f x)
[PROOFSTEP]
simp only [add_zero, Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul,
  ofReal_re, eq_self_iff_true, sub_zero, mul_neg, ofReal_neg, mul_re, mul_zero, sub_neg_eq_add,
  ContinuousLinearMap.map_smul]
[GOAL]
case him
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
this : ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))
⊢ ↑im (↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))) = ↑im (↑f x)
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im', zero_mul, ofReal_re, mul_neg,
  mul_im, zero_add, ofReal_neg, mul_re, sub_neg_eq_add, ContinuousLinearMap.map_smul]
  -- And we derive the equality of the norms by bounding on both sides.
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ (∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x) ∧ ‖ContinuousLinearMap.extendTo𝕜 g‖ = ‖f‖
[PROOFSTEP]
refine' ⟨h, le_antisymm _ _⟩
[GOAL]
case intro.intro.refine'_1
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ ‖ContinuousLinearMap.extendTo𝕜 g‖ ≤ ‖f‖
[PROOFSTEP]
calc
  ‖g.extendTo𝕜‖ = ‖g‖ := g.norm_extendTo𝕜
  _ = ‖fr‖ := hnormeq
  _ ≤ ‖reClm‖ * ‖f‖ := (ContinuousLinearMap.op_norm_comp_le _ _)
  _ = ‖f‖ := by rw [reClm_norm, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ ‖reClm‖ * ‖f‖ = ‖f‖
[PROOFSTEP]
rw [reClm_norm, one_mul]
[GOAL]
case intro.intro.refine'_2
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ ‖f‖ ≤ ‖ContinuousLinearMap.extendTo𝕜 g‖
[PROOFSTEP]
exact f.op_norm_le_bound g.extendTo𝕜.op_norm_nonneg fun x => h x ▸ g.extendTo𝕜.le_op_norm x
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ‖↑‖x‖ • coord 𝕜 x h‖ = 1
[PROOFSTEP]
rw [norm_smul (x := coord 𝕜 x h), IsROrC.norm_coe_norm, coord_norm, mul_inv_cancel (mt norm_eq_zero.mp h)]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
let p : Submodule 𝕜 E := 𝕜 ∙ x
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
let f := (‖x‖ : 𝕜) • coord 𝕜 x h
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
obtain ⟨g, hg⟩ := exists_extension_norm_eq p f
[GOAL]
case intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
refine' ⟨g, _, _⟩
[GOAL]
case intro.refine'_1
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ‖g‖ = 1
[PROOFSTEP]
rw [hg.2, coord_norm']
[GOAL]
case intro.refine'_2
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑‖x‖
[PROOFSTEP]
calc
  g x = g (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [coe_mk]
  _ = ((‖x‖ : 𝕜) • coord 𝕜 x h) (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [← hg.1]
  _ = ‖x‖ := by simp
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑g ↑{ val := x, property := (_ : x ∈ span 𝕜 {x}) }
[PROOFSTEP]
rw [coe_mk]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g ↑{ val := x, property := (_ : x ∈ span 𝕜 {x}) } =
    ↑(↑‖x‖ • coord 𝕜 x h) { val := x, property := (_ : x ∈ span 𝕜 {x}) }
[PROOFSTEP]
rw [← hg.1]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑(↑‖x‖ • coord 𝕜 x h) { val := x, property := (_ : x ∈ span 𝕜 {x}) } = ↑‖x‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
obtain ⟨y, hy⟩ := exists_ne (0 : E)
[GOAL]
case pos.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
obtain ⟨g, hg⟩ : ∃ g : E →L[𝕜] 𝕜, ‖g‖ = 1 ∧ g y = ‖y‖ := exists_dual_vector 𝕜 y hy
[GOAL]
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
refine' ⟨g, hg.left, _⟩
[GOAL]
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ↑g x = ↑‖x‖
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
exact exists_dual_vector 𝕜 x hx
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
refine' ⟨0, by simp, _⟩
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ‖0‖ ≤ 1
[PROOFSTEP]
simp
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ↑0 x = ↑‖x‖
[PROOFSTEP]
symm
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ↑‖x‖ = ↑0 x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
rcases exists_dual_vector 𝕜 x hx with ⟨g, g_norm, g_eq⟩
[GOAL]
case neg.intro.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
g : E →L[𝕜] 𝕜
g_norm : ‖g‖ = 1
g_eq : ↑g x = ↑‖x‖
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
exact ⟨g, g_norm.le, g_eq⟩