CH2.varphi_fourier_ident

@[blueprint  "varphi-fourier-ident"  (title := "Fourier transform of $\\varphi$")  (statement := /--\[\widehat{\varphi^{\pm}_{\nu}}(x) = \int_{-1}^{1} \varphi^{\pm}_{\nu}(t)\, e(-tx)\, dt = \int_{-1}^{0} \bigl(\Phi^{\pm,\circ}_{\nu}(t) - \Phi^{\pm,\star}_{\nu}(t)\bigr) e(-tx)\, dt + \int_0^1 \bigl(\Phi^{\pm,\circ}_{\nu}(t) + \Phi^{\pm,\star}_{\nu}(t)\bigr) e(-tx)\, dt.\]  -/)  (proof := /-- By the definition of the Fourier transform, and the fact that $\varphi^{\pm}_{\nu}$ is supported on $[-1,1]$. -/)  (latexEnv := "sublemma")  (discussion := 1079)]theorem varphi_fourier_ident (ν ε : ℝ) (hlam : ν ≠ 0) (x : ℝ) :    𝓕 (ϕ_pm ν ε) x =      (∫ t in Set.Icc (-1 : ℝ) 0, (Phi_circ ν ε t - Phi_star ν ε t) * E (-t * x)) +      (∫ t in Set.Icc 0 (1 : ℝ), (Phi_circ ν ε t + Phi_star ν ε t) * E (-t * x)) := by  calc 𝓕 (ϕ_pm ν ε) x    _ = ∫ (t : ℝ), ϕ_pm ν ε t * E (-t * x) := fourier_eq_E_integral _ x    _ = ∫ t in Set.Icc (-1:ℝ) 1, ϕ_pm ν ε t * E (-t * x) := by      apply (setIntegral_eq_integral_of_forall_compl_eq_zero ?_).symm      intro t ht      unfold ϕ_pm      split_ifs with h      · exact (ht (Set.mem_Icc.mpr h)).elim      · rw [zero_mul]    _ = (∫ t in Set.Icc (-1:ℝ) 0, ϕ_pm ν ε t * E (-t * x)) +        (∫ t in Set.Icc 0 (1:ℝ), ϕ_pm ν ε t * E (-t * x)) := by      conv_lhs =>        rw [show Set.Icc (-1 : ℝ) 1 = Set.Icc (-1) 0 ∪ Set.Icc 0 1 from          (Set.Icc_union_Icc_eq_Icc (by norm_num) (by norm_num)).symm]      refine MeasureTheory.setIntegral_union₀ ?_ nullMeasurableSet_Icc        (ϕ_pm_mul_E_integrableOn_Icc ν ε hlam x _ _)        (ϕ_pm_mul_E_integrableOn_Icc ν ε hlam x _ _)      have hcap : Set.Icc (-1 : ℝ) 0 ∩ Set.Icc 0 1 = {0} := by        ext t; simp only [Set.mem_inter_iff, Set.mem_Icc, Set.mem_singleton_iff]        constructor        · rintro ⟨⟨-, h1⟩, h2, -⟩; linarith        · rintro rfl; norm_num      simp [AEDisjoint, hcap]    _ = (∫ t in Set.Icc (-1:ℝ) 0, (Phi_circ ν ε t - Phi_star ν ε t) * E (-t * x)) +        (∫ t in Set.Icc 0 (1:ℝ), (Phi_circ ν ε t + Phi_star ν ε t) * E (-t * x)) := by      congr 1      · exact setIntegral_congr_fun measurableSet_Icc fun t ht => by          rw [ϕ_pm_eq_on_Icc_neg ν ε ht]      · exact setIntegral_congr_fun measurableSet_Icc fun t ht => by          rw [ϕ_pm_eq_on_Icc_pos ν ε ht]