theorem
proved
tactic proof
running_g_scaling
show as:
view Lean formalization →
formal statement (Lean)
32theorem running_g_scaling (r r_ref : ℝ) (hr : r > 0) (href : r_ref > 0) :
33 deriv (fun x => G_ratio x r_ref) r =
34 (abs beta_running * beta_running / r_ref) * (r / r_ref) ^ (beta_running - 1) := by
proof body
Tactic-mode proof.
35 unfold G_ratio
36 rw [deriv_add]
37 · rw [deriv_const, zero_add]
38 rw [deriv_mul_const]
39 · -- deriv (fun x => (x / r_ref) ^ beta_running) r
40 -- = beta_running * (r / r_ref) ^ (beta_running - 1) * (1 / r_ref)
41 have h_deriv : deriv (fun x => (x / r_ref) ^ beta_running) r =
42 beta_running * (r / r_ref) ^ (beta_running - 1) * (1 / r_ref) := by
43 -- Use chain rule: (f ∘ g)' = f'(g(x)) * g'(x)
44 -- f(u) = u ^ beta_running, g(x) = x / r_ref
45 rw [deriv_rpow_const]
46 · -- u ^ (beta_running - 1) * deriv (fun x => x / r_ref) r
47 rw [deriv_div_const]
48 · rw [deriv_id'']
49 ring
50 · -- g(x) = r / r_ref > 0
51 exact div_pos hr href
52 rw [h_deriv]
53 ring
54 · -- differentiability of (fun x => (x / r_ref) ^ beta_running) at r
55 apply DifferentiableAt.rpow_const
56 · apply DifferentiableAt.div_const
57 exact differentiableAt_id
58 · exact Or.inl (ne_of_gt (div_pos hr href))
59 · -- differentiability of const 1
60 exact differentiableAt_const 1
61 · -- differentiability of the second term
62 apply DifferentiableAt.const_mul
63 apply DifferentiableAt.rpow_const
64 · apply DifferentiableAt.div_const
65 exact differentiableAt_id
66 · exact Or.inl (ne_of_gt (div_pos hr href))
67
68end RunningG
69end IndisputableMonolith.Gravity