spatialRadius_coordRay_ne_zero_proved

proof body

Tactic-mode proof.

  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) =
  69      spatialNormSq x +
  70      2 * s * (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩) +
  71      s ^ 2 * (∑ i : Fin 3, (basisVec ν ⟨i.val + 1, by omega⟩) ^ 2) := by
  72    unfold spatialNormSq coordRay basisVec
  73    ring
  74  -- The cross-term A = ∑ x_i δ_{iν} = x ν if ν ∈ {1,2,3}, else 0
  75  -- Bound: |A| ≤ spatialRadius x (by Cauchy-Schwarz in ℝ³)
  76  -- The quadratic term B = |basisVec ν|² ≥ 0
  77  -- Lower bound: spatialNormSq(coordRay x ν s) ≥ r² - 2|s|*r + 0
  78  -- = r(r - 2|s|) > 0 when |s| < r/2
  79  have h_A_bound : |∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ *
  80        basisVec ν ⟨i.val + 1, by omega⟩| ≤ spatialRadius x := by
  81    calc |∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩|
  82        ≤ ∑ i : Fin 3, |x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩| :=
  83          Finset.abs_sum_le_sum_abs _ _
  84      _ ≤ ∑ i : Fin 3, (|x ⟨i.val + 1, by omega⟩| * 1) := by
  85          apply Finset.sum_le_sum
  86          intro i _
  87          rw [abs_mul]
  88          apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)
  89          unfold basisVec
  90          split_ifs <;> simp [abs_le, le_refl]
  91      _ = ∑ i : Fin 3, |x ⟨i.val + 1, by omega⟩| := by simp [mul_one]
  92      _ ≤ spatialRadius x := by
  93          have : spatialRadius x = Real.sqrt (spatialNormSq x) := rfl
  94          rw [this]
  95          calc ∑ i : Fin 3, |x ⟨i.val + 1, by omega⟩|
  96              ≤ Real.sqrt (3 * spatialNormSq x) := by
  97                apply le_trans (Finset.sum_le_card_nsmul _ _ (spatialRadius x) _)
  98                · intro i _
  99                  apply abs_le_of_sq_le_sq (spatialRadius x) (le_of_lt hr_pos)
 100                  rw [this, Real.sq_sqrt (spatialNormSq_nonneg x)]
 101                  unfold spatialNormSq
 102                  have hi : (i : Fin 4) = ⟨i.val + 1, by omega⟩ := by ext; simp
 103                  calc x ⟨i.val + 1, by omega⟩ ^ 2
 104                      ≤ x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 := by nlinarith [sq_nonneg (x 1), sq_nonneg (x 2), sq_nonneg (x 3), sq_nonneg (x ⟨i.val + 1, by omega⟩)]
 105                · simp [Finset.card_fin]
 106                  nlinarith [Real.sq_sqrt (spatialNormSq_nonneg x), hr_pos]
 107            _ ≤ Real.sqrt (spatialNormSq x) := by
 108                apply Real.sqrt_le_sqrt
 109                nlinarith [spatialNormSq_nonneg x]
 110  have h_B_nonneg : 0 ≤ ∑ i : Fin 3, (basisVec ν ⟨i.val + 1, by omega⟩) ^ 2 := by
 111    apply Finset.sum_nonneg; intro i _; exact sq_nonneg _
 112  rw [h_expand]
 113  have h_lower : spatialNormSq x + 2 * s *
 114      (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩) +
 115      s ^ 2 * (∑ i : Fin 3, (basisVec ν ⟨i.val + 1, by omega⟩) ^ 2) ≥
 116      spatialNormSq x - 2 * |s| * spatialRadius x := by
 117    nlinarith [mul_nonneg h_B_nonneg (sq_nonneg s),
 118               mul_comm s (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩),
 119               abs_mul s (∑ i : Fin 3, x ⟨i.val + 1, by omega⟩ * basisVec ν ⟨i.val + 1, by omega⟩),
 120               neg_abs_le s (by exact rfl) |>.le]
 121  linarith [mul_pos (by linarith [hs] : 0 < spatialRadius x - 2 * |s|) hr_pos,
 122-- ... 8 more lines elided ...