partialDeriv_v2_radialInv

proof body

Tactic-mode proof.

 512  unfold partialDeriv_v2 radialInv
 513  by_cases hμ : μ = 0
 514  · simp only [hμ, ↓reduceIte]
 515    have h : ∀ t, spatialRadius (coordRay x 0 t) = spatialRadius x :=
 516      spatialRadius_coordRay_temporal x
 517    have h2 : (fun t => 1 / spatialRadius (coordRay x 0 t) ^ n) =
 518              (fun _ => 1 / spatialRadius x ^ n) := by
 519      funext t; rw [h]
 520    simp_rw [h2]; exact deriv_const 0 _
 521  · simp only [hμ, ↓reduceIte]
 522    cases n with
 523    | zero => simp
 524    | succ k =>
 525      have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
 526      have h_r_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 :=
 527        differentiableAt_coordRay_spatialRadius x μ hx
 528      have h_r_pow_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t) ^ (k + 1)) 0 :=
 529        h_r_da.pow (k + 1)
 530      have h_r_pow_ne : spatialRadius (coordRay x μ 0) ^ (k + 1) ≠ 0 := by
 531        simp only [coordRay_zero]
 532        exact pow_ne_zero (k + 1) hx
 533      have h_r_deriv : deriv (fun t => spatialRadius (coordRay x μ t)) 0 = x μ / spatialRadius x := by
 534        have := partialDeriv_v2_spatialRadius μ x hx
 535        simp only [partialDeriv_v2, hμ, ↓reduceIte] at this
 536        exact this
 537      have h_r_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t)) (x μ / spatialRadius x) 0 := by
 538        have : HasDerivAt (fun t => spatialRadius (coordRay x μ t))
 539            (deriv (fun t => spatialRadius (coordRay x μ t)) 0) 0 := h_r_da.hasDerivAt
 540        simpa [h_r_deriv] using this
 541      have h_rpow_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t) ^ (k + 1))
 542          (↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) 0 := by
 543        have h1 := h_r_hda.pow (k + 1)
 544        simp only [coordRay_zero] at h1
 545        convert h1 using 2
 546      have h_rinv_hda : HasDerivAt (fun t => (spatialRadius (coordRay x μ t) ^ (k + 1))⁻¹)
 547          (-(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) /
 548             (spatialRadius x ^ (k + 1)) ^ 2) 0 := by
 549        have h2 := h_rpow_hda.inv h_r_pow_ne
 550        simp only [coordRay_zero] at h2
 551        exact h2
 552      have h_inv : (fun t => 1 / spatialRadius (coordRay x μ t) ^ (k + 1)) = fun t => (spatialRadius (coordRay x μ t) ^ (k + 1))⁻¹ := by funext t; exact one_div _
 553      rw [h_inv, h_rinv_hda.deriv]
 554      have hr_ne : spatialRadius x ≠ 0 := hx
 555      have h_pow1 : (spatialRadius x ^ (k + 1)) ^ 2 = spatialRadius x ^ (2 * k + 2) := by
 556        rw [← pow_mul]; congr 1; omega
 557      have h_pow2 : k + 1 + 2 = k + 3 := by omega
 558      rw [div_eq_div_iff]
 559      · change -(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) * spatialRadius x ^ (k + 1 + 2) = -↑(k + 1) * x μ * (spatialRadius x ^ (k + 1)) ^ 2
 560        rw [h_pow1]
 561        rw [h_pow2]
 562        calc -(↑(k + 1) * spatialRadius x ^ k * (x μ / spatialRadius x)) * spatialRadius x ^ (k + 3)
 563          _ = -(↑(k + 1) * spatialRadius x ^ k * (x μ * (spatialRadius x)⁻¹)) * spatialRadius x ^ (k + 3) := by rw [div_eq_mul_inv]
 564          _ = -↑(k + 1) * x μ * (spatialRadius x ^ k * (spatialRadius x)⁻¹ * spatialRadius x ^ (k + 3)) := by ring
 565          _ = -↑(k + 1) * x μ * (spatialRadius x ^ k * spatialRadius x ^ (k + 3) * (spatialRadius x)⁻¹) := by ring
 566          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 3) * (spatialRadius x)⁻¹) := by
 567            have : spatialRadius x ^ k * spatialRadius x ^ (k + 3) = spatialRadius x ^ (2 * k + 3) := by rw [← pow_add]; congr 1; omega
 568            rw [this]
 569          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * spatialRadius x * (spatialRadius x)⁻¹) := by
 570            have : spatialRadius x ^ (2 * k + 2) * spatialRadius x = spatialRadius x ^ (2 * k + 3) := by
 571              calc spatialRadius x ^ (2 * k + 2) * spatialRadius x
 572                _ = spatialRadius x ^ (2 * k + 2) * spatialRadius x ^ 1 := by rw [pow_one]
 573                _ = spatialRadius x ^ (2 * k + 2 + 1) := by rw [← pow_add]
 574                _ = spatialRadius x ^ (2 * k + 3) := by rfl
 575            rw [← this]
 576          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * (spatialRadius x * (spatialRadius x)⁻¹)) := by ring
 577          _ = -↑(k + 1) * x μ * (spatialRadius x ^ (2 * k + 2) * 1) := by rw [mul_inv_cancel₀ hr_ne]
 578          _ = -↑(k + 1) * x μ * spatialRadius x ^ (2 * k + 2) := by ring
 579      · exact pow_ne_zero 2 (pow_ne_zero (k + 1) hr_ne)
 580      · exact pow_ne_zero (k + 1 + 2) hr_ne
 581
 582/-- Differentiability of `s ↦ ∂(1/r^n)/∂x_μ` along a coordinate ray.
 583
 584    For temporal direction (μ = 0), `partialDeriv_v2 (radialInv n) 0 y = 0` whenever
 585    `spatialRadius y ≠ 0`, so the function is locally constant 0 near `s = 0`.
 586
 587    For spatial direction (μ ≠ 0), `partialDeriv_v2 (radialInv n) μ y =
 588    -n · y_μ / r(y)^(n+2)` whenever `spatialRadius y ≠ 0`, so the function is
 589    locally a quotient of differentiable functions:
 590    - numerator `s ↦ -n · (coordRay x ν s)_μ` is linear in `s`
 591    - denominator `s ↦ r(coordRay x ν s)^(n+2)` is the `(n+2)`-power of the
 592-- ... 5 more lines elided ...