Theory Poincare

theory Poincare
  imports Complex_Main "HOL-Analysis.Inner_Product" GammaFactor
begin

typedef PoincareDisc = "{z::complex. cmod z < 1}"
  by (rule exI [where x=0], auto)

setup_lifting type_definition_PoincareDisc

abbreviation to_complex :: "PoincareDisc ⇒ complex" where 
  "to_complex ≡ Rep_PoincareDisc" 
abbreviation of_complex :: "complex ⇒ PoincareDisc" where 
  "of_complex ≡ Abs_PoincareDisc" 

lemma poincare_disc_two_elems:
  shows "∃ z1 z2::PoincareDisc. z1 ≠ z2"
proof-
  have "cmod 0 < 1"
    by simp
  moreover
  have "cmod (1/2) < 1"
    by simp
  moreover
  have "(0::complex) ≠ 1/2"
    by simp
  ultimately
  show ?thesis
    by transfer blast
qed

lift_definition inner_p :: "PoincareDisc ⇒ PoincareDisc ⇒ real" (infixl "⋅" 100) is inner .

lift_definition norm_p :: "PoincareDisc ⇒ real"  ("⟪_⟫" [100] 101) is norm .

lemma norm_lt_one:
  shows "⟪u⟫ < 1"
  by transfer simp

lemma norm_geq_zero:
  shows "⟪u⟫ ≥ 0"
  by transfer simp

lemma square_norm_inner:
  shows "(⟪u⟫)⇧2 = u ⋅ u"
  by transfer (simp add: dot_square_norm)

lift_definition gammma_factor_p :: "PoincareDisc ⇒ real" ("γ⇩p") is gamma_factor .

lemma gamma_factor_p_nonzero [simp]:
  shows "γ⇩p u ≠ 0"
  apply transfer
  unfolding gamma_factor_def
  using gamma_factor_nonzero
  by auto

lemma gamma_factor_p_positive [simp]:
  shows "γ⇩p u > 0"
  by transfer (simp add: gamma_factor_positive)

lemma norm_square_gamma_factor_p:
  shows "(⟪u⟫)^2 = 1 - 1 / (γ⇩p u)^2"
  by transfer (simp add: norm_square_gamma_factor)

lemma norm_square_gamma_factor_p':
  shows "(⟪u⟫)^2 = ((γ⇩p u)^2 - 1) / (γ⇩p u)^2"
  by transfer (simp add: norm_square_gamma_factor')

lemma gamma_factor_p_square_norm:
  shows "(γ⇩p u)⇧2 = 1 / (1 - (⟪u⟫)⇧2)"
  by transfer (simp add: gamma_factor_square_norm)

end