cascadeDepth

formal source

  93/-! ## Cascade Depth -/
  94
  95/-- The cascade depth: N_d = ⌊(3/4) · ln(Re) / ln(φ)⌋. -/
  96def cascadeDepth (re : ℝ) : ℕ :=
  97  if 1 < re then
  98    Nat.floor ((3/4 : ℝ) * Real.log re / Real.log phi)
  99  else 0
 100
 101/-- The cascade depth is zero for Re ≤ 1. -/
 102theorem cascadeDepth_le_one {re : ℝ} (h : re ≤ 1) : cascadeDepth re = 0 := by
 103  unfold cascadeDepth; simp [not_lt.mpr h]
 104
 105/-- The cascade depth is always a concrete natural number. -/
 106theorem cascadeDepth_finite (re : ℝ) : ∃ N : ℕ, cascadeDepth re = N :=
 107  ⟨cascadeDepth re, rfl⟩
 108
 109/-- Cascade depth is monotone in Reynolds number. -/
 110theorem cascadeDepth_mono {re₁ re₂ : ℝ} (h1 : 1 < re₁) (h2 : re₁ ≤ re₂) :
 111    cascadeDepth re₁ ≤ cascadeDepth re₂ := by
 112  have h2' : 1 < re₂ := lt_of_lt_of_le h1 h2
 113  unfold cascadeDepth; simp [h1, h2']
 114  apply Nat.floor_le_floor
 115  apply div_le_div_of_nonneg_right
 116  · apply mul_le_mul_of_nonneg_left
 117    · exact Real.log_le_log (by linarith) h2
 118    · norm_num
 119  · exact le_of_lt (Real.log_pos one_lt_phi)
 120
 121/-! ## Finiteness of the Cascade -/
 122
 123/-- The φ-ladder has finitely many rungs below any fixed scale.
 124    Since φ > 1, φⁿ → ∞. -/
 125theorem finitely_many_rungs_below (L : ℝ) :
 126    ∃ N : ℕ, ∀ n : ℕ, n ≥ N → L ≤ phiRungScale n := by