internlm/Lean-Github huggingface dataset:
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
have xp : x > 0 := lt_of_lt_of_le yp xy
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
have yi : y⁻¹ ≤ (-b).exp := by rw [Real.exp_neg]; bound
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
rw [abs_of_nonneg (sub_nonneg.mpr xy)]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * (x - y)
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ |x.log - y.log| ≤ (-b).exp * (x - y)
Tactic:
rw [abs_of_nonneg (sub_nonneg.mpr ((Real.log_le_log_iff yp xp).mpr xy))]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x.log - y.log ≤ (-b).exp * (x - y)
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x.log - y.log ≤ (-b).exp * (x - y)
Tactic:
rw [← Real.log_div xp.ne' yp.ne']
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (x / y).log ≤ (-b).exp * (x - y)
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (x / y).log ≤ (-b).exp * (x - y)
Tactic:
rw [Real.log_le_iff_le_exp (div_pos xp yp)]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ ((-b).exp * (x - y)).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ ((-b).exp * (x - y)).exp
Tactic:
trans (y⁻¹ * (x - y)).exp
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp
Tactic:
swap
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ (y⁻¹ * (x - y)).exp ≤ ((-b).exp * (x - y)).exp

E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Tactic:
bound
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Tactic:
have e : y⁻¹ * (x - y) = x / y - 1 := by field_simp [yp.ne']
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (y⁻¹ * (x - y)).exp
Tactic:
rw [e]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (x / y - 1).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
⊢ x / y ≤ (x / y - 1).exp
Tactic:
have e1 := Real.add_one_le_exp (x / y - 1)
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y - 1 + 1 ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y - 1 + 1 ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp
Tactic:
simp at e1
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
e : y⁻¹ * (x - y) = x / y - 1
e1 : x / y ≤ (x / y - 1).exp
⊢ x / y ≤ (x / y - 1).exp
Tactic:
exact e1
Proof state after:
no goals
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ y⁻¹ ≤ (-b).exp
Tactic:
rw [Real.exp_neg]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ y⁻¹ ≤ b.exp⁻¹
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
⊢ y⁻¹ ≤ b.exp⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
xp : x > 0
yi : y⁻¹ ≤ (-b).exp
⊢ y⁻¹ * (x - y) = x / y - 1
Tactic:
field_simp [yp.ne']
Proof state after:
no goals
Theorem: LipschitzOnWith.log
Proof state before:
case pos
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
exact half x y ys xy
Proof state after:
no goals
Theorem: LipschitzWith.maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzWith (-b).exp.toNNReal (_root_.maxLog b)
Tactic:
rw [← lipschitzOn_univ]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Theorem: LipschitzWith.maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Tactic:
have h := (LipschitzOnWith.log b).comp ((LipschitzWith.id.const_max b.exp).lipschitzOnWith univ)
  (by simp only [id_eq, Set.mapsTo_univ_iff, Set.mem_Ici, le_max_iff, le_refl, true_or,
    forall_const])
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Theorem: LipschitzWith.maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Tactic:
have e : Real.log ∘ max (Real.exp b) = _root_.maxLog b := by funext x; simp [_root_.maxLog]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
e : Real.log ∘ max b.exp = _root_.maxLog b
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Theorem: LipschitzWith.maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
e : Real.log ∘ max b.exp = _root_.maxLog b
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Tactic:
simpa only [e, mul_one, id_eq, ge_iff_le, lipschitzOn_univ] using h
Proof state after:
no goals
Theorem: LipschitzWith.maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Set.MapsTo (fun x => max b.exp (id x)) univ (Ici b.exp)
Tactic:
simp only [id_eq, Set.mapsTo_univ_iff, Set.mem_Ici, le_max_iff, le_refl, true_or,
forall_const]
Proof state after:
no goals
Theorem: LipschitzWith.maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
⊢ Real.log ∘ max b.exp = _root_.maxLog b
Tactic:
funext x
Proof state after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
x : ℝ
⊢ (Real.log ∘ max b.exp) x = _root_.maxLog b x
Theorem: LipschitzWith.maxLog
Proof state before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
x : ℝ
⊢ (Real.log ∘ max b.exp) x = _root_.maxLog b x
Tactic:
simp [_root_.maxLog]
Proof state after:
no goals
Theorem: atInf_basis
Proof state before:
X : Type
inst✝ : Norm X
⊢ atInf.HasBasis (fun x => True) fun r => {x | r < ‖x‖}
Tactic:
apply Filter.hasBasis_iInf_principal
Proof state after:
case h
X : Type
inst✝ : Norm X
⊢ Directed (fun x x_1 => x ≥ x_1) fun i => {x | i < ‖x‖}
Theorem: atInf_basis
Proof state before:
case h
X : Type
inst✝ : Norm X
⊢ Directed (fun x x_1 => x ≥ x_1) fun i => {x | i < ‖x‖}
Tactic:
apply directed_of_isDirected_le
Proof state after:
case h.H
X : Type
inst✝ : Norm X
⊢ ∀ ⦃i j : ℝ⦄, i ≤ j → {x | i < ‖x‖} ≥ {x | j < ‖x‖}
Theorem: atInf_basis
Proof state before:
case h.H
X : Type
inst✝ : Norm X
⊢ ∀ ⦃i j : ℝ⦄, i ≤ j → {x | i < ‖x‖} ≥ {x | j < ‖x‖}
Tactic:
intro a b ab
Proof state after:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ {x | a < ‖x‖} ≥ {x | b < ‖x‖}
Theorem: atInf_basis
Proof state before:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ {x | a < ‖x‖} ≥ {x | b < ‖x‖}
Tactic:
simp only [ge_iff_le, le_eq_subset, setOf_subset_setOf]
Proof state after:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ ∀ (a_1 : X), b < ‖a_1‖ → a < ‖a_1‖
Theorem: atInf_basis
Proof state before:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
⊢ ∀ (a_1 : X), b < ‖a_1‖ → a < ‖a_1‖
Tactic:
intro x h
Proof state after:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
x : X
h : b < ‖x‖
⊢ a < ‖x‖
Theorem: atInf_basis
Proof state before:
case h.H
X : Type
inst✝ : Norm X
a b : ℝ
ab : a ≤ b
x : X
h : b < ‖x‖
⊢ a < ‖x‖
Tactic:
linarith
Proof state after:
no goals
Theorem: tendsto_atInf
Proof state before:
X Y : Type
inst✝ : Norm Y
f : X → Y
l : Filter X
⊢ Tendsto f l atInf ↔ ∀ (r : ℝ), ∀ᶠ (x : X) in l, r < ‖f x‖
Tactic:
rw [atInf_basis.tendsto_right_iff]
Proof state after:
X Y : Type
inst✝ : Norm Y
f : X → Y
l : Filter X
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : X) in l, f x ∈ {x | i < ‖x‖}) ↔ ∀ (r : ℝ), ∀ᶠ (x : X) in l, r < ‖f x‖
Theorem: tendsto_atInf
Proof state before:
X Y : Type
inst✝ : Norm Y
f : X → Y
l : Filter X
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : X) in l, f x ∈ {x | i < ‖x‖}) ↔ ∀ (r : ℝ), ∀ᶠ (x : X) in l, r < ‖f x‖
Tactic:
simp only [true_imp_iff, mem_setOf]
Proof state after:
no goals
Theorem: tendsto_atTop_atInf
Proof state before:
X : Type
inst✝ : Norm X
f : ℕ → X
⊢ Tendsto f atTop atInf ↔ ∀ (r : ℝ), ∃ N, ∀ (n : ℕ), N ≤ n → r < ‖f n‖
Tactic:
have h := Filter.HasBasis.tendsto_iff (f := f) Filter.atTop_basis atInf_basis
Proof state after:
X : Type
inst✝ : Norm X
f : ℕ → X
h : Tendsto f atTop atInf ↔ ∀ (ib : ℝ), True → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ {x | ib < ‖x‖}
⊢ Tendsto f atTop atInf ↔ ∀ (r : ℝ), ∃ N, ∀ (n : ℕ), N ≤ n → r < ‖f n‖
Theorem: tendsto_atTop_atInf
Proof state before:
X : Type
inst✝ : Norm X
f : ℕ → X
h : Tendsto f atTop atInf ↔ ∀ (ib : ℝ), True → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ {x | ib < ‖x‖}
⊢ Tendsto f atTop atInf ↔ ∀ (r : ℝ), ∃ N, ∀ (n : ℕ), N ≤ n → r < ‖f n‖
Tactic:
simpa only [mem_Ici, ge_iff_le, mem_setOf_eq, exists_true_left, forall_true_left, true_and]
  using h
Proof state after:
no goals
Theorem: tendsto_atInf_iff_norm_tendsto_atTop
Proof state before:
X Y : Type
inst✝ : Norm Y
f : Filter X
g : X → Y
⊢ Tendsto (fun x => g x) f atInf ↔ Tendsto (fun x => ‖g x‖) f atTop
Tactic:
rw [Filter.atTop_basis_Ioi.tendsto_right_iff]
Proof state after:
X Y : Type
inst✝ : Norm Y
f : Filter X
g : X → Y
⊢ Tendsto (fun x => g x) f atInf ↔ ∀ (i : ℝ), True → ∀ᶠ (x : X) in f, ‖g x‖ ∈ Ioi i
Theorem: tendsto_atInf_iff_norm_tendsto_atTop
Proof state before:
X Y : Type
inst✝ : Norm Y
f : Filter X
g : X → Y
⊢ Tendsto (fun x => g x) f atInf ↔ ∀ (i : ℝ), True → ∀ᶠ (x : X) in f, ‖g x‖ ∈ Ioi i
Tactic:
simp only [atInf_basis.tendsto_right_iff, true_imp_iff, mem_setOf, mem_Ioi]
Proof state after:
no goals
Theorem: mem_atInf_iff
Proof state before:
X : Type
inst✝ : Norm X
s : Set X
⊢ s ∈ atInf ↔ ∃ r, {x | ‖x‖ > r} ⊆ s
Tactic:
simp only [Filter.hasBasis_iff.mp atInf_basis s, exists_true_left, true_and]
Proof state after:
no goals
Theorem: eventually_atInf
Proof state before:
X : Type
inst✝ : Norm X
r : ℝ
⊢ ∀ᶠ (x : X) in atInf, ‖x‖ > r
Tactic:
rw [Filter.eventually_iff, mem_atInf_iff]
Proof state after:
X : Type
inst✝ : Norm X
r : ℝ
⊢ ∃ r_1, {x | ‖x‖ > r_1} ⊆ {x | ‖x‖ > r}
Theorem: eventually_atInf
Proof state before:
X : Type
inst✝ : Norm X
r : ℝ
⊢ ∃ r_1, {x | ‖x‖ > r_1} ⊆ {x | ‖x‖ > r}
Tactic:
use r
Proof state after:
no goals
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ Tendsto f atInf l ↔ Tendsto (fun x => f x⁻¹) (𝓝[≠] 0) l
Tactic:
rw [Filter.HasBasis.tendsto_left_iff atInf_basis, Metric.nhdsWithin_basis_ball.tendsto_left_iff]
Proof state after:
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) ↔ ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) ↔ ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
constructor
Proof state after:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) → ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t) → ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) → ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
intro h t tl
Proof state after:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
rcases h t tl with ⟨r, _, m⟩
Proof state after:
case mp.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case mp.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
by_cases rp : 0 < r
Proof state after:
case pos
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

case neg
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case pos
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
use r⁻¹
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ 0 < r⁻¹ ∧ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ 0 < r⁻¹ ∧ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t
Tactic:
simp only [rp, inv_pos, true_and_iff]
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t
Tactic:
intro x xs
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t
Tactic:
refine m ?_
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [mem_inter_iff, mem_ball_zero_iff, mem_compl_iff, mem_singleton_iff] at xs
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : ‖x‖ < r⁻¹ ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : ‖x‖ < r⁻¹ ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [← lt_inv (norm_pos_iff.mpr xs.2) rp, xs.1, mem_setOf_eq, norm_inv]
Proof state after:
no goals
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case neg
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
use 1
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ 0 < 1 ∧ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t
Theorem: tendsto_atInf_iff_tendsto_nhds_zero
Proof state before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ 0 < 1 ∧ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t
Tactic:
simp only [zero_lt_one, true_and_iff]
Proof state after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t