Theory GammaFactor

theory GammaFactor
  imports Complex_Main MoreComplex
begin

definition gamma_factor :: "'a::real_inner ⇒ real" ("γ") where
  "γ u = (if norm u < 1 then 
             1 / sqrt (1 - (norm u)⇧2)
          else
             0)"

lemma gamma_factor_nonzero:
  assumes "norm u < 1"
  shows "1 / sqrt (1 - (norm u)⇧2) ≠ 0"
  using assms square_norm_one by force

lemma gamma_factor_increasing:
  fixes t1 t2 ::real
  assumes "0 ≤ t2" "t2 < t1" "t1 < 1"
  shows "γ t2 < γ t1"
proof-
  have d: "cmod t1 = abs t1" "cmod t2 = abs t2"
    using norm_of_real 
    by blast+

  have "¦t2¦ * ¦t2¦ < ¦t1¦ * ¦t1¦"
    by (simp add: assms mult_strict_mono')
  then have "1 - ¦t1¦ * ¦t1¦ < 1 - ¦t2¦ * ¦t2¦"
    by auto
  then have "sqrt (1 - ¦t1¦ * ¦t1¦) < sqrt (1 - ¦t2¦ * ¦t2¦)"
    using real_sqrt_less_iff 
    by blast
  then have "1 / sqrt (1 - ¦t2¦ * ¦t2¦) < 1 / sqrt (1 - ¦t1¦ * ¦t1¦)"
    using assms
    by (smt (z3) frac_less2 mult_less_cancel_right2 real_sqrt_gt_zero)

  moreover

  have "norm t1 < 1" "norm t2 < 1"
    using assms 
    by force+
  then have "γ t1 = 1 / sqrt(1 - (abs t1)^2)" "γ t2 = 1 / sqrt(1 - (abs t2)^2)"
    using assms d 
    unfolding gamma_factor_def
    by auto

  ultimately

  show ?thesis
    using d 
    by (metis power2_eq_square)
qed

lemma gamma_factor_increase_reverse:
  fixes t1 t2 :: real
  assumes "t1 ≥ 0" "t1 < 1" "t2 ≥ 0" "t2 < 1"
  assumes "γ t1 > γ t2"
  shows "t1 > t2"
  using assms
  by (smt (verit, best) gamma_factor_increasing)
  
lemma gamma_factor_u_normu:
  fixes u :: real
  assumes "0 ≤ u" "u ≤ 1"
  shows "γ u = γ (norm u)"
  unfolding gamma_factor_def
  by auto

lemma gamma_factor_positive:
  assumes "norm u < 1"
  shows "γ u > 0"
  using assms
  unfolding gamma_factor_def
  by (smt (verit, del_insts) divide_pos_pos norm_ge_zero power2_eq_square power2_nonneg_ge_1_iff real_sqrt_gt_0_iff)

lemma norm_square_gamma_factor:
  assumes "norm u < 1"
  shows "(norm u)^2 = 1 - 1 / (γ u)^2"
proof-
  have "γ u = 1 / sqrt (1 - (norm u)^2)"
    by (metis assms gamma_factor_def)
  then have "(γ u)^2 = 1 / (1 - (norm u)^2)"
    using assms
    by (metis abs_power2 gamma_factor_positive less_eq_real_def norm_ge_zero norm_power power2_eq_imp_eq real_norm_def real_sqrt_abs real_sqrt_divide real_sqrt_eq_1_iff real_sqrt_eq_iff)
  then show ?thesis 
    by auto
qed

lemma norm_square_gamma_factor':
  assumes "norm u < 1"
  shows "(norm u)^2 = ((γ u)^2 - 1) / (γ u)^2"
  using norm_square_gamma_factor[OF assms]
  by (metis assms diff_divide_distrib div_self gamma_factor_positive norm_not_less_zero norm_zero power_not_zero)


lemma gamma_factor_square_norm:
  assumes "norm u < 1"
  shows "(γ u)⇧2 = 1 / (1 - (norm u)⇧2)"
  by (smt (verit) assms gamma_factor_def gamma_factor_positive real_sqrt_divide real_sqrt_eq_iff real_sqrt_one real_sqrt_unique)

lemma gamma_expression_eq_one_1:
  assumes "norm u < 1" 
  shows "1 / γ u + (γ u * (norm u)^2) / (1 + γ u) = 1"
proof-
  have "γ u ≠ 0" "1 + γ u ≠ 0"
    using assms gamma_factor_positive 
    by fastforce+

  have "1 / γ u + γ u * (norm u)^2 / (1 + γ u) =
        (1 + γ u + (γ u)^2 * (norm u)^2) / (γ u * (1 + γ u))"
    using ‹γ u ≠ 0› ‹1 + γ u ≠ 0›
    by (metis (no_types, lifting) add_divide_distrib nonzero_divide_mult_cancel_right nonzero_mult_divide_mult_cancel_left numeral_One power_add_numeral2 power_one_right semiring_norm(2))
  also have "… = (1 + γ u + (γ u)^2 * (1 - 1 / ((γ u)^2))) / (γ u * (1 + γ u))"
    by (simp add: assms norm_square_gamma_factor)
  also have "… = (1 + γ u + (γ u)^2 - 1) / (γ u * (1 + γ u))"
    by (simp add: Rings.ring_distribs(4))
  also have "... = (γ u * (1 + γ u)) / (γ u * (1 + γ u))"
    by (simp add: power2_eq_square ring_class.ring_distribs(1))
  finally show ?thesis
    using ‹γ u ≠ 0› ‹1 + γ u ≠ 0›
    by (metis div_by_1 divide_divide_eq_right eq_divide_eq_1)
qed

lemma gamma_expression_eq_one_2:
  assumes "norm u < 1"
  shows "((γ u)^2 * (norm u)^2) / (1 + γ u)^2 + (2 * γ u) / (γ u * (1 + γ u)) = 1"
proof-
  have *: "γ u ≠ 0" "1 + γ u ≠ 0"
    using assms gamma_factor_positive
    by force+

  have "((γ u)^2 * (norm u)^2) / (1 + γ u)^2 + (2 * γ u) / (γ u * (1 + γ u)) = 
        ((γ u)^2 * (1 - 1 / (γ u)^2)) / (1 + γ u)^2 + (2 * γ u) / (γ u * (1 + γ u))"
    using norm_square_gamma_factor[OF assms]
    by presburger
  also have "… = ((γ u)^2 - 1) / (1 + γ u)^2 + (2 * γ u) / (γ u * (1 + γ u))"
    using ‹γ u ≠ 0›
    by (simp add: right_diff_distrib)
  also have "… = (γ u * ((γ u)^2 - 1)) / (γ u * (1 + γ u)^2) + (2 * γ u * (1 + γ u)) / (γ u * (1 + γ u)^2)"
    using ‹γ u ≠ 0›
    by (simp add: mult.commute power2_eq_square)
  also have "… = (γ u * ((γ u)^2 - 1) + 2 * γ u * (1 + γ u)) / (γ u * (1 + γ u)^2)"
    by argo
  also have "… = ((γ u)^3 + γ u + 2 * (γ u)^2) / (γ u * (1 + γ u)^2)"
    by (simp add: power2_eq_square power3_eq_cube right_diff_distrib ring_class.ring_distribs(1))
  also have "… = (γ u * (1 + γ u) ^ 2) / (γ u * (1 + γ u)^2)"
    by (simp add: field_simps power2_eq_square power3_eq_cube)
  finally show ?thesis 
    using *
    by simp
qed


end