pith. machine review for the scientific record. sign in
theorem proved term proof

scale_perturbed_low

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)

  57theorem scale_perturbed_low (levels : ℕ → ℝ) (j : ℕ) (t : ℝ)
  58    (k : ℕ) (hk : k ≤ j) :
  59    ScalePerturbed levels j t k = levels k := by

proof body

Term-mode proof.

  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. -/

depends on (7)

Lean names referenced from this declaration's body.