IndisputableMonolith.TruthCore.MRD.Scaling

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace TruthCore
   5namespace MRD
   6
   7structure ScalingModel where
   8  gamma : ℝ
   9  f     : ℝ → ℝ → ℝ
  10  f_hom0 : ∀ {c t1 t2}, 0 < c → f (c * t1) (c * t2) = f t1 t2
  11
  12noncomputable section
  13
  14@[simp] noncomputable def predicted_ratio (M : ScalingModel) (tau_m1 tau_m2 tau_f : ℝ) : ℝ :=
  15  ((tau_m1 / tau_m2) ^ M.gamma) * M.f (tau_m1 / tau_f) (tau_m2 / tau_f)
  16
  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
  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
  42