`normalized`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.RunningMaxNormalization
domain: NavierStokes
line: 70 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.RunningMaxNormalization on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  67
  68/-- The normalized sequence: ã(n) = a(n) / runningMax(a)(n).
  69    By construction, |ã(n)| ≤ 1 for all n. -/
  70noncomputable def normalized (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  71  a n / runningMax a n
  72
  73/-- The normalized sequence is bounded by 1 in absolute value. -/
  74theorem normalized_le_one (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  75    normalized a n ≤ 1 := by
  76  unfold normalized
  77  exact (div_le_one (runningMax_pos a n h)).mpr (runningMax_ge a n)
  78
  79/-- The normalized sequence achieves 1 at the running-max index. -/
  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
  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/λₙ². -/
  91noncomputable def rescaleLength (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  92  1 / Real.sqrt (runningMax a n)
  93
  94/-- The rescaling factor is positive. -/
  95theorem rescaleLength_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  96    0 < rescaleLength a n := by
  97  unfold rescaleLength
  98  apply div_pos one_pos
  99  exact Real.sqrt_pos.mpr (runningMax_pos a n h)
 100

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.