FKS.remark_3_7

@[blueprint  "fks-remark-3-7"  (title := "FKS Remark 3.7")  (statement := /-- If $H_0 > 1$, $R > 0$, and  $\sigma < 1 - 1/(R \log H_0)$, then $H_σ = H_0$. -/)]theorem remark_3_7 {H₀ R σ : ℝ} (hH₀ : H₀ > 1) (hR : R > 0)    (hσ : σ < 1 - 1 / (R * log H₀)) : Hσ H₀ R σ = H₀ := by  unfold Hσ; rw [max_eq_left]  have hlog := log_pos hH₀  have hRlog := mul_pos hR hlog  have h1σ : 1 - σ > 0 := by linarith [div_pos one_pos hRlog]  have key : 1 / (R * (1 - σ)) < log H₀ := by    rw [div_lt_iff₀ (mul_pos hR h1σ)]    calc log H₀ * (R * (1 - σ))        = R * (1 - σ) * log H₀ := by ring      _ > R * (1 / (R * log H₀)) * log H₀ :=          mul_lt_mul_of_pos_right            (mul_lt_mul_of_pos_left (by linarith) hR) hlog      _ = 1 := by field_simp  linarith [exp_strictMono key,    exp_log (show H₀ > 0 by linarith)]