Source indexedlemma · leanprover/lean4:v4.32.0

Smooth1LeOne

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1135 to 1190

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "Smooth1LeOne")
  (statement := /--
  If $\nu$ is nonnegative and has mass one, then $\widetilde{1_{\epsilon}}(x)\le 1$, $\forall x>0$.
  -/)
  (proof := /--
  By Definitions \ref{Smooth1}, \ref{MellinConvolution} and \ref{DeltaSpike}
  $$
    \widetilde{1_\epsilon}(x)
    =\int_0^\infty 1_{(0,1]}(y)\frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y
  $$
  and since $1_{(0,1]}(y)\le 1$, and all the factors in the integrand are nonnegative,
  $$
    \widetilde{1_\epsilon}(x)\le\int_0^\infty \frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y
  $$
  (because in mathlib the integral of a non-integrable function is $0$, for the inequality above
  to be true, we must prove that $\nu((x/y)^{\frac1\epsilon})/y$ is integrable; this follows from
  the computation below).
  We then change variables to $z=(x/y)^{\frac1\epsilon}$:
  $$
    \widetilde{1_\epsilon}(x)\le\int_0^\infty \nu(z) \frac{dz}z
  $$
  which by Theorem \ref{SmoothExistence} is 1.
  -/)
  (latexEnv := "lemma")]
lemma Smooth1LeOne {ν : ℝ → ℝ} (νnonneg : ∀ x > 0, 0 ≤ ν x)
    (mass_one : ∫ x in Ioi 0, ν x / x = 1) {ε : ℝ} (εpos : 0 < ε) {x : ℝ} (xpos : 0 < x) :
    Smooth1 ν ε x ≤ 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "Smooth1LeOne")  (statement := /--  If $\nu$ is nonnegative and has mass one, then $\widetilde{1_{\epsilon}}(x)\le 1$, $\forall x>0$.  -/)  (proof := /--  By Definitions \ref{Smooth1}, \ref{MellinConvolution} and \ref{DeltaSpike}  $$    \widetilde{1_\epsilon}(x)    =\int_0^\infty 1_{(0,1]}(y)\frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y  $$  and since $1_{(0,1]}(y)\le 1$, and all the factors in the integrand are nonnegative,  $$    \widetilde{1_\epsilon}(x)\le\int_0^\infty \frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y  $$  (because in mathlib the integral of a non-integrable function is $0$, for the inequality above  to be true, we must prove that $\nu((x/y)^{\frac1\epsilon})/y$ is integrable; this follows from  the computation below).  We then change variables to $z=(x/y)^{\frac1\epsilon}$:  $$    \widetilde{1_\epsilon}(x)\le\int_0^\infty \nu(z) \frac{dz}z  $$  which by Theorem \ref{SmoothExistence} is 1.  -/)  (latexEnv := "lemma")]lemma Smooth1LeOne {ν : ℝ → ℝ} (νnonneg : ∀ x > 0, 0 ≤ ν x)    (mass_one : ∫ x in Ioi 0, ν x / x = 1) {ε : ℝ} (εpos : 0 < ε) {x : ℝ} (xpos : 0 < x) :    Smooth1 ν ε x ≤ 1 := by  unfold Smooth1 MellinConvolution DeltaSpike  have := Smooth1LeOne_aux xpos εpos mass_one  calc    _ = ∫ (y : ℝ) in Ioi 0,        (fun y ↦ if y ∈ Ioc 0 1 then 1 else 0) y * (ν ((x / y) ^ (1 / ε)) / ε / y) := ?_    _ ≤ ∫ (y : ℝ) in Ioi 0, (ν ((x / y) ^ (1 / ε)) / ε) / y := ?_    _ = 1 := this  · rw [setIntegral_congr_fun (by simp)]    simp only [ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq, mem_Ioc]    intro y hy; aesop  · refine setIntegral_mono_on ?_ (integrable_of_integral_eq_one this) (by simp) ?_    · refine integrable_of_integral_eq_one this |>.bdd_mul ?_        (ae_of_all _ <| by aesop)      have : (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) =          indicator (Ioc 0 1) (1 : ℝ → ℝ) := by        aesop      simp only [mem_Ioc, this, measurableSet_Ioc, aestronglyMeasurable_indicator_iff]      exact aestronglyMeasurable_one    · simp only [ite_mul, one_mul, zero_mul]      intro y hy      by_cases h : y ≤ 1      · aesop      field_simp      simp only [mem_Ioc, h, and_false, ↓reduceIte, one_div, mul_zero]      simp only [mem_Ioi] at hy      apply div_nonneg      · apply νnonneg; exact rpow_pos_of_pos (div_pos xpos <| mem_Ioi.mp hy) _      · positivity