PhiPow_zero

formal source

  72            / Real.exp (Real.log (Constants.phi) * y) := by
  73              simp [div_eq_mul_inv]
  74
  75@[simp] lemma PhiPow_zero : PhiPow 0 = 1 := by
  76  unfold PhiPow; simp
  77
  78@[simp] lemma PhiPow_one : PhiPow 1 = Constants.phi := by
  79  unfold PhiPow
  80  have hφ : 0 < Constants.phi := Constants.phi_pos
  81  simp [one_mul, Real.exp_log hφ]
  82
  83@[simp] lemma PhiPow_neg (y : ℝ) : PhiPow (-y) = 1 / PhiPow y := by
  84  have := PhiPow_sub 0 y
  85  simp [PhiPow_zero, sub_eq_add_neg] at this
  86  simpa using this
  87
  88@[simp] noncomputable def lambdaA : ℝ := Real.log Constants.phi
  89@[simp] noncomputable def kappaA  : ℝ := Constants.phi
  90
  91@[simp] noncomputable def F_ofZ (Z : ℤ) : ℝ := (Real.log (1 + (Z : ℝ) / kappaA)) / lambdaA
  92
  93@[simp] def Z_quark (Q : ℤ) : ℤ := 4 + (6 * Q) ^ (2 : Nat) + (6 * Q) ^ (4 : Nat)
  94@[simp] def Z_lepton (Q : ℤ) : ℤ := (6 * Q) ^ (2 : Nat) + (6 * Q) ^ (4 : Nat)
  95@[simp] def Z_neutrino : ℤ := 0
  96
  97lemma kappaA_pos : 0 < kappaA := by
  98  unfold kappaA; simpa using Constants.phi_pos
  99
 100lemma lambdaA_ne_zero : lambdaA ≠ 0 := by
 101  have hpos : 0 < Constants.phi := Constants.phi_pos
 102  have hne1 : Constants.phi ≠ 1 := Constants.phi_ne_one
 103  simpa [lambdaA] using Real.log_ne_zero_of_pos_of_ne_one hpos hne1
 104
 105lemma kappaA_ne_zero : kappaA ≠ 0 := by