auto_cheby_exists_smooth_nonneg_fourier_kernel

lemma auto_cheby_exists_smooth_nonneg_fourier_kernel :    ∃ (ψ : ℝ → ℂ), ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧    (∀ y, 0 ≤ (𝓕 ψ y).re ∧ (𝓕 ψ y).im = 0) ∧ 0 < (𝓕 ψ 0).re := by  obtain ⟨φ_real, hφSmooth, hφCompact, hφIcc, _, hφsupp⟩ :=    smooth_urysohn_support_Ioo (a := 1/2) (b := 1) (c := 1) (d := 2) (by norm_num) (by norm_num)  let φ : ℝ → ℂ := Complex.ofReal ∘ φ_real  let φ_rev : ℝ → ℂ := fun x ↦ conj (φ (-x))  let ψ_fun : ℝ → ℂ := convolution φ φ_rev (ContinuousLinearMap.mul ℂ ℂ) volume  have hφSmooth' : ContDiff ℝ ∞ φ := contDiff_ofReal.comp hφSmooth  have hφCompact' : HasCompactSupport φ := hφCompact.comp_left rfl  have hφRevSmooth : ContDiff ℝ ∞ φ_rev := Complex.conjCLE.contDiff.comp (hφSmooth'.comp contDiff_neg)  have hφRevCompact : HasCompactSupport φ_rev := (hφCompact'.comp_homeomorph (Homeomorph.neg ℝ)).comp_left (by simp)  have hφInt : Integrable φ := hφSmooth'.continuous.integrable_of_hasCompactSupport hφCompact'  have hφRevInt : Integrable φ_rev := hφRevSmooth.continuous.integrable_of_hasCompactSupport hφRevCompact  have hψSmooth : ContDiff ℝ ∞ ψ_fun := by    convert! hφRevCompact.contDiff_convolution_right (ContinuousLinearMap.mul ℝ ℂ)      (hφSmooth'.continuous.locallyIntegrable (μ := volume)) hφRevSmooth  have hψCompact : HasCompactSupport ψ_fun :=    HasCompactSupport.convolution (ContinuousLinearMap.mul ℂ ℂ) hφCompact' hφRevCompact  refine ⟨ψ_fun, hψSmooth, hψCompact, fun y ↦ ?_, ?_⟩  · rw [Real.fourierIntegral_convolution hφInt hφRevInt, Pi.mul_apply,      Real.fourierIntegral_conj_neg y, mul_comm, ← Complex.normSq_eq_conj_mul_self]    exact ⟨Complex.normSq_nonneg _, rfl⟩  · have hφ_nonneg : ∀ x, 0 ≤ φ_real x := fun x ↦ by      have hx := hφIcc x; by_cases h : x ∈ Set.Icc (1:ℝ) 1      · simp only [Set.indicator_of_mem h, Pi.one_apply] at hx; linarith      · simp only [Set.indicator_of_notMem h] at hx; exact hx    have hvol_supp : (1 : ENNReal) ≤ volume (Function.support φ_real) := by      have hsub : Set.Ico (1:ℝ) 2 ⊆ Function.support φ_real := fun x hx ↦        hφsupp.symm ▸ Set.mem_Ioo.mpr ⟨by linarith [hx.1], hx.2⟩      calc _ = volume (Set.Ico (1:ℝ) 2) := by simp [Real.volume_Ico]; norm_num           _ ≤ _ := volume.mono hsub    have hφint_pos : 0 < ∫ x, φ_real x :=      (integral_pos_iff_support_of_nonneg_ae (.of_forall hφ_nonneg)        (hφSmooth.continuous.integrable_of_hasCompactSupport hφCompact)).2        (lt_of_lt_of_le (by simp) hvol_supp)    have hFφ0_re : 0 < (𝓕 φ 0).re := by      simp only [φ, fourier_real_eq, mul_zero, neg_zero, AddChar.map_zero_eq_one, one_smul,        Function.comp_apply]      have hint : Integrable (fun x => (φ_real x : ℂ)) :=        (hφSmooth.continuous.integrable_of_hasCompactSupport hφCompact).ofReal      calc (∫ x, (φ_real x : ℂ)).re = ∫ x, (φ_real x : ℂ).re := (integral_re hint).symm        _ = ∫ x, φ_real x := by simp only [Complex.ofReal_re]        _ > 0 := hφint_pos    rw [Real.fourierIntegral_convolution hφInt hφRevInt, Pi.mul_apply,      Real.fourierIntegral_conj_neg 0, mul_comm, ← Complex.normSq_eq_conj_mul_self]    exact Complex.normSq_pos.2 (fun h ↦ (ne_of_gt hFφ0_re) (by simp [h]))