phiRungScale_succ

formal source

  86  exact pow_lt_pow_right₀ one_lt_phi hab
  87
  88/-- φ-rung scale at n+1 equals φ times the scale at n. -/
  89theorem phiRungScale_succ (n : ℕ) :
  90    phiRungScale (n + 1) = phi * phiRungScale n := by
  91  unfold phiRungScale; rw [pow_succ]; ring
  92
  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)