Created
March 2, 2024 20:52
-
-
Save brando90/0786c13414a510d4652351a2d96b51fc to your computer and use it in GitHub Desktop.
vertical_asymptote_of_1_over_x.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- | |
-/ | |
import Mathlib.Data.Real.Basic | |
-- define 1/x (reciprical) for reals | |
noncomputable def f (x : ℝ ): ℝ := x⁻¹ | |
#check f | |
-- unit test that f 1 = 1, f 2 = 1/2 | |
theorem test_f1 : f 1 = 1 := by simp[f] | |
theorem test_f2 : f 2 = 2⁻¹ := by simp[f] | |
#print test_f1 | |
#print test_f2 | |
-- set_option pp.notation false | |
-- The limit of f x as x approaches c+ from the right is +infinity i.e., limit is unbounded from the right | |
-- i.e., lim_{x -> c+} f(x) = +infinity | |
def has_unbounded_limit_right (f: ℝ -> ℝ) (c : ℝ) : Prop := | |
∀ M : ℝ, 0 < M → ∃ δ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x | |
#print has_unbounded_limit_right | |
theorem reciprocal_has_unbounded_limit_right : has_unbounded_limit_right f 0 := by | |
unfold has_unbounded_limit_right | |
intro M h_0_lt_M | |
-- select delta that works since func is 1/x then anything less than 1/M will make f x be greater than M (so it should work) | |
use M⁻¹ | |
-- TODO split (what did scott want with this, read) | |
constructor | |
. rwa [inv_pos] | |
. -- consider any x with 0 < x - 0 < M⁻¹ but introduce both hypothesis 0 < x - 0 and x - 0 < M⁻¹ | |
intro x ⟨h_x_pos, h_x_lt_δ⟩ | |
-- rintro x ⟨h_x_pos, h_x_lt_δ⟩ -- TODO tomorrow, why did scott do this? | |
-- rewrite both hypothesis using fact m - 0 = m | |
rw [sub_zero] at h_x_pos h_x_lt_δ | |
unfold f | |
-- multiply both sides of h_x_lt_δ by x⁻¹ on the left using mul_lt_mul_right | |
rwa [propext (lt_inv h_0_lt_M h_x_pos)] | |
-- def F {α : Type} (p : α -> Prop) : Prop := p | |
-- #eval F ℝ (fun x => 0 < x) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment