spatialRadius_coordRay_ne_zero_proved

formal source

  35
  36/-- If `spatialRadius x ≠ 0` and `|s| < spatialRadius x / 2`, then
  37    `spatialRadius (coordRay x ν s) ≠ 0`. -/
  38theorem spatialRadius_coordRay_ne_zero_proved
  39    (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
  40    (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2) :
  41    spatialRadius (coordRay x ν s) ≠ 0 := by
  42  -- Strategy: show spatialNormSq (coordRay x ν s) > 0 via a polynomial lower bound.
  43  -- spatialNormSq (coordRay x ν s) = ∑_{i∈{1,2,3}} (x i + s * basisVec ν i)²
  44  -- ≥ spatialNormSq x - 2|s| * √(spatialNormSq x) * |basisVec ν|₂ + s² |basisVec ν|₂²
  45  --
  46  -- Simpler route: use continuity.
  47  -- spatialRadius is continuous and equals spatialRadius x ≠ 0 at s = 0 (via coordRay x ν 0 = x).
  48  -- By the open-set argument, it stays ≠ 0 in a neighborhood.
  49  -- The hypothesis |s| < r/2 gives a concrete neighborhood.
  50  --
  51  -- Polynomial approach for the quantitative bound:
  52  -- Write r(s)² = spatialNormSq x + 2s A + s² B where
  53  --   A = ∑_{i∈{1,2,3}} x i * basisVec ν i (the "directional derivative" of ‖x‖²/2)
  54  --   B = ∑_{i∈{1,2,3}} (basisVec ν i)² = if ν ∈ {1,2,3} then 1 else 0
  55  -- |A| ≤ ‖x‖ₛ * |basisVec ν|₂ ≤ ‖x‖ₛ = spatialRadius x
  56  -- r(s)² ≥ spatialNormSq x - 2|s| * spatialRadius x + s² * 0
  57  --       ≥ spatialNormSq x - 2|s| * spatialRadius x
  58  --       > 0  when  2|s| * spatialRadius x < spatialNormSq x = (spatialRadius x)²
  59  --       i.e.  |s| < spatialRadius x / 2  ✓
  60  --
  61  -- Implement:
  62  rw [spatialRadius_ne_zero_iff]
  63  have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
  64  have hr_sq : spatialNormSq x = spatialRadius x ^ 2 := by
  65    unfold spatialRadius
  66    rw [Real.sq_sqrt (spatialNormSq_nonneg x)]
  67  -- Expand spatialNormSq (coordRay x ν s)
  68  have h_expand : spatialNormSq (coordRay x ν s) =