pith. machine review for the scientific record. sign in
lemma proved tactic proof

predicted_ratio_rescale

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  17lemma predicted_ratio_rescale (M : ScalingModel)
  18  (c tau_m1 tau_m2 tau_f : ℝ) (hc : 0 < c) :
  19  predicted_ratio M (c * tau_m1) (c * tau_m2) (c * tau_f)
  20    = predicted_ratio M tau_m1 tau_m2 tau_f := by

proof body

Tactic-mode proof.

  21  dsimp [predicted_ratio]
  22  have h12 : (c * tau_m1) / (c * tau_m2) = tau_m1 / tau_m2 := by
  23    have hc0 : (c:ℝ) ≠ 0 := ne_of_gt hc
  24    field_simp [hc0]
  25  have h1f : (c * tau_m1) / (c * tau_f) = tau_m1 / tau_f := by
  26    have hc0 : (c:ℝ) ≠ 0 := ne_of_gt hc
  27    field_simp [hc0]
  28  have h2f : (c * tau_m2) / (c * tau_f) = tau_m2 / tau_f := by
  29    have hc0 : (c:ℝ) ≠ 0 := ne_of_gt hc
  30    field_simp [hc0]
  31  have hf : M.f ((c * tau_m1) / (c * tau_f)) ((c * tau_m2) / (c * tau_f))
  32            = M.f (tau_m1 / tau_f) (tau_m2 / tau_f) := by
  33    simpa [h1f, h2f, one_mul] using
  34      (M.f_hom0 (c:=1) (t1:=tau_m1 / tau_f) (t2:=tau_m2 / tau_f) (by norm_num))
  35  simp [h12, hf]
  36
  37end
  38
  39end MRD
  40end TruthCore
  41end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.