open Real Complex MeasureTheory
open scoped EuclideanGeometry FourierTransform

namespace Attack

abbrev V2 := EuclideanSpace ℝ (Fin 2)

noncomputable def G (x : V2) : ℝ := 3 * Real.exp (-2 * ‖x‖^2) - Real.exp (-1 * ‖x‖^2)
noncomputable def F (x : V2) : ℝ := if x = 0 then Real.sqrt 3 * π / 12 else G x

lemma Gc (x : V2) : ((G x : ℝ) : ℂ)
    = 3 * Complex.exp (-2 * (‖x‖:ℂ)^2) - Complex.exp (-1 * (‖x‖:ℂ)^2) := by
  simp [G, Complex.ofReal_exp]

lemma intg (b : ℝ) (hb : 0 < b) :
    Integrable (fun (v : V2) ↦ Complex.exp (-(b:ℂ) * ‖v‖ ^ 2)) := by
  have := GaussianFourier.integrable_cexp_neg_mul_sq_norm_add (V := V2)
    (b := (b:ℂ)) (by simpa using hb) 0 0
  simpa using this

lemma ftg2 (w : V2) :
    𝓕 (fun (v : V2) ↦ Complex.exp (-2 * (‖v‖:ℂ) ^ 2)) w
      = (π / 2) * Complex.exp (-π ^ 2 * (‖w‖:ℂ) ^ 2 / 2) := by
  have := fourier_gaussian_innerProductSpace (V := V2) (b := (2:ℂ)) (by norm_num) w
  rw [this]; norm_num

lemma ftg1 (w : V2) :
    𝓕 (fun (v : V2) ↦ Complex.exp (-1 * (‖v‖:ℂ) ^ 2)) w
      = π * Complex.exp (-π ^ 2 * (‖w‖:ℂ) ^ 2) := by
  have := fourier_gaussian_innerProductSpace (V := V2) (b := (1:ℂ)) (by norm_num) w
  rw [this]; norm_num

lemma ft_lin {u v : V2 → ℂ} (hu : Integrable u) (hv : Integrable v) (a : ℂ) (t : V2) :
    𝓕 (fun x => a * u x - v x) t = a * 𝓕 u t - 𝓕 v t := by
  have hu' := (Real.fourierIntegral_convergent_iff (μ := volume) (f := u) t).2 hu
  have hv' := (Real.fourierIntegral_convergent_iff (μ := volume) (f := v) t).2 hv
  simp_rw [Real.fourier_eq, smul_sub, ← mul_smul_comm]
  rw [integral_sub (hu'.const_mul a) hv', integral_const_mul]

lemma ftG (t : V2) : 𝓕 (fun x : V2 => ((G x : ℝ) : ℂ)) t
    = ((3 * (π/2) * Real.exp (-π^2 * ‖t‖^2 / 2) - π * Real.exp (-π^2 * ‖t‖^2) : ℝ) : ℂ) := by
  simp_rw [Gc]
  have h2 : Integrable (fun (v : V2) ↦ Complex.exp (-2 * (‖v‖:ℂ) ^ 2)) := by
    have := intg 2 (by norm_num); norm_num at this ⊢; convert this using 3
  have h1 : Integrable (fun (v : V2) ↦ Complex.exp (-1 * (‖v‖:ℂ) ^ 2)) := by
    have := intg 1 (by norm_num); norm_num at this ⊢; convert this using 3
  rw [ft_lin h2 h1 3 t, ftg2, ftg1]
  push_cast [Complex.ofReal_exp]
  ring

-- F equals G a.e.
lemma FaeG : (fun x : V2 => ((F x : ℝ) : ℂ)) =ᵐ[volume] (fun x : V2 => ((G x : ℝ) : ℂ)) := by
  have h0 : (volume ({0} : Set V2)) = 0 := measure_singleton 0
  refine Filter.eventuallyEq_of_mem (s := ({0} : Set V2)ᶜ) ?_ ?_
  · simp [MeasureTheory.mem_ae_iff, h0]
  · intro x hx
    simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at hx
    simp [F, hx]

lemma fHatF (t : V2) : Green42.fHat F t = Green42.fHat G t := by
  unfold Green42.fHat
  congr 1
  simp_rw [Real.fourier_eq]
  exact integral_congr_ae (FaeG.mono (fun x hx => by dsimp only at hx ⊢; rw [hx]))

lemma fHatG (t : V2) :
    Green42.fHat G t = 3 * (π/2) * Real.exp (-π^2 * ‖t‖^2 / 2) - π * Real.exp (-π^2 * ‖t‖^2) := by
  unfold Green42.fHat
  rw [ftG]
  exact Complex.ofReal_re _

end Attack

namespace Attack
-- ============ elementary estimates ============
lemma key (r : ℝ) (hr : 0 ≤ r) : (1 + r)^3 ≤ 8 * Real.exp (r^2) := by
  have h1 : 1 + r^2/3 ≤ Real.exp (r^2/3) := by
    have := Real.add_one_le_exp (r^2/3); linarith
  have hpos : (0:ℝ) < 1 + r^2/3 := by positivity
  have h2 : 1 + r ≤ 2 * (1 + r^2/3) := by nlinarith
  have h3 : (1+r)^3 ≤ (2*(1+r^2/3))^3 := by
    have h0 : (0:ℝ) ≤ 1 + r := by linarith
    gcongr
  have h4 : (1 + r^2/3)^3 ≤ (Real.exp (r^2/3))^3 := by
    have h0 : (0:ℝ) ≤ 1 + r^2/3 := le_of_lt hpos
    gcongr
  have h5 : (Real.exp (r^2/3))^3 = Real.exp (r^2) := by
    rw [← Real.exp_nat_mul]; ring_nf
  nlinarith [h3, h4, h5]
end Attack

namespace Attack

lemma sqrt3_le : Real.sqrt 3 ≤ 2 := by
  nlinarith [Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 3), Real.sqrt_nonneg 3]

lemma sqrt3_pos : 0 < Real.sqrt 3 := Real.sqrt_pos.2 (by norm_num)

lemma rpow3 (y : ℝ) (hy : 0 ≤ y) :
    (1 + y) ^ ((Module.finrank ℝ V2 : ℝ) + 1) = (1 + y)^(3:ℕ) := by
  have h : ((Module.finrank ℝ V2 : ℝ) + 1) = ((3:ℕ):ℝ) := by
    simp [finrank_euclideanSpace_fin]; norm_num
  rw [h, Real.rpow_natCast]

lemma absG (x : V2) : |G x| ≤ 4 * Real.exp (-‖x‖^2) := by
  have hn : (0:ℝ) ≤ ‖x‖ := norm_nonneg x
  have h1 : Real.exp (-2 * ‖x‖^2) ≤ Real.exp (-1 * ‖x‖^2) := by
    apply Real.exp_le_exp.2; nlinarith
  have h2 : 0 < Real.exp (-2*‖x‖^2) := Real.exp_pos _
  have h3 : 0 < Real.exp (-1*‖x‖^2) := Real.exp_pos _
  have h4 : Real.exp (-1*‖x‖^2) = Real.exp (-‖x‖^2) := by ring_nf
  rw [abs_le]
  constructor <;> simp only [G] <;> nlinarith

lemma fHatF_eq (t : V2) :
    Green42.fHat F t = 3 * (π/2) * Real.exp (-π^2 * ‖t‖^2 / 2) - π * Real.exp (-π^2 * ‖t‖^2) := by
  rw [fHatF, fHatG]

lemma pi_sq_ge : (9:ℝ) ≤ π^2 := by nlinarith [Real.pi_gt_three, Real.pi_pos]

lemma fHat_nonneg (t : V2) : 0 ≤ Green42.fHat F t := by
  rw [fHatF_eq]
  have hs : (0:ℝ) ≤ ‖t‖^2 := sq_nonneg _
  have h1 : Real.exp (-π^2 * ‖t‖^2) ≤ Real.exp (-π^2 * ‖t‖^2 / 2) := by
    apply Real.exp_le_exp.2; nlinarith [pi_sq_ge]
  have h2 : 0 < Real.exp (-π^2 * ‖t‖^2 / 2) := Real.exp_pos _
  nlinarith [Real.pi_pos]

lemma fHat_abs_bound (t : V2) : |Green42.fHat F t| ≤ 5 * π / 2 * Real.exp (-‖t‖^2) := by
  rw [fHatF_eq]
  have hn : (0:ℝ) ≤ ‖t‖ := norm_nonneg t
  have hs : (0:ℝ) ≤ ‖t‖^2 := sq_nonneg _
  have h1 : Real.exp (-π^2 * ‖t‖^2) ≤ Real.exp (-π^2 * ‖t‖^2 / 2) := by
    apply Real.exp_le_exp.2; nlinarith [pi_sq_ge]
  have h2 : Real.exp (-π^2 * ‖t‖^2 / 2) ≤ Real.exp (-‖t‖^2) := by
    apply Real.exp_le_exp.2; nlinarith [pi_sq_ge]
  have h3 : 0 < Real.exp (-π^2 * ‖t‖^2) := Real.exp_pos _
  have h4 : 0 < Real.exp (-π^2 * ‖t‖^2 / 2) := Real.exp_pos _
  rw [abs_le]
  constructor <;> nlinarith [Real.pi_pos]

theorem main : Green42.CohnElkiesOptimal 2 (Real.sqrt 3 / 6) := by
  have hF0 : F 0 = Real.sqrt 3 * π / 12 := by simp [F]
  have hfHat0 : Green42.fHat F 0 = π / 2 := by
    rw [fHatF_eq]; simp; ring
  refine ⟨F, ⟨⟨100, by norm_num, 1, by norm_num, ?_, ?_⟩, ?_, ?_, fHat_nonneg, ?_, ?_⟩, ?_⟩
  · -- decay of F
    intro x
    have hn : (0:ℝ) ≤ ‖x‖ := norm_nonneg x
    rw [rpow3 _ hn, le_div_iff₀ (by positivity)]
    by_cases hx : x = 0
    · subst hx
      have : |F 0| = Real.sqrt 3 * π / 12 := by
        rw [hF0, abs_of_nonneg (by positivity)]
      rw [this]
      simp only [norm_zero]
      nlinarith [sqrt3_le, Real.pi_le_four, Real.pi_pos, sqrt3_pos]
    · have hFx : F x = G x := by simp [F, hx]
      rw [hFx]
      have hk := key ‖x‖ hn
      have ha := absG x
      have he : Real.exp (-‖x‖^2) * Real.exp (‖x‖^2) = 1 := by
        rw [← Real.exp_add]; simp
      have hp1 : 0 < Real.exp (-‖x‖^2) := Real.exp_pos _
      have hp2 : 0 < Real.exp (‖x‖^2) := Real.exp_pos _
      have habs : 0 ≤ |G x| := abs_nonneg _
      nlinarith [pow_nonneg (by linarith : (0:ℝ) ≤ 1 + ‖x‖) 3]
  · -- decay of fHat F
    intro t
    have hn : (0:ℝ) ≤ ‖t‖ := norm_nonneg t
    rw [rpow3 _ hn, le_div_iff₀ (by positivity)]
    have hk := key ‖t‖ hn
    have ha := fHat_abs_bound t
    have he : Real.exp (-‖t‖^2) * Real.exp (‖t‖^2) = 1 := by rw [← Real.exp_add]; simp
    have hp1 : 0 < Real.exp (-‖t‖^2) := Real.exp_pos _
    have hp2 : 0 < Real.exp (‖t‖^2) := Real.exp_pos _
    have habs : 0 ≤ |Green42.fHat F t| := abs_nonneg _
    nlinarith [pow_nonneg (by linarith : (0:ℝ) ≤ 1 + ‖t‖) 3, Real.pi_le_four, Real.pi_pos]
  · -- radial
    intro x y hxy
    by_cases hx : x = 0
    · subst hx
      have hy : y = 0 := by
        rw [norm_zero] at hxy; exact norm_eq_zero.1 hxy.symm
      subst hy; rfl
    · have hy : y ≠ 0 := by
        intro h; subst h; rw [norm_zero] at hxy; exact hx (norm_eq_zero.1 hxy)
      simp [F, hx, hy, G, hxy]
  · -- spatial
    intro x hx
    have hx0 : x ≠ 0 := by
      intro h; subst h; rw [norm_zero] at hx; linarith
    have hFx : F x = G x := by simp [F, hx0]
    rw [hFx]
    have hr : (4:ℝ) ≤ ‖x‖^2 := by nlinarith [norm_nonneg x]
    have he : Real.exp (-1 * ‖x‖^2) = Real.exp (-2 * ‖x‖^2) * Real.exp (‖x‖^2) := by
      rw [← Real.exp_add]; ring_nf
    have h3 : (3:ℝ) ≤ Real.exp (‖x‖^2) := by
      nlinarith [Real.add_one_le_exp (‖x‖^2)]
    have hp : 0 < Real.exp (-2 * ‖x‖^2) := Real.exp_pos _
    simp only [G]
    nlinarith
  · rw [hfHat0]; linarith [Real.pi_pos]
  · rw [hF0]; positivity
  · rw [hF0, hfHat0]
    field_simp
    ring

theorem final : True ↔ Green42.CohnElkiesOptimal 2 (Real.sqrt 3 / 6) :=
  ⟨fun _ => main, fun _ => trivial⟩

end Attack


theorem target : fcTypeOfName% "Green42.green_42" := Attack.final