ScalePerturbed

formal source

  41/-- Perturbed level sequence: shift all levels above position `j` by the
  42factor `exp(t)`. This changes the ratio at position `j` to `r_j · exp(t)`
  43while preserving all other ratios and positivity for every `t ∈ ℝ`. -/
  44noncomputable def ScalePerturbed (levels : ℕ → ℝ) (j : ℕ) (t : ℝ) (k : ℕ) : ℝ :=
  45  if k ≤ j then levels k else levels k * Real.exp t
  46
  47/-- Every perturbed level is positive. -/
  48theorem scale_perturbed_pos (levels : ℕ → ℝ) (j : ℕ)
  49    (h_pos : ∀ k, 0 < levels k) (t : ℝ) (k : ℕ) :
  50    0 < ScalePerturbed levels j t k := by
  51  unfold ScalePerturbed
  52  split
  53  · exact h_pos k
  54  · exact mul_pos (h_pos k) (Real.exp_pos t)
  55
  56/-- The perturbation fixes all levels at or below position `j`. -/
  57theorem scale_perturbed_low (levels : ℕ → ℝ) (j : ℕ) (t : ℝ)
  58    (k : ℕ) (hk : k ≤ j) :
  59    ScalePerturbed levels j t k = levels k := by
  60  unfold ScalePerturbed; rw [if_pos hk]
  61
  62/-- Different perturbation parameters give different level sequences.
  63The key step: at position `j + 1` the values are `levels(j+1) · exp(t)`,
  64and `exp` is injective. -/
  65theorem scale_perturbed_family_injective (levels : ℕ → ℝ) (j : ℕ)
  66    (h_pos : 0 < levels (j + 1)) :
  67    Function.Injective (ScalePerturbed levels j) := by
  68  intro t₁ t₂ h
  69  have h_eval := congr_fun h (j + 1)
  70  unfold ScalePerturbed at h_eval
  71  rw [if_neg (by omega : ¬(j + 1 ≤ j)), if_neg (by omega : ¬(j + 1 ≤ j))] at h_eval
  72  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
  73  exact Real.exp_injective (mul_left_cancel₀ h_ne h_eval)
  74