90 lines
2.8 KiB
Text
90 lines
2.8 KiB
Text
|
-- actually it's analytical trigonometry
|
||
|
|
import Mathlib.Data.Real.Basic
|
||
|
|
import Mathlib.Tactic.LibrarySearch
|
||
|
|
|
||
|
|
axiom sin : Real → Real
|
||
|
|
axiom csc : Real → Real
|
||
|
|
|
||
|
|
axiom sin_eq_reciprocal_of_csc : ∀x, sin x = 1 / (csc x)
|
||
|
|
axiom csc_eq_reciprocal_of_sin : ∀x, csc x = 1 / (sin x)
|
||
|
|
|
||
|
|
axiom cos : Real → Real
|
||
|
|
axiom sec : Real → Real
|
||
|
|
|
||
|
|
axiom cos_eq_reciprocal_of_sec : ∀x, cos x = (sec x)⁻¹
|
||
|
|
axiom sec_eq_reciprocal_of_cos : ∀x, sec x = (cos x)⁻¹
|
||
|
|
|
||
|
|
@[simp]
|
||
|
|
noncomputable def tan (x : Real) : Real := sin x / cos x
|
||
|
|
theorem tan_def : ∀x, tan x = sin x / cos x := by simp
|
||
|
|
@[simp]
|
||
|
|
noncomputable def cot (x : Real) : Real := cos x / sin x
|
||
|
|
|
||
|
|
theorem tan_eq_sin_div_cos : ∀x, tan x = sin x / cos x := by simp
|
||
|
|
theorem cot_eq_cos_div_sin : ∀x, cot x = cos x / sin x := by simp
|
||
|
|
|
||
|
|
theorem tan_eq_reciprocal_of_cot : ∀x, tan x = 1 / (cot x) := by simp
|
||
|
|
theorem cot_eq_reciprocal_of_tan : ∀x, cot x = 1 / (tan x) := by simp
|
||
|
|
|
||
|
|
noncomputable def sin2 (x : Real) : Real := sin x * sin x
|
||
|
|
noncomputable def cos2 (x : Real) : Real := cos x * cos x
|
||
|
|
noncomputable def tan2 (x : Real) : Real := tan x * tan x
|
||
|
|
theorem tan2_def : ∀x, tan2 x = sin2 x / cos2 x := by
|
||
|
|
intro x
|
||
|
|
simp [tan2, sin2, cos2]
|
||
|
|
exact div_mul_div_comm (sin x) (cos x) (sin x) (cos x)
|
||
|
|
|
||
|
|
noncomputable def csc2 (x : Real) : Real := csc x * csc x
|
||
|
|
noncomputable def sec2 (x : Real) : Real := sec x * sec x
|
||
|
|
theorem sec2_eq_reciprocal_of_cos2 : ∀x, sec2 x = (cos2 x)⁻¹ := by
|
||
|
|
intro x
|
||
|
|
rw [sec2, cos2]
|
||
|
|
simp
|
||
|
|
rw [sec_eq_reciprocal_of_cos]
|
||
|
|
|
||
|
|
noncomputable def cot2 (x : Real) : Real := cot x * cot x
|
||
|
|
|
||
|
|
noncomputable def sin3 (x : Real) : Real := sin2 x * sin x
|
||
|
|
noncomputable def cos3 (x : Real) : Real := cos2 x * cos x
|
||
|
|
noncomputable def tan3 (x : Real) : Real := tan2 x * tan x
|
||
|
|
|
||
|
|
noncomputable def csc3 (x : Real) : Real := csc2 x * csc x
|
||
|
|
noncomputable def sec3 (x : Real) : Real := sec2 x * sec x
|
||
|
|
noncomputable def cot3 (x : Real) : Real := cot2 x * cot x
|
||
|
|
|
||
|
|
@[simp]
|
||
|
|
axiom pyth_id : ∀x, sin2 x + cos2 x = 1
|
||
|
|
|
||
|
|
theorem sin_squared_eq {x : Real} : sin2 x = 1 - cos2 x := by
|
||
|
|
rw [← add_left_inj (cos2 x)]
|
||
|
|
rw [sub_add_cancel]
|
||
|
|
exact pyth_id x
|
||
|
|
|
||
|
|
theorem cos_squared_eq {x : Real} : cos2 x = 1 - sin2 x := by
|
||
|
|
rw [← add_left_inj (sin2 x)]
|
||
|
|
rw [sub_add_cancel]
|
||
|
|
rw [add_comm]
|
||
|
|
exact pyth_id x
|
||
|
|
|
||
|
|
theorem bleh {a b c : Real} (d : Real) : a + b = c → a / d + b / d = c / d := by
|
||
|
|
intro h
|
||
|
|
rw [← add_div, h]
|
||
|
|
|
||
|
|
def tan_pyth_id : ∀x, cos2 x ≠ 0 → tan2 x + 1 = sec2 x := by
|
||
|
|
intro x
|
||
|
|
intro hnz
|
||
|
|
have h := pyth_id x
|
||
|
|
have h : sin2 x / cos2 x + cos2 x / cos2 x = 1 / cos2 x :=
|
||
|
|
bleh (cos2 x) h
|
||
|
|
|
||
|
|
rw [← tan2_def] at h
|
||
|
|
simp at h
|
||
|
|
rw [← sec2_eq_reciprocal_of_cos2, div_self] at h
|
||
|
|
exact h
|
||
|
|
exact hnz
|
||
|
|
|
||
|
|
example (x : Real) : 2 * (1 / (csc x)) = 2 * (sin x) := by
|
||
|
|
rw [sin_eq_reciprocal_of_csc]
|
||
|
|
|
||
|
|
--todo evens and odds and the sin/cos (a ± b) ones
|