theorem
proved
tactic proof
x_reciprocity_identity
show as:
view Lean formalization →
formal statement (Lean)
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)
proof body
Tactic-mode proof.
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. -/