IndisputableMonolith.ILG.Reciprocity

   1import Mathlib
   2import IndisputableMonolith.ILG.Kernel
   3
   4namespace IndisputableMonolith
   5namespace ILG
   6
   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
  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
  52    rw [deriv_div_const]
  53    simp
  54
  55  -- Combine
  56  dsimp
  57  rw [h_deriv_a, h_deriv_k]
  58  field_simp [ha, hk]
  59  ring
  60
  61/-- The logarithmic form of the identity: ∂lnQ/∂lna = -∂lnQ/∂lnk. -/
  62theorem x_reciprocity_log_identity (tau0 : ℝ) (Q_tilde : ℝ → ℝ)
  63    (a k : ℝ) (ha : a ≠ 0) (hk : k ≠ 0) (hQpos : Q_tilde (X_var k a tau0) ≠ 0)
  64    (hQ : DifferentiableAt ℝ Q_tilde (X_var k a tau0)) :
  65    let Q := fun (a k : ℝ) => Q_tilde (X_var k a tau0)
  66    (a / Q a k) * (deriv (fun a' => Q a' k) a) = - ((k / Q a k) * (deriv (fun k' => Q a k') k)) := by
  67  have h := x_reciprocity_identity tau0 Q_tilde a k ha hk hQ
  68  dsimp at h |-
  69  field_simp [hQpos]
  70  linear_combination h
  71
  72end ILG
  73end IndisputableMonolith
  74