Erdos392.boundary_term_le

lemma boundary_term_le (P : Params) :    (if (P.n / P.L).Prime then      ((P.n : ℝ) / (P.n / P.L : ℕ)) * Real.log ((P.n : ℝ) / (P.n / P.L : ℕ))    else 0) ≤ (P.L + 1) * Real.log (P.L + 1) := by  by_cases hprime : (P.n / P.L).Prime  · have hL_le_div : P.L ≤ P.n / P.L := by      exact (Nat.le_div_iff_mul_le P.hL_pos).2 (Nat.le_of_lt P.hL)    have hdiv_pos_nat : 0 < P.n / P.L := lt_of_lt_of_le P.hL_pos hL_le_div    have hq_pos : (0 : ℝ) < (P.n / P.L : ℕ) := by exact_mod_cast hdiv_pos_nat    have hmod_lt_div : P.n % P.L < P.n / P.L := lt_of_lt_of_le (Nat.mod_lt _ P.hL_pos) hL_le_div    have hdecomp : P.n = (P.n / P.L) * P.L + P.n % P.L := by      simpa [Nat.mul_comm] using (Nat.div_add_mod P.n P.L).symm    have hn_lt : P.n < (P.L + 1) * (P.n / P.L) := by      have haux : (P.n / P.L) * P.L + P.n % P.L < (P.n / P.L) * P.L + (P.n / P.L) :=        Nat.add_lt_add_left hmod_lt_div ((P.n / P.L) * P.L)      calc P.n = (P.n / P.L) * P.L + P.n % P.L := hdecomp        _ < (P.n / P.L) * P.L + (P.n / P.L) := haux        _ = (P.n / P.L) * (P.L + 1) := by ring        _ = (P.L + 1) * (P.n / P.L) := by ring    have hdiv_le : (P.n : ℝ) / (P.n / P.L : ℕ) ≤ P.L + 1 := by      exact le_of_lt ((div_lt_iff₀ hq_pos).2 (by exact_mod_cast hn_lt))    have hdiv_ge1 : (1 : ℝ) ≤ (P.n : ℝ) / (P.n / P.L : ℕ) := by      rw [le_div_iff₀ hq_pos]      simpa [one_mul] using        (show ((P.n / P.L : ℕ) : ℝ) ≤ P.n by exact_mod_cast (Nat.div_le_self P.n P.L))    have hlog_nonneg : 0 ≤ Real.log ((P.n : ℝ) / (P.n / P.L : ℕ)) := Real.log_nonneg hdiv_ge1    have hlog_le : Real.log ((P.n : ℝ) / (P.n / P.L : ℕ)) ≤ Real.log (P.L + 1) := by      have hdiv_pos' : 0 < (P.n : ℝ) / (P.n / P.L : ℕ) := by        have hn_pos : (0 : ℝ) < P.n := by          exact_mod_cast Nat.lt_of_lt_of_le (Nat.mul_pos P.hL_pos P.hL_pos) (Nat.le_of_lt P.hL)        exact div_pos hn_pos hq_pos      apply Real.log_le_log hdiv_pos'      exact hdiv_le    rw [if_pos hprime]    exact mul_le_mul hdiv_le hlog_le hlog_nonneg (by positivity)  · have hRHS_nonneg : 0 ≤ (P.L + 1 : ℝ) * Real.log (P.L + 1) := by      have hL1 : (1 : ℝ) ≤ P.L + 1 := by nlinarith      exact mul_nonneg (by positivity) (Real.log_nonneg hL1)    simpa [hprime] using hRHS_nonneg