`spatialRadius_pos_of_ne_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Calculus.Derivatives
domain: Relativity
line: 162 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Calculus.Derivatives on GitHub at line 162.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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)
 166
 167/-- Temporal coordinate ray doesn't change spatial components. -/
 168lemma coordRay_temporal_spatial (x : Fin 4 → ℝ) (s : ℝ) (i : Fin 4) (hi : i ≠ 0) :
 169    (coordRay x 0 s) i = x i := by
 170  simp [coordRay, basisVec, hi]
 171
 172/-- spatialNormSq is invariant under temporal coordinate ray. -/
 173lemma spatialNormSq_coordRay_temporal (x : Fin 4 → ℝ) (s : ℝ) :
 174    spatialNormSq (coordRay x 0 s) = spatialNormSq x := by
 175  unfold spatialNormSq
 176  have h1 : (coordRay x 0 s) 1 = x 1 := coordRay_temporal_spatial x s 1 (by decide)
 177  have h2 : (coordRay x 0 s) 2 = x 2 := coordRay_temporal_spatial x s 2 (by decide)
 178  have h3 : (coordRay x 0 s) 3 = x 3 := coordRay_temporal_spatial x s 3 (by decide)
 179  rw [h1, h2, h3]
 180
 181/-- spatialRadius is invariant under temporal coordinate ray. -/
 182lemma spatialRadius_coordRay_temporal (x : Fin 4 → ℝ) (s : ℝ) :
 183    spatialRadius (coordRay x 0 s) = spatialRadius x := by
 184  unfold spatialRadius
 185  rw [spatialNormSq_coordRay_temporal]
 186
 187/-- For any spatial index `i ∈ {1,2,3}`, `x_i² ≤ spatialNormSq x`. -/
 188private lemma sq_le_spatialNormSq_1 (x : Fin 4 → ℝ) :
 189    x 1 ^ 2 ≤ spatialNormSq x := by
 190  unfold spatialNormSq; nlinarith [sq_nonneg (x 2), sq_nonneg (x 3)]
 191
 192private lemma sq_le_spatialNormSq_2 (x : Fin 4 → ℝ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.