Source indexedlemma · leanprover/lean4:v4.32.0

Smooth1Properties_below

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:886 to 957

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "Smooth1Properties-below")
  (statement := /--
  Fix $\epsilon>0$. There is an absolute constant $c>0$ so that:
  If $0 < x \leq (1-c\epsilon)$, then
  $$\widetilde{1_{\epsilon}}(x) = 1.$$
  -/)
  (proof := /--
  Opening the definition, we have that the Mellin convolution of $1_{(0,1]}$ with $\nu_\epsilon$ is
  $$
  \int_0^\infty 1_{(0,1]}(y)\nu_\epsilon(x/y)\frac{dy}{y}
  =
  \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y}.
  $$
  The support of $\nu_\epsilon$ is contained in $[1/2^\epsilon,2^\epsilon]$, so it suffices to
  consider $y \in [1/2^\epsilon x,2^\epsilon x]$ for nonzero contributions. If $x < 2^{-\epsilon}$,
  then the integral is the same as that over $(0,\infty)$:
  $$
  \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y}
  =
  \int_0^\infty \nu_\epsilon(x/y)\frac{dy}{y},
  $$
  in which we change variables to $z=x/y$ (using $x>0$):
  $$
  \int_0^\infty \nu_\epsilon(x/y)\frac{dy}{y}
  =
  \int_0^\infty \nu_\epsilon(z)\frac{dz}{z},
  $$
  which is equal to one by Lemma \ref{DeltaSpikeMass}.
  We then choose
  $$
    c:=\log 2,
  $$
  which satisfies
  $$
    c > \frac{1-2^{-\epsilon}}\epsilon
  $$
  by Lemma \ref{Smooth1Properties_estimate}, so
  $$
    1-c\epsilon < 2^{-\epsilon}.
  $$
  -/)
  (latexEnv := "lemma")]
lemma Smooth1Properties_below {ν : ℝ → ℝ} (suppν : ν.support ⊆ Icc (1 / 2) 2)
    (mass_one : ∫ x in Ioi 0, ν x / x = 1) :
    ∃ (c : ℝ), 0 < c ∧ c = Real.log 2 ∧
      ∀ (ε x) (_ : 0 < ε), 0 < x → x ≤ 1 - c * ε → Smooth1 ν ε x = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "Smooth1Properties-below")  (statement := /--  Fix $\epsilon>0$. There is an absolute constant $c>0$ so that:  If $0 < x \leq (1-c\epsilon)$, then  $$\widetilde{1_{\epsilon}}(x) = 1.$$  -/)  (proof := /--  Opening the definition, we have that the Mellin convolution of $1_{(0,1]}$ with $\nu_\epsilon$ is  $$  \int_0^\infty 1_{(0,1]}(y)\nu_\epsilon(x/y)\frac{dy}{y}  =  \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y}.  $$  The support of $\nu_\epsilon$ is contained in $[1/2^\epsilon,2^\epsilon]$, so it suffices to  consider $y \in [1/2^\epsilon x,2^\epsilon x]$ for nonzero contributions. If $x < 2^{-\epsilon}$,  then the integral is the same as that over $(0,\infty)$:  $$  \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y}  =  \int_0^\infty \nu_\epsilon(x/y)\frac{dy}{y},  $$  in which we change variables to $z=x/y$ (using $x>0$):  $$  \int_0^\infty \nu_\epsilon(x/y)\frac{dy}{y}  =  \int_0^\infty \nu_\epsilon(z)\frac{dz}{z},  $$  which is equal to one by Lemma \ref{DeltaSpikeMass}.  We then choose  $$    c:=\log 2,  $$  which satisfies  $$    c > \frac{1-2^{-\epsilon}}\epsilon  $$  by Lemma \ref{Smooth1Properties_estimate}, so  $$    1-c\epsilon < 2^{-\epsilon}.  $$  -/)  (latexEnv := "lemma")]lemma Smooth1Properties_below {ν : ℝ → ℝ} (suppν : ν.support ⊆ Icc (1 / 2) 2)    (mass_one : ∫ x in Ioi 0, ν x / x = 1) :    ∃ (c : ℝ), 0 < c ∧ c = Real.log 2 ∧      ∀ (ε x) (_ : 0 < ε), 0 < x → x ≤ 1 - c * ε → Smooth1 ν ε x = 1 := by  set c := Real.log 2; use c  refine ⟨log_pos (by norm_num), rfl, ?_⟩  intro ε x εpos xpos hx  have hx2 := Smooth1Properties_below_aux hx εpos  rewrite [← DeltaSpikeMass mass_one εpos]  unfold Smooth1 MellinConvolution  calc    _ = ∫ (y : ℝ) in Ioi 0,        indicator (Ioc 0 1) (fun y ↦ DeltaSpike ν ε (x / y) / ↑y) y := ?_    _ = ∫ (y : ℝ) in Ioi 0, DeltaSpike ν ε (x / y) / y := ?_    _ = _ := integral_comp_div_I0i_haar (fun y ↦ DeltaSpike ν ε y) xpos  · rw [setIntegral_congr_fun (by simp)]    intro y hy    by_cases h : y ≤ 1 <;> simp [indicator, mem_Ioi.mp hy, h]  · rw [setIntegral_congr_fun (by simp)]    intro y hy    have : y ≠ 0 := by      rintro rfl      simp at hy    simp only [indicator_apply_eq_self, mem_Ioc, not_and, not_le, div_eq_zero_iff, this, or_false]    intro hy2; replace hy2 := hy2 <| mem_Ioi.mp hy    apply DeltaSpikeSupport εpos ?_ suppν    · simp only [mem_Icc, not_and, not_le]; intro      linarith [(by apply (div_lt_iff₀ (by linarith)).mpr; nlinarith : x / y < 2 ^ (-ε))]    · rw [le_div_iff₀ (by linarith), zero_mul]; exact xpos.le