Source indexedlemma · leanprover/lean4:v4.32.0

Smooth1Properties_estimate

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:844 to 870

Source documentation

Let $c:=2^\epsilon > 1$ , in terms of which we wish to prove

-1 < c \log c - c .

Letting $f(x):=x\log x - x$ , we can rewrite this as $f(1) < f(c)$ . Since

\frac {d}{dx}f(x) = \log x > 0 ,

$f$ is monotone increasing on [1, \infty), and we are done. -/) (latexEnv := "definition")] noncomputable def Smooth1 (ν : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ := MellinConvolution (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike ν ε)

-- This lemma might not be necessary, but the RHS is supported on [0, infinity), which makes -- results like support_MellinConvolution_subsets easier to apply. lemma Smooth1_def_ite {ν : ℝ → ℝ} {ε x : ℝ} (xpos : 0 < x) : Smooth1 ν ε x = MellinConvolution (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) (fun x ↦ if x < 0 then 0 else DeltaSpike ν ε x) x := by unfold Smooth1 rw [MellinConvolutionSymmetric _ _ xpos] conv => lhs; rw [MellinConvolutionSymmetric _ _ xpos] unfold MellinConvolution apply MeasureTheory.integral_congr_ae filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ioi] simp +contextual only [mem_Ioi, true_and, ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq, mul_ite, mul_zero] intro y ypos rw [eq_comm, if_neg (by push Not; positivity)]

/-% ** Wrong delimiters on purpose, no need to include this in blueprint \begin{lemma}[Smooth1Properties_estimate]\label{Smooth1Properties_estimate} \lean{Smooth1Properties_estimate}\leanok For $\epsilon>0$ ,

\log2>\frac{1-2^{-\epsilon}}\epsilon

\end{lemma} %

Exact Lean statement

lemma Smooth1Properties_estimate {ε : ℝ} (εpos : 0 < ε) :
    (1 - 2 ^ (-ε)) / ε < Real.log 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Smooth1Properties_estimate {ε : ℝ} (εpos : 0 < ε) :    (1 - 2 ^ (-ε)) / ε < Real.log 2 := by  apply (div_lt_iff₀' εpos).mpr  have : 1 - 1 / (2 : ℝ) ^ ε = ((2 : ℝ) ^ ε - 1) / (2 : ℝ) ^ ε := by    rw [sub_div, div_self (by positivity)]  rw [← Real.log_rpow (by norm_num), rpow_neg (by norm_num), inv_eq_one_div (2 ^ ε), this]  set c := (2 : ℝ) ^ ε  have hc : 1 < c := by    rw [← rpow_zero (2 : ℝ)]    apply Real.rpow_lt_rpow_of_exponent_lt (by norm_num) εpos  apply (div_lt_iff₀' (by positivity)).mpr <| lt_sub_iff_add_lt'.mp ?_  let f := (fun x ↦ x * Real.log x - x)  rw [(by simp [f] : -1 = f 1), (by simp [f] : c * Real.log c - c = f c)]  have mono: StrictMonoOn f <| Ici 1 := by    refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ ?_    · apply continuousOn_id.mul (continuousOn_id.log ?_) |>.sub continuousOn_id      intro x hx; simp only [mem_Ici] at hx; simp only [id_eq, ne_eq]; linarith    · intro x hx; simp only [nonempty_Iio, interior_Ici', mem_Ioi] at hx      dsimp only [f]      rw [deriv_fun_sub, deriv_fun_mul, Real.deriv_log, deriv_id'', one_mul, mul_inv_cancel₀]      · simp [log_pos hx]      · linarith      · simp only [differentiableAt_fun_id]      · simp only [differentiableAt_log_iff, ne_eq]; linarith      · exact differentiableAt_fun_id.mul <| differentiableAt_fun_id.log (by linarith)      · simp only [differentiableAt_fun_id]  exact mono (by rw [mem_Ici]) (mem_Ici.mpr <| le_of_lt hc) hc