Mathlib.Analysis.Approximation.Chebyshev.Jackson

theorem finiteFourier_twice_summation_by_parts (a : ℤ → ℂ) (ha : HasFiniteSupport a) (u : ℝ) : finiteFourier (complexDelta2 a) u = (exp (-I * (u : ℂ)) - 1) ^ 2 * finiteFourier a u := by let z : ℂ := I * (u : ℂ) let F : ℤ → ℂ := fun j => a j * exp ((j : ℂ) * z) have hs (k : ℤ) : Summable (fun j : ℤ => a (j + k) * exp ((j : ℂ) * z)) := by apply summable_of_hasFiniteSupport apply Function.HasFiniteSupport.mul_left exact ha.fun_comp_of_injective (Equiv.addRight k).injective have hshift (k : ℤ) : (∑' j : ℤ, a (j + k) * exp ((j : ℂ) * z)) = exp (-(k : ℂ) * z) * (∑' j : ℤ, F j) := by calc _ = ∑' j : ℤ, exp (-(k : ℂ) * z) * F (j + k) := by congr 1 funext j dsimp [F] have he : exp (-(k : ℂ) * z) * exp (((j + k : ℤ) : ℂ) * z) = exp ((j : ℂ) * z) := by rw [← Complex.exp_add] congr 1 push_cast ring calc a (j + k) * exp ((j : ℂ) * z) = a (j + k) * (exp (-(k : ℂ) * z) * exp (((j + k : ℤ) : ℂ) * z)) := by rw [he] _ = _ := by ring _ = exp (-(k : ℂ) * z) * (∑' j : ℤ, F (j + k)) := by rw [tsum_mul_left] _ = _ := by congr 1 simpa [Equiv.addRight] using (Equiv.tsum_eq (Equiv.addRight k) F) have hexp : exp (-(2 : ℂ) * z) = exp (-z) ^ 2 := by rw [show -(2 : ℂ) * z = -z + -z by ring, Complex.exp_add] ring have hz : -z = -I * (u : ℂ) := by simp [z] have hphase (j : ℤ) : I * (j : ℂ) * (u : ℂ) = (j : ℂ) * z := by dsimp [z] ring simp only [finiteFourier, complexDelta2] simp_rw [hphase] change (∑' j : ℤ, (a (j + 2) - 2 * a (j + 1) + a j) * exp ((j : ℂ) * z)) = (exp (-I * (u : ℂ)) - 1) ^ 2 * (∑' j : ℤ, F j) simp only [add_mul, sub_mul] rw [Summable.tsum_add, Summable.tsum_sub] · rw [hshift 2] simp only [mul_assoc] rw [tsum_mul_left, hshift 1] change exp (-((2 : ℤ) : ℂ) * z) * (∑' j : ℤ, F j) - 2 * (exp (-((1 : ℤ) : ℂ) * z) * (∑' j : ℤ, F j)) + (∑' j : ℤ, F j) = (exp (-I * (u : ℂ)) - 1) ^ 2 * (∑' j : ℤ, F j) norm_num only [Int.cast_ofNat, one_mul] rw [hexp] ring_nf rw [hz] ring · exact hs 2 · simpa only [mul_assoc, ← mul_assoc] using (hs 1).mul_left (2 : ℂ) · exact (hs 2).sub (by simpa only [mul_assoc, ← mul_assoc] using (hs 1).mul_left (2 : ℂ)) · simpa only [add_zero] using hs 0

theorem kernelCoeff_eq_normalizedCoeff (N : ℕ) (hN : 0 < N) (j : ℤ) : kernelCoeff N j = normalizedCoeff N j := by let s : Finset ℤ := Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) have hs : ∀ k : ℤ, k ∈ s ↔ -k ∈ s := by intro k simp only [s, Finset.mem_Icc] omega have ha : ∀ k : ℤ, normalizedCoeff N (-k) = normalizedCoeff N k := by intro k simp only [normalizedCoeff, convolution_even] have hcoeff := cosine_coefficient_even_finite s (normalizedCoeff N) hs ha j unfold kernelCoeff simp_rw [kernel_fourier N hN] change (1 / (2 * pi)) * ∫ u in Icc (-pi) pi, (∑ k ∈ s, normalizedCoeff N k * cos ((k : ℝ) * u)) * cos ((j : ℝ) * u) = normalizedCoeff N j rw [hcoeff] by_cases hj : j ∈ s · simp [hj] · have hfar : ((2 * N - 2 : ℕ) : ℤ) < |j| := by have hj' : j ∉ Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) := hj simp only [Finset.mem_Icc] at hj' rcases le_total j 0 with h | h · rw [abs_of_nonpos h] omega · rw [abs_of_nonneg h] omega simp [hj, normalizedCoeff, convolution_support N j hfar]

theorem normalizedCoeff_delta2_l1 (N : ℕ) (hN : 0 < N) : (∑' j : ℤ, |delta2 (normalizedCoeff N) j|) ≤ 6 / (N : ℝ) := by have hraw (j : ℤ) : delta2 (convolution N) j = ∑' k : ℤ, delta (triangle N) k * delta (triangle N) (j - k) := by rw [delta2_convolution] exact (finite_convolution_tsum_eq_sum _ _ _ (delta_triangle_outside N) j).symm have hmass : (∑' j : ℤ, |delta2 (convolution N) j|) ≤ 4 * (N : ℝ) ^ 2 := by have h := finite_convolution_l1 (delta (triangle N)) (delta (triangle N)) (delta_triangle_finite N) (delta_triangle_finite N) simp_rw [← hraw] at h rw [triangle_delta_l1] at h nlinarith have hpos := convolution_zero_pos N hN have hdiff (j : ℤ) : delta2 (normalizedCoeff N) j = delta2 (convolution N) j / convolution N 0 := by unfold delta2 delta normalizedCoeff ring have hscale : (∑' j : ℤ, |delta2 (normalizedCoeff N) j|) = (∑' j : ℤ, |delta2 (convolution N) j|) / convolution N 0 := by simp_rw [hdiff, abs_div, abs_of_pos hpos, div_eq_mul_inv] rw [tsum_mul_right] rw [hscale] have hn : (0 : ℝ) < N := by exact_mod_cast hN rw [convolution_zero N] at hpos ⊢ apply (div_le_iff₀ hpos).2 rw [show 6 / (N : ℝ) * ((2 * (N : ℝ) ^ 3 + N) / 3) = (6 * ((2 * (N : ℝ) ^ 3 + N) / 3)) / N by ring] apply (le_div_iff₀ hn).2 have hmul := mul_le_mul_of_nonneg_right hmass hn.le nlinarith [sq_nonneg (N : ℝ)]

theorem packet_center_bounds : ∃ c C : ℝ, 0 < c ∧ c ≤ C ∧ ∀ N : ℕ, 2 ≤ N → c / (N : ℝ) ≤ |packetAntideriv N 0| ∧ |packetAntideriv N 0| ≤ C / (N : ℝ) := by refine ⟨1 / 72, 1 / 2, by norm_num, by norm_num, ?_⟩ intro N hN let s : Finset ℤ := Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) have hn : (0 : ℝ) < N := by exact_mod_cast (by omega : 0 < N) have hnorm (j : ℤ) : 0 ≤ normalizedCoeff N j := by unfold normalizedCoeff convolution apply div_nonneg · apply Finset.sum_nonneg intro k hk exact mul_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _) · exact le_of_lt (convolution_zero_pos N (by omega)) have hfreq (j : ℤ) (hj : j ∈ s) : 2 * (N : ℝ) ≤ 4 * (N : ℝ) + (j : ℝ) ∧ 4 * (N : ℝ) + (j : ℝ) ≤ 6 * (N : ℝ) ∧ 2 * (N : ℝ) ≤ 4 * (N : ℝ) - (j : ℝ) ∧ 4 * (N : ℝ) - (j : ℝ) ≤ 6 * (N : ℝ) := by have hj' : -((2 * N - 2 : ℕ) : ℤ) ≤ j ∧ j ≤ ((2 * N - 2 : ℕ) : ℤ) := Finset.mem_Icc.mp hj have hsub : 2 * N - 2 ≤ 2 * N := Nat.sub_le _ _ have hlo : -(2 * (N : ℤ)) ≤ j := by omega have hhi : j ≤ 2 * (N : ℤ) := by omega have hlo' : -(2 * (N : ℝ)) ≤ (j : ℝ) := by exact_mod_cast hlo have hhi' : (j : ℝ) ≤ 2 * (N : ℝ) := by exact_mod_cast hhi refine ⟨?_, ?_, ?_, ?_⟩ <;> linarith have hrec (j : ℤ) (hj : j ∈ s) (σ : ℝ) (hσ : σ = 1 ∨ σ = -1) : 1 / (36 * (N : ℝ) ^ 2) ≤ reciprocalSquare N σ j ∧ reciprocalSquare N σ j ≤ 1 / (4 * (N : ℝ) ^ 2) := by obtain ⟨hp1, hp2, hm1, hm2⟩ := hfreq j hj have hp0 : 0 < 4 * (N : ℝ) + (j : ℝ) := by linarith have hm0 : 0 < 4 * (N : ℝ) - (j : ℝ) := by linarith rcases hσ with rfl | rfl · unfold reciprocalSquare simp only [one_mul] constructor · apply one_div_le_one_div_of_le (by positivity) nlinarith [mul_nonneg (show 0 ≤ 6 * (N : ℝ) - (4 * (N : ℝ) + (j : ℝ)) by linarith) (show 0 ≤ 6 * (N : ℝ) + (4 * (N : ℝ) + (j : ℝ)) by linarith)] · apply one_div_le_one_div_of_le (by positivity) nlinarith [mul_nonneg (show 0 ≤ (4 * (N : ℝ) + (j : ℝ)) - 2 * (N : ℝ) by linarith) (show 0 ≤ (4 * (N : ℝ) + (j : ℝ)) + 2 * (N : ℝ) by linarith)] · unfold reciprocalSquare simp only [neg_mul, one_mul] constructor · apply one_div_le_one_div_of_le (by positivity) nlinarith [mul_nonneg (show 0 ≤ 6 * (N : ℝ) - (4 * (N : ℝ) - (j : ℝ)) by linarith) (show 0 ≤ 6 * (N : ℝ) + (4 * (N : ℝ) - (j : ℝ)) by linarith)] · apply one_div_le_one_div_of_le (by positivity) nlinarith [mul_nonneg (show 0 ≤ (4 * (N : ℝ) - (j : ℝ)) - 2 * (N : ℝ) by linarith) (show 0 ≤ (4 * (N : ℝ) - (j : ℝ)) + 2 * (N : ℝ) by linarith)] have hterm (j : ℤ) (hj : j ∈ s) : normalizedCoeff N j * (1 / (18 * (N : ℝ) ^ 2)) ≤ packetCoeffPlus N j + packetCoeffMinus N j ∧ packetCoeffPlus N j + packetCoeffMinus N j ≤ normalizedCoeff N j * (1 / (2 * (N : ℝ) ^ 2)) := by obtain ⟨hpL, hpU⟩ := hrec j hj 1 (inl rfl) obtain ⟨hmL, hmU⟩ := hrec j hj (-1) (inr rfl) have ha := hnorm j simp only [packetCoeffPlus, packetCoeffMinus, weightedCoeff] constructor · calc _ = normalizedCoeff N j * (1 / (36 * (N : ℝ) ^ 2)) + normalizedCoeff N j * (1 / (36 * (N : ℝ) ^ 2)) := by ring _ ≤ _ := add_le_add (mul_le_mul_of_nonneg_left hpL ha) (mul_le_mul_of_nonneg_left hmL ha) · calc _ ≤ normalizedCoeff N j * (1 / (4 * (N : ℝ) ^ 2)) + normalizedCoeff N j * (1 / (4 * (N : ℝ) ^ 2)) := add_le_add (mul_le_mul_of_nonneg_left hpU ha) (mul_le_mul_of_nonneg_left hmU ha) _ = _ := by ring have hmass : (∑ j ∈ s, normalizedCoeff N j) = ∑' j : ℤ, |normalizedCoeff N j| := by rw [tsum_eq_sum (s := s)] · simp_rw [abs_of_nonneg (hnorm _)] · intro j hj have hfar : ((2 * N - 2 : ℕ) : ℤ) < |j| := by simp only [s, Finset.mem_Icc] at hj rcases le_total j 0 with h | h · rw [abs_of_nonpos h]; omega · rw [abs_of_nonneg h]; omega simp [normalizedCoeff_support N j hfar] have hsumL : (∑ j ∈ s, normalizedCoeff N j * (1 / (18 * (N : ℝ) ^ 2))) ≤ ∑ j ∈ s, (packetCoeffPlus N j + packetCoeffMinus N j) := by apply Finset.sum_le_sum intro j hj exact (hterm j hj).1 have hsumU : (∑ j ∈ s, (packetCoeffPlus N j + packetCoeffMinus N j)) ≤ ∑ j ∈ s, normalizedCoeff N j * (1 / (2 * (N : ℝ) ^ 2)) := by apply Finset.sum_le_sum intro j hj exact (hterm j hj).2 have hsum0 : 0 ≤ ∑ j ∈ s, (packetCoeffPlus N j + packetCoeffMinus N j) := by apply Finset.sum_nonneg intro j hj exact le_trans (mul_nonneg (hnorm j) (by positivity)) (hterm j hj).1 have hcenter : |packetAntideriv N 0| = (1 / 2 : ℝ) * ∑ j ∈ s, (packetCoeffPlus N j + packetCoeffMinus N j) := by simp only [packetAntideriv, mul_zero, Real.cos_zero, mul_one] change |-(1 / 2 : ℝ) * (∑ j ∈ s, (packetCoeffPlus N j + packetCoeffMinus N j))| = _ rw [abs_mul, abs_neg, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2), abs_of_nonneg hsum0] rw [hcenter] have hmL := normalizedCoeff_l1_lower N hN have hmU := normalizedCoeff_l1 N (by omega) rw [← hmass] at hmL hmU rw [← Finset.sum_mul] at hsumL hsumU constructor · calc (1 / 72 : ℝ) / N ≤ (1 / 2 : ℝ) * ((∑ j ∈ s, normalizedCoeff N j) * (1 / (18 * (N : ℝ) ^ 2))) := by calc _ = (1 / 2 : ℝ) * ((N / 2) * (1 / (18 * (N : ℝ) ^ 2))) := by field_simp ring _ ≤ _ := by gcongr _ ≤ _ := mul_le_mul_of_nonneg_left hsumL (by norm_num) · calc _ ≤ (1 / 2 : ℝ) * ((∑ j ∈ s, normalizedCoeff N j) * (1 / (2 * (N : ℝ) ^ 2))) := mul_le_mul_of_nonneg_left hsumU (by norm_num) _ ≤ (1 / 2 : ℝ) / N := by calc _ ≤ (1 / 2 : ℝ) * ((2 * N) * (1 / (2 * (N : ℝ) ^ 2))) := by gcongr _ = _ := by field_simp

theorem normalizedCoeff_l1_lower (N : ℕ) (hN : 2 ≤ N) : (N : ℝ) / 2 ≤ ∑' j : ℤ, |normalizedCoeff N j| := by have hNpos : 0 < N := by omega have htri (j : ℤ) : 0 ≤ triangle N j := Nat.cast_nonneg _ have hconv (j : ℤ) : 0 ≤ convolution N j := by unfold convolution apply Finset.sum_nonneg intro k hk exact mul_nonneg (htri k) (htri (j - k)) have htriMass : (∑' j : ℤ, triangle N j) = (N : ℝ) ^ 2 := by simpa only [abs_of_nonneg (htri _)] using triangle_l1 N have hpair := triangle_pair_sum_eq_convolution N hNpos 0 simp only [mul_zero, Real.cos_zero, mul_one] at hpair have hmass : (∑' j : ℤ, |convolution N j|) = (N : ℝ) ^ 4 := by rw [tsum_eq_sum (s := Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ))] · simp_rw [abs_of_nonneg (hconv _)] rw [← hpair] simp_rw [← Finset.mul_sum] rw [← Finset.sum_mul] have hsum : (∑ k ∈ Icc (-(N : ℤ)) (N : ℤ), triangle N k) = (N : ℝ) ^ 2 := by rw [← htriMass] symm apply tsum_eq_sum intro k hk have : (N : ℤ) ≤ |k| := by simp only [Finset.mem_Icc] at hk rcases le_total k 0 with h | h · rw [abs_of_nonpos h] omega · rw [abs_of_nonneg h] omega exact triangle_support N k this rw [hsum] ring · intro j hj have hfar : ((2 * N - 2 : ℕ) : ℤ) < |j| := by simp only [Finset.mem_Icc] at hj rcases le_total j 0 with h | h · rw [abs_of_nonpos h] omega · rw [abs_of_nonneg h] omega simp [convolution_support N j hfar] have hpos := convolution_zero_pos N hNpos have hscale : (∑' j : ℤ, |normalizedCoeff N j|) = (∑' j : ℤ, |convolution N j|) / convolution N 0 := by simp_rw [normalizedCoeff, abs_div, abs_of_pos hpos, div_eq_mul_inv] rw [tsum_mul_right] rw [hscale, hmass, convolution_zero N] have hn : (2 : ℝ) ≤ N := by exact_mod_cast hN have hd : 0 < (2 * (N : ℝ) ^ 3 + N) / 3 := by positivity apply (le_div_iff₀ hd).2 have hs : 1 ≤ (N : ℝ) ^ 2 := by nlinarith have hp : 0 ≤ (N : ℝ) ^ 2 * ((N : ℝ) ^ 2 - 1) := mul_nonneg (sq_nonneg _) (by linarith) nlinarith [hp]

theorem packet_twice_deriv (N : ℕ) (hN : 2 ≤ N) (u : ℝ) : deriv (deriv (packetAntideriv N)) u = packetOscillation N u := by let S : Finset ℤ := Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) let p (j : ℤ) : ℝ := ((4 * (N : ℤ) + j : ℤ) : ℝ) let m (j : ℤ) : ℝ := ((4 * (N : ℤ) - j : ℤ) : ℝ) let a (j : ℤ) : ℝ := packetCoeffPlus N j let b (j : ℤ) : ℝ := packetCoeffMinus N j have hcos (c k x : ℝ) : HasDerivAt (fun y : ℝ => c * cos (k * y)) (-c * k * sin (k * x)) x := by convert ((Real.hasDerivAt_cos (k * x)).comp x ((hasDerivAt_id x).const_mul k)).const_mul c using 1 <;> first | rfl | ring have hsin (c k x : ℝ) : HasDerivAt (fun y : ℝ => c * sin (k * y)) (c * k * cos (k * x)) x := by convert ((Real.hasDerivAt_sin (k * x)).comp x ((hasDerivAt_id x).const_mul k)).const_mul c using 1 <;> first | rfl | ring have hfirst (x : ℝ) : deriv (packetAntideriv N) x = (1 / 2 : ℝ) * ∑ j ∈ S, (a j * p j * sin (p j * x) + b j * m j * sin (m j * x)) := by have ht (j : ℤ) : HasDerivAt (fun y : ℝ => a j * cos (p j * y) + b j * cos (m j * y)) (-(a j) * p j * sin (p j * x) - b j * m j * sin (m j * x)) x := by convert (hcos (a j) (p j) x).add (hcos (b j) (m j) x) using 1 <;> first | rfl | ring have hs := (HasDerivAt.fun_sum (u := S) (fun j hj => ht j)).const_mul (-1 / 2 : ℝ) have hs' := hs.deriv convert hs' using 1 · congr 1 funext y simp only [packetAntideriv, S, a, b, p, m] ring · simp only [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring have hsecond : HasDerivAt (fun x : ℝ => (1 / 2 : ℝ) * ∑ j ∈ S, (a j * p j * sin (p j * x) + b j * m j * sin (m j * x))) ((1 / 2 : ℝ) * ∑ j ∈ S, (a j * p j ^ 2 * cos (p j * u) + b j * m j ^ 2 * cos (m j * u))) u := by have ht (j : ℤ) : HasDerivAt (fun x : ℝ => a j * p j * sin (p j * x) + b j * m j * sin (m j * x)) (a j * p j ^ 2 * cos (p j * u) + b j * m j ^ 2 * cos (m j * u)) u := by convert (hsin (a j * p j) (p j) u).add (hsin (b j * m j) (m j) u) using 1 <;> first | rfl | ring convert (HasDerivAt.fun_sum (u := S) (fun j hj => ht j)).const_mul (1 / 2 : ℝ) using 1 rw [show deriv (packetAntideriv N) = fun x => (1 / 2 : ℝ) * ∑ j ∈ S, (a j * p j * sin (p j * x) + b j * m j * sin (m j * x)) from funext hfirst] rw [hsecond.deriv] have hcancel (j : ℤ) (hj : j ∈ S) : a j * p j ^ 2 = normalizedCoeff N j ∧ b j * m j ^ 2 = normalizedCoeff N j := by have hj' : -((2 * N - 2 : ℕ) : ℤ) ≤ j ∧ j ≤ ((2 * N - 2 : ℕ) : ℤ) := Finset.mem_Icc.mp hj have hp : p j ≠ 0 := by dsimp [p] have : 4 * (N : ℤ) + j ≠ 0 := by omega exact_mod_cast this have hm : m j ≠ 0 := by dsimp [m] have : 4 * (N : ℤ) - j ≠ 0 := by omega exact_mod_cast this constructor · have hden : 4 * (N : ℝ) + (1 : ℝ) * (j : ℝ) = p j := by dsimp [p]; push_cast; ring change normalizedCoeff N j * (1 / (4 * (N : ℝ) + 1 * (j : ℝ)) ^ 2) * p j ^ 2 = normalizedCoeff N j rw [hden] field_simp · have hden : 4 * (N : ℝ) + (-1 : ℝ) * (j : ℝ) = m j := by dsimp [m]; push_cast; ring change normalizedCoeff N j * (1 / (4 * (N : ℝ) + -1 * (j : ℝ)) ^ 2) * m j ^ 2 = normalizedCoeff N j rw [hden] field_simp have htrig (j : ℤ) : cos (p j * u) + cos (m j * u) = 2 * cos ((j : ℝ) * u) * cos ((4 * N : ℝ) * u) := by have hp : p j * u = (4 * N : ℝ) * u + (j : ℝ) * u := by dsimp [p]; push_cast; ring have hm : m j * u = (4 * N : ℝ) * u - (j : ℝ) * u := by dsimp [m]; push_cast; ring rw [hp, hm, Real.cos_add, Real.cos_sub] ring calc (1 / 2 : ℝ) * ∑ j ∈ S, (a j * p j ^ 2 * cos (p j * u) + b j * m j ^ 2 * cos (m j * u)) = (∑ j ∈ S, normalizedCoeff N j * cos ((j : ℝ) * u)) * cos ((4 * N : ℝ) * u) := by rw [Finset.mul_sum, Finset.sum_mul] apply Finset.sum_congr rfl intro j hj obtain ⟨hp, hm⟩ := hcancel j hj rw [hp, hm] rw [← mul_add, htrig] ring _ = packetOscillation N u := by rw [← kernel_fourier N (by omega : 0 < N) u] rfl

theorem packetAntideriv_eq_finiteFourier (N : ℕ) (u : ℝ) : packetAntideriv N u = -(1 / 2 : ℝ) * ((exp (I * (4 * (N : ℝ) * u : ℂ)) * finiteFourier (fun j => (packetCoeffPlus N j : ℂ)) u).re + (exp (I * (4 * (N : ℝ) * u : ℂ)) * finiteFourier (fun j => (packetCoeffMinus N j : ℂ)) (-u)).re) := by let s : Finset ℤ := Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) have hout (j : ℤ) (hj : j ∉ s) : packetCoeffPlus N j = 0 ∧ packetCoeffMinus N j = 0 := by have hj' : ((2 * N - 2 : ℕ) : ℤ) < |j| := by simp only [s, Finset.mem_Icc, not_and_or, not_le] at hj have ha := le_abs_self j have hb := neg_le_abs j rcases hj with hj | hj <;> omega exact ⟨weightedCoeff_support N 1 j hj', weightedCoeff_support N (-1) j hj'⟩ have hplus : finiteFourier (fun j => (packetCoeffPlus N j : ℂ)) u = ∑ j ∈ s, (packetCoeffPlus N j : ℂ) * exp (I * (j : ℂ) * (u : ℂ)) := by unfold finiteFourier apply tsum_eq_sum intro j hj simp [(hout j hj).1] have hminus : finiteFourier (fun j => (packetCoeffMinus N j : ℂ)) (-u) = ∑ j ∈ s, (packetCoeffMinus N j : ℂ) * exp (I * (j : ℂ) * ((-u : ℝ) : ℂ)) := by unfold finiteFourier apply tsum_eq_sum intro j hj simp [(hout j hj).2] have hphase (c : ℝ) (j : ℤ) (v : ℝ) : (exp (I * (4 * (N : ℝ) * u : ℂ)) * ((c : ℂ) * exp (I * (j : ℂ) * (v : ℂ)))).re = c * cos ((4 * (N : ℝ) * u) + (j : ℝ) * v) := by rw [show exp (I * (4 * (N : ℝ) * u : ℂ)) * ((c : ℂ) * exp (I * (j : ℂ) * (v : ℂ))) = (c : ℂ) * exp (((4 * (N : ℝ) * u) + (j : ℝ) * v : ℝ) * I) by calc _ = (c : ℂ) * (exp (I * (4 * (N : ℝ) * u : ℂ)) * exp (I * (j : ℂ) * (v : ℂ))) := by ring _ = _ := by rw [← Complex.exp_add] congr 1 apply congrArg exp push_cast ring] simp only [Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero, Complex.exp_ofReal_mul_I_re] rw [hplus, hminus] simp only [Finset.mul_sum, Complex.re_sum] unfold packetAntideriv congr 1 rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro j hj rw [hphase (packetCoeffPlus N j) j u, hphase (packetCoeffMinus N j) j (-u)] congr 1 <;> congr 1 <;> push_cast <;> ring

theorem packet_pointwise_localization : ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, 2 ≤ N → ∀ u : ℝ, |packetAntideriv N u| ≤ C / ((N : ℝ) * (1 + (N : ℝ) * torusDistance u) ^ 2) := by refine ⟨8192, by norm_num, ?_⟩ intro N hN u have hn : (0 : ℝ) < N := by exact_mod_cast (by omega : 0 < N) let d := torusDistance u have hd : 0 ≤ d := (torusDistance_bounds u).1 have hden : 0 < (N : ℝ) * (1 + (N : ℝ) * d) ^ 2 := by positivity have hp := finiteFourier_norm_le (weightedCoeff N 1) (weightedCoeff_finite N 1) u have hm := finiteFourier_norm_le (weightedCoeff N (-1)) (weightedCoeff_finite N (-1)) (-u) have hnear : |packetAntideriv N u| ≤ 2 / (N : ℝ) := by calc _ ≤ (‖finiteFourier (fun j => (packetCoeffPlus N j : ℂ)) u‖ + ‖finiteFourier (fun j => (packetCoeffMinus N j : ℂ)) (-u)‖) / 2 := packet_abs_le_fourier N u _ ≤ ((∑' j : ℤ, |weightedCoeff N 1 j|) + (∑' j : ℤ, |weightedCoeff N (-1) j|)) / 2 := by dsimp [packetCoeffPlus, packetCoeffMinus] gcongr _ ≤ 2 / (N : ℝ) := by have hp' := weightedCoeff_l1 N hN 1 (inl rfl) have hm' := weightedCoeff_l1 N hN (-1) (inr rfl) linarith by_cases hsmall : (N : ℝ) * d ≤ 1 · calc |packetAntideriv N u| ≤ 2 / (N : ℝ) := hnear _ ≤ 8192 / ((N : ℝ) * (1 + (N : ℝ) * d) ^ 2) := by have hsq : (1 + (N : ℝ) * d) ^ 2 ≤ 4 := by have hnd : 0 ≤ (N : ℝ) * d := mul_nonneg hn.le hd nlinarith [mul_le_mul_of_nonneg_left hsmall hnd] apply (div_le_div_iff₀ hn hden).mpr nlinarith [mul_le_mul_of_nonneg_left hsq (le_of_lt hn)] · have hlarge : 1 ≤ (N : ℝ) * d := by linarith have hdpos : 0 < d := by nlinarith have hfplus := weightedCoeff_fourier_far N hN 1 u (inl rfl) hdpos have hfminus := weightedCoeff_fourier_far N hN (-1) (-u) (inr rfl) (by simpa only [torusDistance_neg] using hdpos) have hfar : |packetAntideriv N u| ≤ 2048 / ((N : ℝ) ^ 3 * d ^ 2) := by calc _ ≤ (‖finiteFourier (fun j => (packetCoeffPlus N j : ℂ)) u‖ + ‖finiteFourier (fun j => (packetCoeffMinus N j : ℂ)) (-u)‖) / 2 := packet_abs_le_fourier N u _ ≤ (2048 / ((N : ℝ) ^ 3 * d ^ 2) + 2048 / ((N : ℝ) ^ 3 * d ^ 2)) / 2 := by dsimp [packetCoeffPlus, packetCoeffMinus] rw [torusDistance_neg] at hfminus exact div_le_div_of_nonneg_right (add_le_add hfplus hfminus) (by norm_num) _ = _ := by ring calc |packetAntideriv N u| ≤ 2048 / ((N : ℝ) ^ 3 * d ^ 2) := hfar _ ≤ 8192 / ((N : ℝ) * (1 + (N : ℝ) * d) ^ 2) := by have hsq : (1 + (N : ℝ) * d) ^ 2 ≤ 4 * ((N : ℝ) * d) ^ 2 := by nlinarith [sq_nonneg ((N : ℝ) * d - 1)] apply (div_le_div_iff₀ (by positivity) hden).mpr nlinarith [mul_le_mul_of_nonneg_left hsq (le_of_lt hn)]

theorem weightedCoeff_delta2_l1 (N : ℕ) (hN : 2 ≤ N) (σ : ℝ) (hσ : σ = 1 ∨ σ = -1) : (∑' j : ℤ, |delta2 (weightedCoeff N σ) j|) ≤ 512 / (N : ℝ) ^ 3 := by let S : Finset ℤ := Icc (-(2 * (N : ℤ))) (2 * (N : ℤ)) let f : ℤ → ℝ := normalizedCoeff N let q : ℤ → ℝ := reciprocalSquare N σ have hzero (j : ℤ) (hj : j ∉ S) (m : ℤ) (hm : 0 ≤ m ∧ m ≤ 2) : f (j + m) = 0 := by apply normalizedCoeff_support N simp only [S, Finset.mem_Icc, not_and_or, not_le] at hj rcases hj with hj | hj · rw [abs_of_nonpos (by omega : j + m ≤ 0)] omega · rw [abs_of_nonneg (by omega : 0 ≤ j + m)] omega have hzero_delta2 (j : ℤ) (hj : j ∉ S) : delta2 (weightedCoeff N σ) j = 0 := by have h0 : f j = 0 := by simpa using hzero j hj 0 ⟨by omega, by omega⟩ have h1 := hzero j hj 1 ⟨by omega, by omega⟩ have h2 := hzero j hj 2 ⟨by omega, by omega⟩ have hw0 : weightedCoeff N σ j = 0 := by change f j * q j = 0; simp [h0] have hw1 : weightedCoeff N σ (j + 1) = 0 := by change f (j + 1) * q (j + 1) = 0 simp [h1] have hw2 : weightedCoeff N σ (j + 2) = 0 := by change f (j + 2) * q (j + 2) = 0 simp [h2] simp [delta2, delta, hw0, hw1, hw2, show j + 1 + 1 = j + 2 by omega] have hs : Summable (fun j : ℤ => |delta2 (weightedCoeff N σ) j|) := summable_of_ne_finset_zero (s := S) (by intro j hj; simp [hzero_delta2 j hj]) have hf0 : Summable (fun j : ℤ => |f (j + 2)|) := summable_of_ne_finset_zero (s := S) (by intro j hj simp [hzero j hj 2 ⟨by omega, by omega⟩]) have hf1 : Summable (fun j : ℤ => |delta f (j + 1)|) := summable_of_ne_finset_zero (s := S) (by intro j hj have h1 := hzero j hj 1 ⟨by omega, by omega⟩ have h2 := hzero j hj 2 ⟨by omega, by omega⟩ simp [delta, h1, h2, show j + 1 + 1 = j + 2 by omega]) have hf2 : Summable (fun j : ℤ => |delta f j|) := summable_of_ne_finset_zero (s := S) (by intro j hj have h0 : f j = 0 := by simpa using hzero j hj 0 ⟨by omega, by omega⟩ have h1 := hzero j hj 1 ⟨by omega, by omega⟩ simp [delta, h0, h1]) have hf3 : Summable (fun j : ℤ => |delta2 f j|) := summable_of_ne_finset_zero (s := S) (by intro j hj have h0 : f j = 0 := by simpa using hzero j hj 0 ⟨by omega, by omega⟩ have h1 := hzero j hj 1 ⟨by omega, by omega⟩ have h2 := hzero j hj 2 ⟨by omega, by omega⟩ simp [delta2, delta, h0, h1, h2, show j + 1 + 1 = j + 2 by omega]) have hn : (0 : ℝ) < N := by exact_mod_cast (lt_of_lt_of_le (by norm_num : 0 < 2) hN) have hpoint (j : ℤ) : |delta2 (weightedCoeff N σ) j| ≤ (64 / (N : ℝ) ^ 4) * |f (j + 2)| + (16 / (N : ℝ) ^ 3) * |delta f (j + 1)| + (16 / (N : ℝ) ^ 3) * |delta f j| + (1 / (N : ℝ) ^ 2) * |delta2 f j| := by by_cases hj : j ∈ S · have hjabs : |j| ≤ ((2 * N : ℕ) : ℤ) := by simp only [S, Finset.mem_Icc] at hj rcases hj with ⟨hlo, hhi⟩ exact abs_le.mpr ⟨by omega, by omega⟩ have hq0 := reciprocalSquare_delta2_bound N hN σ hσ j hjabs have hq1 := reciprocalSquare_delta_bound N hN σ hσ j hjabs have hq2 : |q (j + 1)| ≤ 1 / (N : ℝ) ^ 2 := by have hwin := (reciprocalSquare_window N hN σ hσ j hjabs).2.1 dsimp [q, reciprocalSquare] rw [abs_of_nonneg (by positivity)] apply one_div_le_one_div_of_le (by positivity) gcongr rw [show weightedCoeff N σ = fun k => f k * q k by rfl, delta2_mul f q j] calc |f (j + 2) * delta2 q j + (delta f (j + 1) + delta f j) * delta q j + q (j + 1) * delta2 f j| ≤ |f (j + 2)| * |delta2 q j| + (|delta f (j + 1)| + |delta f j|) * |delta q j| + |q (j + 1)| * |delta2 f j| := by calc _ ≤ |f (j + 2) * delta2 q j| + |(delta f (j + 1) + delta f j) * delta q j| + |q (j + 1) * delta2 f j| := by simpa only [add_assoc] using (abs_add_three (f (j + 2) * delta2 q j) ((delta f (j + 1) + delta f j) * delta q j) (q (j + 1) * delta2 f j)) _ ≤ _ := by simp only [abs_mul] gcongr exact abs_add_le _ _ _ ≤ _ := by change |delta2 q j| ≤ _ at hq0 change |delta q j| ≤ _ at hq1 nlinarith [mul_le_mul_of_nonneg_left hq0 (abs_nonneg (f (j + 2))), mul_le_mul_of_nonneg_left hq1 (abs_nonneg (delta f (j + 1))), mul_le_mul_of_nonneg_left hq1 (abs_nonneg (delta f j)), mul_le_mul_of_nonneg_left hq2 (abs_nonneg (delta2 f j))] · have h0 : f j = 0 := by simpa using hzero j hj 0 ⟨by omega, by omega⟩ have h1 := hzero j hj 1 ⟨by omega, by omega⟩ have h2 := hzero j hj 2 ⟨by omega, by omega⟩ rw [hzero_delta2 j hj] simp [delta2, delta, h0, h1, h2, show j + 1 + 1 = j + 2 by omega] have hrhs : Summable (fun j : ℤ => (64 / (N : ℝ) ^ 4) * |f (j + 2)| + (16 / (N : ℝ) ^ 3) * |delta f (j + 1)| + (16 / (N : ℝ) ^ 3) * |delta f j| + (1 / (N : ℝ) ^ 2) * |delta2 f j|) := by exact (((hf0.mul_left _).add (hf1.mul_left _)).add (hf2.mul_left _)).add (hf3.mul_left _) have hmain := hs.tsum_le_tsum hpoint hrhs rw [(((hf0.mul_left _).add (hf1.mul_left _)).add (hf2.mul_left _)).tsum_add (hf3.mul_left _), ((hf0.mul_left _).add (hf1.mul_left _)).tsum_add (hf2.mul_left _), (hf0.mul_left _).tsum_add (hf1.mul_left _)] at hmain simp only [tsum_mul_left] at hmain have hshift0 : (∑' j : ℤ, |f (j + 2)|) = ∑' j : ℤ, |f j| := by simpa [Equiv.addRight] using (Equiv.tsum_eq (Equiv.addRight (2 : ℤ)) (fun j : ℤ => |f j|)) have hshift1 : (∑' j : ℤ, |delta f (j + 1)|) = ∑' j : ℤ, |delta f j| := by simpa [Equiv.addRight] using (Equiv.tsum_eq (Equiv.addRight (1 : ℤ)) (fun j : ℤ => |delta f j|)) rw [hshift0, hshift1] at hmain have hNpos : 0 < N := by omega have hm0 := normalizedCoeff_l1 N hNpos have hm1 := normalizedCoeff_delta_l1 N hNpos have hm2 := normalizedCoeff_delta2_l1 N hNpos dsimp [f] at hmain calc (∑' j : ℤ, |delta2 (weightedCoeff N σ) j|) ≤ (64 / (N : ℝ) ^ 4) * (2 * N) + (16 / (N : ℝ) ^ 3) * 4 + (16 / (N : ℝ) ^ 3) * 4 + (1 / (N : ℝ) ^ 2) * (6 / N) := by exact hmain.trans (by gcongr) _ ≤ 512 / (N : ℝ) ^ 3 := by have : (N : ℝ) ≠ 0 := ne_of_gt hn field_simp nlinarith [pow_pos hn 3]

theorem packet_shifted_support (N : ℕ) (hN : 2 ≤ N) (r : ℤ) (hr : |r| < (2 * N + 2 : ℕ) ∨ (6 * N - 2 : ℕ) < |r|) : (∫ u in Icc (-pi) pi, packetOscillation N u * cos ((r : ℝ) * u)) = 0 ∧ (∫ u in Icc (-pi) pi, packetOscillation N u * sin ((r : ℝ) * u)) = 0 := by let s : Finset ℤ := Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) have hfreq (j : ℤ) (hj : j ∈ s) : |4 * (N : ℤ) + j| ≠ |r| ∧ |4 * (N : ℤ) - j| ≠ |r| := by have hb : -(2 * (N : ℤ) - 2) ≤ j ∧ j ≤ 2 * (N : ℤ) - 2 := by change j ∈ Icc (-((2 * N - 2 : ℕ) : ℤ)) ((2 * N - 2 : ℕ) : ℤ) at hj simp only [Finset.mem_Icc] at hj omega have hp : 0 ≤ 4 * (N : ℤ) + j := by omega have hm : 0 ≤ 4 * (N : ℤ) - j := by omega rw [abs_of_nonneg hp, abs_of_nonneg hm] rcases hr with hr | hr <;> constructor <;> omega have hsin (m : ℤ) : (∫ u in Icc (-pi) pi, sin ((m : ℝ) * u)) = 0 := by by_cases hm : m = 0 · subst m; simp · rw [MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le (a := -pi) (b := pi) (by linarith [Real.pi_pos] : -pi ≤ pi)] have hm0 : (m : ℝ) ≠ 0 := by exact_mod_cast hm rw [intervalIntegral.integral_comp_mul_left sin hm0, integral_sin] simp [mul_neg, Real.cos_neg] have hmix (k : ℤ) : (∫ u in Icc (-pi) pi, cos ((k : ℝ) * u) * sin ((r : ℝ) * u)) = 0 := by have hp (u : ℝ) : cos ((k : ℝ) * u) * sin ((r : ℝ) * u) = (sin (((r + k : ℤ) : ℝ) * u) + sin (((r - k : ℤ) : ℝ) * u)) / 2 := by rw [show (((r + k : ℤ) : ℝ) * u) = (r : ℝ) * u + (k : ℝ) * u by push_cast; ring, show (((r - k : ℤ) : ℝ) * u) = (r : ℝ) * u - (k : ℝ) * u by push_cast; ring, Real.sin_add, Real.sin_sub] ring simp_rw [hp] rw [MeasureTheory.integral_div] rw [MeasureTheory.integral_add ((show Continuous (fun u : ℝ => sin (((r + k : ℤ) : ℝ) * u)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc) ((show Continuous (fun u : ℝ => sin (((r - k : ℤ) : ℝ) * u)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc)] rw [hsin, hsin] ring have hfourier (u : ℝ) : packetOscillation N u = ∑ j ∈ s, normalizedCoeff N j * ((cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u)) / 2) := by rw [packetOscillation, kernel_fourier N (by omega : 0 < N) u] simp only [Finset.sum_mul] apply Finset.sum_congr rfl intro j hj rw [show (4 * N : ℝ) * u = ((4 * (N : ℤ) : ℤ) : ℝ) * u by push_cast; ring] rw [show (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) = ((4 * (N : ℤ) : ℤ) : ℝ) * u + (j : ℝ) * u by push_cast; ring, show (((4 * (N : ℤ) - j : ℤ) : ℝ) * u) = ((4 * (N : ℤ) : ℤ) : ℝ) * u - (j : ℝ) * u by push_cast; ring, Real.cos_add, Real.cos_sub] ring have hint (j : ℤ) (f : ℝ → ℝ) (hf : Continuous f) : IntegrableOn (fun u : ℝ => normalizedCoeff N j * ((cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u)) / 2) * f u) (Icc (-pi) pi) := by exact (show Continuous (fun u : ℝ => normalizedCoeff N j * ((cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u)) / 2) * f u) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc constructor · simp_rw [hfourier, Finset.sum_mul] rw [MeasureTheory.integral_finsetSum s (fun j _ => hint j (fun u => cos ((r : ℝ) * u)) (by fun_prop))] apply Finset.sum_eq_zero intro j hj have hp := (hfreq j hj).1 have hm := (hfreq j hj).2 have hzero (k : ℤ) (hk : |k| ≠ |r|) : (∫ u in Icc (-pi) pi, cos ((k : ℝ) * u) * cos ((r : ℝ) * u)) = 0 := by have h := cosine_mode_orthogonality k r have h00 : ¬ (k = 0 ∧ r = 0) := by rintro ⟨rfl, rfl⟩ exact hk rfl simp only [h00, hk, if_false] at h exact (mul_eq_zero.mp h).resolve_left (by positivity) rw [show (fun u : ℝ => normalizedCoeff N j * ((cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u)) / 2) * cos ((r : ℝ) * u)) = (fun u : ℝ => normalizedCoeff N j / 2 * (cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) * cos ((r : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u) * cos ((r : ℝ) * u))) by funext u; ring] rw [MeasureTheory.integral_const_mul, MeasureTheory.integral_add ((show Continuous (fun u : ℝ => cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) * cos ((r : ℝ) * u)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc) ((show Continuous (fun u : ℝ => cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u) * cos ((r : ℝ) * u)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc)] rw [hzero _ hp, hzero _ hm] ring · simp_rw [hfourier, Finset.sum_mul] rw [MeasureTheory.integral_finsetSum s (fun j _ => hint j (fun u => sin ((r : ℝ) * u)) (by fun_prop))] apply Finset.sum_eq_zero intro j hj rw [show (fun u : ℝ => normalizedCoeff N j * ((cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u)) / 2) * sin ((r : ℝ) * u)) = (fun u : ℝ => normalizedCoeff N j / 2 * (cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) * sin ((r : ℝ) * u) + cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u) * sin ((r : ℝ) * u))) by funext u; ring] rw [MeasureTheory.integral_const_mul, MeasureTheory.integral_add ((show Continuous (fun u : ℝ => cos (((4 * (N : ℤ) + j : ℤ) : ℝ) * u) * sin ((r : ℝ) * u)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc) ((show Continuous (fun u : ℝ => cos (((4 * (N : ℤ) - j : ℤ) : ℝ) * u) * sin ((r : ℝ) * u)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc)] rw [hmix, hmix] ring

theorem character_gap_ge_torusDistance (u : ℝ) : 2 / Real.pi * torusDistance u ≤ ‖Complex.exp (-I * (u : ℂ)) - 1‖ := by let j : ℤ := round (u / (2 * Real.pi)) let v : ℝ := u - 2 * Real.pi * j have hp : (0 : ℝ) < 2 * Real.pi := by positivity have hj := abs_sub_round (u / (2 * Real.pi)) have hv : |v| ≤ Real.pi := by have heq : v = (2 * Real.pi) * (u / (2 * Real.pi) - (j : ℝ)) := by dsimp [v] field_simp rw [heq, abs_mul, abs_of_pos hp] have := mul_le_mul_of_nonneg_left hj hp.le nlinarith have hdist : torusDistance u ≤ |v| := by apply csInf_le · exact ⟨0, by rintro r ⟨k, rfl⟩; exact abs_nonneg _⟩ · exact ⟨j, rfl⟩ have hhalf : |v / 2| ≤ Real.pi / 2 := by rw [abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)] exact div_le_div_of_nonneg_right hv (by norm_num) have hs := Real.mul_abs_le_abs_sin hhalf have hsin : 2 / Real.pi * |v| ≤ 2 * |sin (v / 2)| := by have heq : |v / 2| = |v| / 2 := by norm_num [abs_div] rw [heq] at hs nlinarith have hperiod : exp (-I * (u : ℂ)) = exp (I * ((-v : ℝ) : ℂ)) := by have hshift : (-I * (u : ℂ)) = I * ((-v : ℝ) : ℂ) + ((-j : ℤ) : ℂ) * (2 * (Real.pi : ℂ) * I) := by dsimp [v] push_cast ring rw [hshift, Complex.exp_add, Complex.exp_int_mul_two_pi_mul_I, mul_one] rw [hperiod, Complex.norm_exp_I_mul_ofReal_sub_one] have hnorm : ‖(2 : ℝ) * sin (-v / 2)‖ = 2 * |sin (v / 2)| := by rw [neg_div, Real.sin_neg, Real.norm_eq_abs, abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 2), abs_neg] rw [hnorm] have hpos : 0 ≤ 2 / Real.pi := by positivity exact (mul_le_mul_of_nonneg_left hdist hpos).trans hsin