cascadeDepth_finite

formal source

 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
 127  have htend : Filter.Tendsto (fun n => phi ^ n) Filter.atTop Filter.atTop :=
 128    tendsto_pow_atTop_atTop_of_one_lt one_lt_phi
 129  rw [Filter.tendsto_atTop_atTop] at htend
 130  obtain ⟨N, hN⟩ := htend ⌈L⌉₊
 131  use N
 132  intro n hn
 133  show L ≤ phi ^ n
 134  calc L ≤ ↑⌈L⌉₊ := Nat.le_ceil L
 135    _ ≤ phi ^ n := hN n hn
 136