density_exceeds_threshold

formal source

 130/-- **LOCAL DENSITY EVENTUALLY EXCEEDS ANY THRESHOLD**
 131
 132    K₀ * φ^N / (V₀ * (N+1)³) → ∞ as N → ∞. -/
 133theorem density_exceeds_threshold (K₀ : ℝ) (hK₀ : 0 < K₀)
 134    (V₀ : ℝ) (hV₀ : 0 < V₀) (threshold : ℝ) (hT : 0 < threshold) :
 135    ∃ N : ℕ, K₀ * phi ^ N / (V₀ * ((N : ℝ) + 1) ^ 3) > threshold := by
 136  -- Need phi^N > (threshold * V₀ / K₀) * (N+1)^3
 137  have hC : 0 < threshold * V₀ / K₀ := by positivity
 138  obtain ⟨N, hN⟩ := phi_exp_defeats_cubic_succ (threshold * V₀ / K₀) hC
 139  refine ⟨N, ?_⟩
 140  have hdenom_pos : 0 < V₀ * ((N : ℝ) + 1) ^ 3 := by positivity
 141  rw [gt_iff_lt, lt_div_iff₀ hdenom_pos]
 142  -- Goal: threshold * (V₀ * (N+1)^3) < K₀ * phi^N
 143  -- From hN: phi^N > (threshold*V₀/K₀) * (N+1)^3
 144  -- So K₀ * phi^N > K₀ * (threshold*V₀/K₀) * (N+1)^3 = threshold*V₀*(N+1)^3
 145  have hphi_pos : 0 < phi ^ N := pow_pos phi_pos N
 146  have hNN3 : 0 < ((N : ℝ) + 1) ^ 3 := by positivity
 147  have hK0phi : K₀ * phi ^ N > K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 := by
 148    have := mul_lt_mul_of_pos_left hN hK₀
 149    simp only [mul_comm, mul_assoc] at this ⊢
 150    linarith
 151  have hsimp : K₀ * (threshold * V₀ / K₀) * ((N : ℝ) + 1) ^ 3 =
 152               threshold * V₀ * ((N : ℝ) + 1) ^ 3 := by
 153    have hK0ne : K₀ ≠ 0 := ne_of_gt hK₀
 154    field_simp [hK0ne]
 155  rw [hsimp] at hK0phi
 156  linarith
 157
 158end GrowthBounds
 159end Foundation
 160end IndisputableMonolith