hbar_derived_pos

formal source

 109
 110def hbar_derived (τ G_val c_val : ℝ) : ℝ := Real.pi * c_val ^ 5 * τ ^ 2 / G_val
 111
 112lemma hbar_derived_pos (τ G_val c_val : ℝ) (hτ : 0 < τ) (hG : 0 < G_val) (hc : 0 < c_val) :
 113    0 < hbar_derived τ G_val c_val := by
 114  unfold hbar_derived
 115  apply div_pos _ hG
 116  exact mul_pos (mul_pos Real.pi_pos (pow_pos hc 5)) (sq_pos_of_pos hτ)
 117
 118/-- **Theorem**: hbar_derived tau0 G_codata c_codata = hbar_codata -/
 119theorem planck_relation_satisfied :
 120    hbar_derived tau0 G_codata c_codata = hbar_codata := by
 121  unfold hbar_derived
 122  rw [tau0_sq_eq]
 123  have hG : G_codata ≠ 0 := G_codata_ne_zero
 124  have hc : c_codata ≠ 0 := c_codata_ne_zero
 125  have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
 126  have hc5 : c_codata ^ 5 ≠ 0 := pow_ne_zero 5 hc
 127  field_simp
 128
 129def G_derived (τ hbar_val c_val : ℝ) : ℝ := Real.pi * c_val ^ 5 * τ ^ 2 / hbar_val
 130
 131lemma G_derived_pos (τ hbar_val c_val : ℝ) (hτ : 0 < τ) (hℏ : 0 < hbar_val) (hc : 0 < c_val) :
 132    0 < G_derived τ hbar_val c_val := by
 133  unfold G_derived
 134  apply div_pos _ hℏ
 135  exact mul_pos (mul_pos Real.pi_pos (pow_pos hc 5)) (sq_pos_of_pos hτ)
 136
 137/-- **Theorem**: G_derived tau0 hbar_codata c_codata = G_codata -/
 138theorem G_relation_satisfied :
 139    G_derived tau0 hbar_codata c_codata = G_codata := by
 140  unfold G_derived
 141  rw [tau0_sq_eq]
 142  have hℏ : hbar_codata ≠ 0 := hbar_codata_ne_zero