X_var

formal source

   7open Real
   8
   9/-- The ILG dimensionless variable X = k * tau0 / a. -/
  10noncomputable def X_var (k a tau0 : ℝ) : ℝ := (k * tau0) / a
  11
  12/-- A function Q(a, k) satisfies X-reciprocity if there exists a function Q_tilde
  13    such that Q(a, k) = Q_tilde (X_var k a tau0). -/
  14def HasXReciprocity (Q : ℝ → ℝ → ℝ) (tau0 : ℝ) : Prop :=
  15  ∃ Q_tilde : ℝ → ℝ, ∀ a k, Q a k = Q_tilde (X_var k a tau0)
  16
  17/-- The X-reciprocity identity: if Q depends only on X = k*tau0/a,
  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