x_reciprocity_identity

formal source

  18    then a * ∂Q/∂a = - k * ∂Q/∂k.
  19
  20    This is the derivative form of ∂lnQ/∂lna = -∂lnQ/∂lnk. -/
  21theorem x_reciprocity_identity (tau0 : ℝ) (Q_tilde : ℝ → ℝ)
  22    (a k : ℝ) (ha : a ≠ 0) (hk : k ≠ 0)
  23    (hQ : DifferentiableAt ℝ Q_tilde (X_var k a tau0)) :
  24    let Q := fun (a k : ℝ) => Q_tilde (X_var k a tau0)
  25    a * (deriv (fun a' => Q a' k) a) = - (k * (deriv (fun k' => Q a k') k)) := by
  26  set X := X_var k a tau0
  27  let f_a := fun a' => Q_tilde (X_var k a' tau0)
  28  let f_k := fun k' => Q_tilde (X_var k' a tau0)
  29
  30  -- Partial with respect to a
  31  have h_deriv_a : deriv f_a a = deriv Q_tilde X * (-(k * tau0) / a^2) := by
  32    rw [show f_a = Q_tilde ∘ (fun a' => (k * tau0) / a') by funext a'; rfl]
  33    have h_inner : DifferentiableAt ℝ (fun a' => (k * tau0) / a') a := by
  34      apply DifferentiableAt.const_div
  35      · exact differentiableAt_id'
  36      · exact ha
  37    rw [deriv_comp a hQ h_inner]
  38    congr
  39    rw [deriv_const_div (k * tau0) differentiableAt_id' ha]
  40    simp
  41    ring
  42
  43  -- Partial with respect to k
  44  have h_deriv_k : deriv f_k k = deriv Q_tilde X * (tau0 / a) := by
  45    rw [show f_k = Q_tilde ∘ (fun k' => (k' * tau0) / a) by funext k'; rfl]
  46    have h_inner : DifferentiableAt ℝ (fun k' => (k' * tau0) / a) k := by
  47      apply DifferentiableAt.div_const
  48      apply DifferentiableAt.mul_const
  49      exact differentiableAt_id'
  50    rw [deriv_comp k hQ h_inner]
  51    congr