Source indexedlemma · leanprover/lean4:v4.32.0

Smooth1_def_ite

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:820 to 832

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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)]