spatialNormSq_eq_zero_iff

formal source

 132  unfold spatialNormSq
 133  positivity
 134
 135theorem spatialNormSq_eq_zero_iff (x : Fin 4 → ℝ) : spatialNormSq x = 0 ↔ x 1 = 0 ∧ x 2 = 0 ∧ x 3 = 0 := by
 136  unfold spatialNormSq
 137  constructor
 138  · intro h
 139    have h1 := sq_nonneg (x 1)
 140    have h2 := sq_nonneg (x 2)
 141    have h3 := sq_nonneg (x 3)
 142    have h1_zero : x 1 ^ 2 = 0 := by linarith
 143    have h2_zero : x 2 ^ 2 = 0 := by linarith
 144    have h3_zero : x 3 ^ 2 = 0 := by linarith
 145    simp only [sq_eq_zero_iff] at h1_zero h2_zero h3_zero
 146    exact ⟨h1_zero, h2_zero, h3_zero⟩
 147  · intro h
 148    simp [h]
 149
 150/-- Spatial radius `r = √(x₁² + x₂² + x₃²)`. -/
 151noncomputable def spatialRadius (x : Fin 4 → ℝ) : ℝ := Real.sqrt (spatialNormSq x)
 152
 153theorem spatialRadius_pos_iff (x : Fin 4 → ℝ) : 0 < spatialRadius x ↔ 0 < spatialNormSq x := by
 154  unfold spatialRadius
 155  rw [Real.sqrt_pos]
 156
 157theorem spatialRadius_ne_zero_iff (x : Fin 4 → ℝ) : spatialRadius x ≠ 0 ↔ spatialNormSq x ≠ 0 := by
 158  unfold spatialRadius
 159  rw [Real.sqrt_ne_zero (spatialNormSq_nonneg x)]
 160
 161/-- Nonzero spatial radius is automatically positive. -/
 162theorem spatialRadius_pos_of_ne_zero (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
 163    0 < spatialRadius x := by
 164  have h_ne : spatialNormSq x ≠ 0 := (spatialRadius_ne_zero_iff x).mp hx
 165  exact (spatialRadius_pos_iff x).2 (lt_of_le_of_ne (spatialNormSq_nonneg x) h_ne.symm)