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

normalized_eq_one_at_max

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)

  80theorem normalized_eq_one_at_max (a : ℕ → ℝ) (n : ℕ)
  81    (hmax : a n = runningMax a n) (hpos : 0 < a n) :
  82    normalized a n = 1 := by

proof body

Term-mode proof.

  83  unfold normalized
  84  rw [hmax]
  85  exact div_self (ne_of_gt (runningMax_pos a n hpos))
  86
  87/-! ## Rescaled Coordinates -/
  88
  89/-- The rescaling factor λₙ = 1 / √(runningMax a n).
  90    Used to rescale space: x ↦ x/λₙ, t ↦ t/λₙ². -/

depends on (3)

Lean names referenced from this declaration's body.