Smooth1Properties_above

@[blueprint  (title := "Smooth1Properties-above")  (statement := /--  Fix $0<\epsilon<1$. There is an absolute constant $c>0$ so that:  if $x\geq (1+c\epsilon)$, then  $$\widetilde{1_{\epsilon}}(x) = 0.$$  -/)  (proof := /--  Again the Mellin convolution is  $$\int_0^1 \nu_\epsilon(x/y)\frac{dy}{y},$$  but now if $x > 2^\epsilon$, then the support of $\nu_\epsilon$ is disjoint  from the region of integration, and hence the integral is zero.  We choose  $$    c:=2\log 2    .  $$  By Lemma \ref{Smooth1Properties_estimate},  $$    c > 2\frac{1-2^{-\epsilon}}\epsilon > 2^\epsilon\frac{1-2^{-\epsilon}}\epsilon    =    \frac{2^\epsilon-1}\epsilon,  $$  so  $$    1+c\epsilon > 2^\epsilon.  $$  -/)  (latexEnv := "lemma")]lemma Smooth1Properties_above {ν : ℝ → ℝ} (suppν : ν.support ⊆ Icc (1 / 2) 2) :    ∃ (c : ℝ), 0 < c ∧ c = 2 * Real.log 2 ∧      ∀ (ε x) (_ : ε ∈ Ioo 0 1), 1 + c * ε ≤ x → Smooth1 ν ε x = 0 := by  set c := 2 * Real.log 2; use c  constructor  · simp only [c, zero_lt_two, mul_pos_iff_of_pos_left]; exact log_pos (by norm_num)  constructor  · rfl  intro ε x hε hx  have hx2 := Smooth1Properties_above_aux hx hε  unfold Smooth1 MellinConvolution  simp only [ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq]  apply setIntegral_eq_zero_of_forall_eq_zero  intro y hy  have ypos := mem_Ioi.mp hy  by_cases y1 : y ≤ 1  swap  · simp [ypos, y1]  simp only [mem_Ioi.mp hy, y1, and_self, ↓reduceIte, div_eq_zero_iff]; left  apply DeltaSpikeSupport hε.1 ?_ suppν  on_goal 1 =>    simp only [mem_Icc, not_and, not_le]  on_goal 2 =>    suffices h : 2 ^ ε < x / y by      linarith [(by apply rpow_pos_of_pos (by norm_num) : 0 < (2 : ℝ) ^ ε)]  all_goals  try intro  have : x / y = ((x / y) ^ (1 / ε)) ^ ε := by    rw [← rpow_mul]    simp only [one_div, inv_mul_cancel₀ (ne_of_gt hε.1), rpow_one]    apply div_nonneg_iff.mpr; left;    exact ⟨(le_trans (rpow_pos_of_pos (by norm_num) ε).le) hx2.le, ypos.le⟩  rw [this]  refine rpow_lt_rpow (by norm_num) ?_ hε.1  exact Smooth1Properties_above_aux2 hε ⟨ypos, y1⟩ hx2