Mathlib.Analysis.Absolute­Value­Moment­Prior­Duality

theorem uniformApproxErrorAbs_le_iff {p : Polynomial ℝ} {e : ℝ} : uniformApproxErrorAbs p ≤ e ↔ ∀ x ∈ Icc (-1 : ℝ) 1, abs (abs x - p.eval x) ≤ e := by let f : ℝ → ℝ := fun x => abs (abs x - p.eval x) have hf : Continuous f := by fun_prop have hI : IsCompact (Icc (-1 : ℝ) 1) := isCompact_Icc have hIne : (Icc (-1 : ℝ) 1).Nonempty := ⟨0, by norm_num⟩ obtain ⟨x, hx, hmax, hge⟩ := hI.exists_sSup_image_eq_and_ge hIne hf.continuousOn constructor · intro h y hy exact (hge y hy).trans (hmax ▸ h) · intro h exact csSup_le (hIne.image f) (by rintro _ ⟨x, hx, rfl⟩ exact h x hx)

theorem bestUniformApproxErrorAbs_eq_sInf (K : ℕ) : bestUniformApproxErrorAbs K = sInf {e : ℝ | ∃ p : Polynomial ℝ, p.natDegree ≤ K ∧ e = uniformApproxErrorAbs p} := by rfl

theorem bestUniformApproxErrorAbs_nonneg (K : ℕ) : 0 ≤ bestUniformApproxErrorAbs K := by rw [bestUniformApproxErrorAbs_eq_sInf] apply le_csInf · exact ⟨uniformApproxErrorAbs 0, 0, by simp⟩ · rintro e ⟨p, -, rfl⟩ have h := (uniformApproxErrorAbs_le_iff (p := p) (e := uniformApproxErrorAbs p)).mp (le_refl _) 0 (by norm_num) exact (abs_nonneg _).trans h

theorem bestUniformApproxErrorAbs_antitone {K L : ℕ} (hKL : K ≤ L) : bestUniformApproxErrorAbs L ≤ bestUniformApproxErrorAbs K := by rw [bestUniformApproxErrorAbs_eq_sInf, bestUniformApproxErrorAbs_eq_sInf] apply csInf_le_csInf · refine ⟨0, ?_⟩ rintro e ⟨p, -, rfl⟩ have h := (uniformApproxErrorAbs_le_iff (p := p) (e := uniformApproxErrorAbs p)).mp (le_refl _) 0 (by norm_num) exact (abs_nonneg _).trans h · exact ⟨uniformApproxErrorAbs 0, 0, by simp⟩ · rintro e ⟨p, hp, rfl⟩ exact ⟨p, hp.trans hKL, rfl⟩

theorem exists_bestPolynomialAbs_interval (K : ℕ) : ∃ p : Polynomial ℝ, p.natDegree ≤ K ∧ (∀ x ∈ Icc (-1 : ℝ) 1, abs (abs x - p.eval x) ≤ bestUniformApproxErrorAbs K) := by obtain ⟨p, hp, herr⟩ := exists_bestPolynomialAbs K refine ⟨p, hp, ?_⟩ exact (uniformApproxErrorAbs_le_iff (p := p) (e := bestUniformApproxErrorAbs K)).mp herr.le

theorem bestUniformApproxErrorAbs_two_mul_add_one (m : ℕ) : bestUniformApproxErrorAbs (2 * m + 1) = bestUniformApproxErrorAbs (2 * m) := by apply le_antisymm · exact bestUniformApproxErrorAbs_antitone (by omega) · obtain ⟨p, hp, herr⟩ := exists_bestPolynomialAbs (2 * m + 1) calc bestUniformApproxErrorAbs (2 * m) ≤ uniformApproxErrorAbs (evenPart p) := bestUniformApproxErrorAbs_le_uniform (evenPart_natDegree_le hp) _ ≤ uniformApproxErrorAbs p := uniformApproxErrorAbs_evenPart_le p _ = bestUniformApproxErrorAbs (2 * m + 1) := herr

theorem exists_absExtremalDecomposition (K : ℕ) : Nonempty (AbsExtremalDecomposition K) := by obtain ⟨L, hL, hLone, hLpows, hLabs⟩ := exists_dual_abs_certificate K obtain ⟨P, N, hPone, hNone, hPN⟩ := exists_positive_half_split L hL hLone let forgetC : CompactlySupportedContinuousMap unitInterval ℝ →ₗ[ℝ] C(unitInterval, ℝ) := { toFun := fun f => f.toContinuousMap map_add' := by intro f g; ext x; rfl map_smul' := by intro c f; ext x; rfl } let Pc : CompactlySupportedContinuousMap unitInterval ℝ →ₚ[ℝ] ℝ := { toLinearMap := P.toLinearMap.comp forgetC monotone' := by intro f g hfg exact P.monotone' (fun x => hfg x) } let Nc : CompactlySupportedContinuousMap unitInterval ℝ →ₚ[ℝ] ℝ := { toLinearMap := N.toLinearMap.comp forgetC monotone' := by intro f g hfg exact N.monotone' (fun x => hfg x) } let μP : Measure unitInterval := RealRMK.rieszMeasure Pc let μN : Measure unitInterval := RealRMK.rieszMeasure Nc haveI : IsFiniteMeasure μP := by dsimp [μP]; infer_instance haveI : IsFiniteMeasure μN := by dsimp [μN]; infer_instance have hμP (c : C(unitInterval, ℝ)) : ∫ x, c x ∂μP = P c := by let cc := CompactlySupportedContinuousMap.continuousMapEquiv c have h := RealRMK.integral_rieszMeasure Pc cc calc (∫ x, c x ∂μP) = ∫ x, cc x ∂RealRMK.rieszMeasure Pc := by simp [μP, cc] _ = Pc cc := h _ = P c := rfl have hμN (c : C(unitInterval, ℝ)) : ∫ x, c x ∂μN = N c := by let cc := CompactlySupportedContinuousMap.continuousMapEquiv c have h := RealRMK.integral_rieszMeasure Nc cc calc (∫ x, c x ∂μN) = ∫ x, cc x ∂RealRMK.rieszMeasure Nc := by simp [μN, cc] _ = Nc cc := h _ = N c := rfl have hmassP : μP univ = (1 / 2 : ENNReal) := by have h := hμP (1 : C(unitInterval, ℝ)) change (∫ _ : unitInterval, (1 : ℝ) ∂μP) = P 1 at h rw [integral_const] at h simp only [smul_eq_mul, mul_one, hPone] at h have htr : (μP univ).toReal = ((1 / 2 : ENNReal)).toReal := by simpa [measureReal_def] using h rcases (ENNReal.toReal_eq_toReal_iff _ _).mp htr with h | h | h · exact h · exact elim (by simpa using h.2) · exact elim ((measure_ne_top μP univ) h.1) have hmassN : μN univ = (1 / 2 : ENNReal) := by have h := hμN (1 : C(unitInterval, ℝ)) change (∫ _ : unitInterval, (1 : ℝ) ∂μN) = N 1 at h rw [integral_const] at h simp only [smul_eq_mul, mul_one, hNone] at h have htr : (μN univ).toReal = ((1 / 2 : ENNReal)).toReal := by simpa [measureReal_def] using h rcases (ENNReal.toReal_eq_toReal_iff _ _).mp htr with h | h | h · exact h · exact elim (by simpa using h.2) · exact elim ((measure_ne_top μN univ) h.1) let positive := symmPush μP let negative := symmPush μN refine ⟨{ positive := positive negative := negative finite_positive := by constructor dsimp only [positive] rw [symmPush_mass μP hmassP] norm_num finite_negative := by constructor dsimp only [negative] rw [symmPush_mass μN hmassN] norm_num positive_mass := by exact symmPush_mass μP hmassP negative_mass := by exact symmPush_mass μN hmassN positive_supported := by exact symmPush_supported μP negative_supported := by exact symmPush_supported μN positive_symmetric := by exact symmPush_symmetric μP negative_symmetric := by exact symmPush_symmetric μN moments_eq := ?_ abs_gap := ?_ }⟩ · intro j hj let rpow : C(unitInterval, ℝ) := ⟨fun x => (-(x : ℝ)) ^ j, by fun_prop⟩ have hrpow : rpow = (-1 : ℝ) ^ j • dualPow j := by ext x change (-(x : ℝ)) ^ j = (-1 : ℝ) ^ j * (x : ℝ) ^ j rw [neg_pow] have hLrpow : L rpow = 0 := by rw [hrpow, map_smul, hLpows j hj, smul_zero] have h₁ := hPN (dualPow j) have h₂ := hPN rpow have hp₁ : (∫ x : unitInterval, (x : ℝ) ^ j ∂μP) = P (dualPow j) := hμP (dualPow j) have hp₂ : (∫ x : unitInterval, (-(x : ℝ)) ^ j ∂μP) = P rpow := hμP rpow have hn₁ : (∫ x : unitInterval, (x : ℝ) ^ j ∂μN) = N (dualPow j) := hμN (dualPow j) have hn₂ : (∫ x : unitInterval, (-(x : ℝ)) ^ j ∂μN) = N rpow := hμN rpow have hp := integral_symmPush μP (fun x : ℝ => x ^ j) (by fun_prop) have hn := integral_symmPush μN (fun x : ℝ => x ^ j) (by fun_prop) change ∫ x : ℝ, x ^ j ∂positive = ∫ x : ℝ, x ^ j ∂negative dsimp only [positive, negative] rw [hp, hn] rw [hp₁, hp₂, hn₁, hn₂] rw [hLpows j hj] at h₁ rw [hLrpow] at h₂ linarith · let rabs : C(unitInterval, ℝ) := ⟨fun x => |-(x : ℝ)|, by fun_prop⟩ have hrabs : rabs = dualAbs := by ext x; simp [rabs, dualAbs] have h₁ := hPN dualAbs have h₂ := hPN rabs have hp₁ : (∫ x : unitInterval, |(x : ℝ)| ∂μP) = P dualAbs := hμP dualAbs have hp₂ : (∫ x : unitInterval, |-(x : ℝ)| ∂μP) = P rabs := hμP rabs have hn₁ : (∫ x : unitInterval, |(x : ℝ)| ∂μN) = N dualAbs := hμN dualAbs have hn₂ : (∫ x : unitInterval, |-(x : ℝ)| ∂μN) = N rabs := hμN rabs have hp := integral_symmPush μP (fun x : ℝ => |x|) (by fun_prop) have hn := integral_symmPush μN (fun x : ℝ => |x|) (by fun_prop) change (∫ x : ℝ, |x| ∂positive) - (∫ x : ℝ, |x| ∂negative) = bestUniformApproxErrorAbs K dsimp only [positive, negative] rw [hp, hn] rw [hp₁, hp₂, hn₁, hn₂] rw [hrabs] at h₂ rw [hLabs] at h₁ h₂ rw [hrabs] linarith

lemma integral_fourier (k : ℤ) : (∫ x : AddCircle pi, fourier k x ∂AddCircle.haarAddCircle) = if k = 0 then 1 else 0 := by have h := congrFun (fourierCoeff_fourier (T := pi) k) 0 rw [fourierCoeff] at h simp only [neg_zero, fourier_zero, one_smul] at h by_cases hk : k = 0 · subst k simpa using h · simpa [hk, Ne.symm hk] using h

lemma fejer_integrand_expand (n k : ℕ) (t : AddCircle pi) : (fejerKernel n t : ℂ) * fourier (k : ℤ) t = (n : ℂ)⁻¹ * ∑ r ∈ range n, ∑ s ∈ range n, fourier ((r : ℤ) - (s : ℤ) + (k : ℤ)) t := by rw [fejerKernel, Complex.sq_norm] simp only [Complex.ofReal_div, Complex.ofReal_natCast] rw [← Complex.mul_conj] simp only [oneSidedFourierSum, ContinuousMap.sum_apply, map_sum] simp_rw [← fourier_neg] simp_rw [div_eq_mul_inv, Finset.sum_mul, Finset.mul_sum] apply Finset.sum_congr rfl intro r hr rw [Finset.sum_mul, Finset.sum_mul] apply Finset.sum_congr rfl intro s hs rw [← fourier_add] rw [show fourier ((r : ℤ) + -(s : ℤ)) t * (n : ℂ)⁻¹ * fourier (k : ℤ) t = (n : ℂ)⁻¹ * (fourier ((r : ℤ) + -(s : ℤ)) t * fourier (k : ℤ) t) by ring] rw [← fourier_add] congr 2

lemma fejerMean_fourier_nat (n k : ℕ) (hn : 0 < n) : fejerMean n (fourier (k : ℤ)) = if k < n then ((n - k : ℕ) : ℝ) / n else 0 := by rw [fejerMean] simp_rw [fejer_integrand_expand] have hfourier (j : ℤ) : Integrable (fourier j : AddCircle pi → ℂ) haarAddCircle := (fourier j).continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _) have hinner (r : ℕ) : Integrable (fun t : AddCircle pi => ∑ s ∈ range n, fourier ((r : ℤ) - (s : ℤ) + (k : ℤ)) t) haarAddCircle := (show Continuous (fun t : AddCircle pi => ∑ s ∈ range n, fourier ((r : ℤ) - (s : ℤ) + (k : ℤ)) t) by fun_prop).integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _) rw [integral_const_mul] rw [integral_finset_sum (range n) (fun r hr => hinner r)] simp_rw [integral_finset_sum (range n) (fun s hs => hfourier ((_ : ℤ) - (s : ℤ) + (k : ℤ)))] simp_rw [integral_fourier] have hinner_sum (r : ℕ) : (∑ s ∈ range n, if (r : ℤ) - (s : ℤ) + (k : ℤ) = 0 then (1 : ℂ) else 0) = if r + k < n then 1 else 0 := by by_cases h : r + k < n · rw [if_pos h, Finset.sum_eq_single (r + k)] · simp · intro b hb hne simp only [ite_eq_right_iff] intro heq have : b = r + k := by omega exact (hne this).elim · simp [h] · rw [if_neg h] apply Finset.sum_eq_zero intro b hb simp only [ite_eq_right_iff] intro heq have : b = r + k := by omega subst b exact (h (Finset.mem_range.mp hb)).elim simp_rw [hinner_sum] by_cases hk : k < n · rw [if_pos hk] have hset : filter (fun r => r + k < n) (range n) = range (n - k) := by ext r simp omega rw [← Finset.sum_filter, hset] simp field_simp · rw [if_neg hk] have hzero : (∑ r ∈ range n, if r + k < n then (1 : ℂ) else 0) = 0 := by apply Finset.sum_eq_zero intro r hr rw [if_neg] omega rw [hzero] simp

lemma fejerMean_fourier_neg_nat (n k : ℕ) (hn : 0 < n) : fejerMean n (fourier (-(k : ℤ))) = if k < n then ((n - k : ℕ) : ℝ) / n else 0 := by rw [fejerMean] simp_rw [fourier_neg] calc (∫ t, (fejerKernel n t : ℂ) * (starRingEnd ℂ) (fourier (k : ℤ) t) ∂AddCircle.haarAddCircle) = (starRingEnd ℂ) (∫ t, (fejerKernel n t : ℂ) * fourier (k : ℤ) t ∂AddCircle.haarAddCircle) := by rw [← integral_conj] congr 1 funext t simp _ = _ := by rw [← fejerMean, fejerMean_fourier_nat n k hn] split <;> simp

lemma integral_fejerKernel (n : ℕ) (hn : 0 < n) : (∫ t, fejerKernel n t ∂AddCircle.haarAddCircle) = 1 := by have hcomplex := fejerMean_fourier_nat n 0 hn simp only [if_pos hn, Nat.cast_sub (zero_le _), cast_zero, sub_zero] at hcomplex have hker : Integrable (fejerKernel n) haarAddCircle := (continuous_fejerKernel n).integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _) have hmap := Complex.ofRealCLM.integral_comp_comm hker rw [show (fun t : AddCircle pi => Complex.ofRealCLM (fejerKernel n t)) = (fun t => (fejerKernel n t : ℂ)) by rfl] at hmap rw [fejerMean] at hcomplex simp only [fourier_zero, mul_one] at hcomplex have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) rw [div_self hnR] at hcomplex have : ((∫ t, fejerKernel n t ∂AddCircle.haarAddCircle : ℝ) : ℂ) = 1 := by calc ((∫ t, fejerKernel n t ∂AddCircle.haarAddCircle : ℝ) : ℂ) = ∫ t, (fejerKernel n t : ℂ) ∂AddCircle.haarAddCircle := hmap.symm _ = 1 := hcomplex exact_mod_cast this

lemma fejerMean_norm_le (n : ℕ) (hn : 0 < n) (f : C(AddCircle pi, ℂ)) (E : ℝ) (hE : ∀ t, ‖f t‖ ≤ E) : ‖fejerMean n f‖ ≤ E := by have hnonneg (t : AddCircle pi) : 0 ≤ fejerKernel n t := by exact div_nonneg (sq_nonneg _) (Nat.cast_nonneg _) have hleft : Integrable (fun t : AddCircle pi => fejerKernel n t * ‖f t‖) haarAddCircle := (show Continuous (fun t : AddCircle pi => fejerKernel n t * ‖f t‖) by exact (continuous_fejerKernel n).mul (f.continuous.norm)).integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _) have hright : Integrable (fun t : AddCircle pi => fejerKernel n t * E) haarAddCircle := (show Continuous (fun t : AddCircle pi => fejerKernel n t * E) by exact (continuous_fejerKernel n).mul continuous_const).integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _) calc ‖fejerMean n f‖ ≤ ∫ t, ‖(fejerKernel n t : ℂ) * f t‖ ∂AddCircle.haarAddCircle := by exact norm_integral_le_integral_norm _ _ = ∫ t, fejerKernel n t * ‖f t‖ ∂AddCircle.haarAddCircle := by apply integral_congr_ae filter_upwards [] with t rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg (hnonneg t)] _ ≤ ∫ t, fejerKernel n t * E ∂AddCircle.haarAddCircle := by apply integral_mono hleft hright intro t exact mul_le_mul_of_nonneg_left (hE t) (hnonneg t) _ = E := by rw [integral_mul_const, integral_fejerKernel n hn, one_mul]

lemma valleePoussinMean_fourier_nat (n k : ℕ) (hn : 0 < n) (hk : k ≤ n) : valleePoussinMeanCLM n hn (fourier (k : ℤ)) = 1 := by rw [valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, smul_eq_mul, fejerMeanCLM_apply] rw [fejerMean_fourier_nat (2 * n) k (by omega), fejerMean_fourier_nat n k hn] by_cases hlt : k < n · rw [if_pos hlt, if_pos (by omega)] push_cast have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) rw [Nat.cast_sub (by omega : k ≤ 2 * n), Nat.cast_sub (by omega : k ≤ n)] push_cast field_simp ring exact mul_inv_cancel₀ (by exact_mod_cast (Nat.ne_of_gt hn) : (n : ℂ) ≠ 0) · have hkn : k = n := by omega subst k rw [if_neg (Nat.lt_irrefl _), if_pos (by omega)] push_cast have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) rw [Nat.cast_sub (by omega : n ≤ 2 * n)] push_cast field_simp ring exact mul_inv_cancel₀ (by exact_mod_cast (Nat.ne_of_gt hn) : (n : ℂ) ≠ 0)

lemma valleePoussinMean_fourier_neg_nat (n k : ℕ) (hn : 0 < n) (hk : k ≤ n) : valleePoussinMeanCLM n hn (fourier (-(k : ℤ))) = 1 := by rw [valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, smul_eq_mul, fejerMeanCLM_apply] rw [fejerMean_fourier_neg_nat (2 * n) k (by omega), fejerMean_fourier_neg_nat n k hn] by_cases hlt : k < n · rw [if_pos hlt, if_pos (by omega)] push_cast have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) rw [Nat.cast_sub (by omega : k ≤ 2 * n), Nat.cast_sub (by omega : k ≤ n)] push_cast field_simp ring exact mul_inv_cancel₀ (by exact_mod_cast (Nat.ne_of_gt hn) : (n : ℂ) ≠ 0) · have hkn : k = n := by omega subst k rw [if_neg (Nat.lt_irrefl _), if_pos (by omega)] push_cast have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn) rw [Nat.cast_sub (by omega : n ≤ 2 * n)] push_cast field_simp ring exact mul_inv_cancel₀ (by exact_mod_cast (Nat.ne_of_gt hn) : (n : ℂ) ≠ 0)

lemma cuspFunctional_fourier_nat_nonneg (n k : ℕ) (hn : 0 < n) : 0 ≤ (cuspFunctionalCLM n hn (fourier (k : ℤ))).re := by rw [cuspFunctionalCLM, valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousMap.evalCLM_apply, ContinuousLinearMap.smul_apply, smul_eq_mul, fejerMeanCLM_apply, fourier_eval_zero] rw [fejerMean_fourier_nat (2 * n) k (by omega), fejerMean_fourier_nat n k hn] by_cases hk2 : k < 2 * n · rw [if_pos hk2] by_cases hk : k < n · rw [if_pos hk] simp only [Complex.sub_re, Complex.one_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, zero_mul, sub_zero] norm_num push_cast rw [Nat.cast_sub (by omega : k ≤ 2 * n), Nat.cast_sub (by omega : k ≤ n)] push_cast have hnR : (0 : ℝ) < n := by exact_mod_cast hn field_simp nlinarith · rw [if_neg hk] simp only [Complex.sub_re, Complex.one_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, zero_mul, sub_zero] norm_num push_cast rw [Nat.cast_sub (by omega : k ≤ 2 * n)] push_cast have hnR : (0 : ℝ) < n := by exact_mod_cast hn have hkR : (n : ℝ) ≤ k := by exact_mod_cast Nat.le_of_not_gt hk field_simp nlinarith · rw [if_neg hk2, if_neg (by omega : ¬ k < n)] norm_num

lemma cuspFunctional_fourier_neg_nat_nonneg (n k : ℕ) (hn : 0 < n) : 0 ≤ (cuspFunctionalCLM n hn (fourier (-(k : ℤ)))).re := by rw [cuspFunctionalCLM, valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousMap.evalCLM_apply, ContinuousLinearMap.smul_apply, smul_eq_mul, fejerMeanCLM_apply, fourier_eval_zero] rw [fejerMean_fourier_neg_nat (2 * n) k (by omega), fejerMean_fourier_neg_nat n k hn] by_cases hk2 : k < 2 * n · rw [if_pos hk2] by_cases hk : k < n · rw [if_pos hk] simp only [Complex.sub_re, Complex.one_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, zero_mul, sub_zero] norm_num push_cast rw [Nat.cast_sub (by omega : k ≤ 2 * n), Nat.cast_sub (by omega : k ≤ n)] push_cast have hnR : (0 : ℝ) < n := by exact_mod_cast hn field_simp nlinarith · rw [if_neg hk] simp only [Complex.sub_re, Complex.one_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, zero_mul, sub_zero] norm_num push_cast rw [Nat.cast_sub (by omega : k ≤ 2 * n)] push_cast have hnR : (0 : ℝ) < n := by exact_mod_cast hn have hkR : (n : ℝ) ≤ k := by exact_mod_cast Nat.le_of_not_gt hk field_simp nlinarith · rw [if_neg hk2, if_neg (by omega : ¬ k < n)] norm_num

lemma cuspFunctional_fourier_nat_high (n k : ℕ) (hn : 0 < n) (hk : 2 * n ≤ k) : cuspFunctionalCLM n hn (fourier (k : ℤ)) = 1 := by rw [cuspFunctionalCLM, valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousMap.evalCLM_apply, ContinuousLinearMap.smul_apply, smul_eq_mul, fejerMeanCLM_apply, fourier_eval_zero] rw [fejerMean_fourier_nat (2 * n) k (by omega), fejerMean_fourier_nat n k hn, if_neg (by omega : ¬ k < 2 * n), if_neg (by omega : ¬ k < n)] norm_num

lemma cuspFunctional_fourier_neg_nat_high (n k : ℕ) (hn : 0 < n) (hk : 2 * n ≤ k) : cuspFunctionalCLM n hn (fourier (-(k : ℤ))) = 1 := by rw [cuspFunctionalCLM, valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousMap.evalCLM_apply, ContinuousLinearMap.smul_apply, smul_eq_mul, fejerMeanCLM_apply, fourier_eval_zero] rw [fejerMean_fourier_neg_nat (2 * n) k (by omega), fejerMean_fourier_neg_nat n k hn, if_neg (by omega : ¬ k < 2 * n), if_neg (by omega : ¬ k < n)] norm_num

lemma cuspFunctional_norm_apply_le (n : ℕ) (hn : 0 < n) (f : C(AddCircle pi, ℂ)) : ‖cuspFunctionalCLM n hn f‖ ≤ 4 * ‖f‖ := by rw [cuspFunctionalCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousMap.evalCLM_apply] calc ‖f 0 - valleePoussinMeanCLM n hn f‖ ≤ ‖f 0‖ + ‖valleePoussinMeanCLM n hn f‖ := norm_sub_le _ _ _ ≤ ‖f‖ + (2 * ‖f‖ + ‖f‖) := by gcongr · exact ContinuousMap.norm_coe_le_norm f 0 · rw [valleePoussinMeanCLM] simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, smul_eq_mul] calc ‖2 * fejerMeanCLM (2 * n) (by omega) f - fejerMeanCLM n hn f‖ ≤ ‖2 * fejerMeanCLM (2 * n) (by omega) f‖ + ‖fejerMeanCLM n hn f‖ := norm_sub_le _ _ _ ≤ 2 * ‖f‖ + ‖f‖ := by rw [norm_mul] norm_num gcongr · simpa [fejerMeanCLM] using fejerMean_norm_le (2 * n) (by omega) f ‖f‖ (fun t => ContinuousMap.norm_coe_le_norm f t) · simpa [fejerMeanCLM] using fejerMean_norm_le n hn f ‖f‖ (fun t => ContinuousMap.norm_coe_le_norm f t) _ = 4 * ‖f‖ := by ring

lemma fourier_pair_eq (A B : ℝ) (k : ℕ) (t : ℝ) : (((A : ℂ) - B * I) / 2) * fourier (k : ℤ) (t : AddCircle Real.pi) + (((A : ℂ) + B * I) / 2) * fourier (-(k : ℤ)) (t : AddCircle Real.pi) = ((A * cos (2 * k * t) + B * sin (2 * k * t) : ℝ) : ℂ) := by rw [fourier_coe_apply, fourier_coe_apply] have hpi : (Real.pi : ℂ) ≠ 0 := by exact_mod_cast Real.pi_ne_zero rw [show 2 * (Real.pi : ℂ) * I * (((k : ℕ) : ℤ) : ℂ) * (t : ℂ) / Real.pi = ((2 * (k : ℝ) * t : ℝ) : ℂ) * I by field_simp push_cast ring] simp only [Int.cast_neg] rw [show 2 * (Real.pi : ℂ) * I * (-(((k : ℕ) : ℤ) : ℂ)) * (t : ℂ) / Real.pi = (-((2 * (k : ℝ) * t : ℝ) : ℂ)) * I by field_simp push_cast ring] rw [Complex.exp_mul_I, Complex.exp_mul_I] simp only [Complex.cos_neg, Complex.sin_neg] push_cast ring_nf rw [Complex.I_sq] ring

lemma fourier_comp_circleDouble (j : ℤ) : (fourier j).comp circleDouble = fourier (2 * j) := by ext t simp only [ContinuousMap.comp_apply, circleDouble, fourier_apply] congr 2 change j • (2 • t) = (2 * j) • t change j • ((2 : ℤ) • t) = _ rw [← mul_zsmul, mul_comm]

theorem bestUniformApproxErrorAbs_upper (K : ℕ) (hK : 0 < K) : bestUniformApproxErrorAbs K ≤ 1 / (K : ℝ) := by let m := K / 2 have hmdeg : 2 * m ≤ K := by dsimp [m] omega calc bestUniformApproxErrorAbs K ≤ uniformApproxErrorAbs (absChebPoly m) := bestUniformApproxErrorAbs_le_explicit (absChebPoly_natDegree_le m |>.trans hmdeg) _ ≤ 2 / (pi * (2 * (m : ℝ) + 1)) := by apply uniformApproxErrorAbs_le_iff.mpr intro x hx exact absChebPoly_error_le m hx _ ≤ 1 / (K : ℝ) := by have hKreal : (0 : ℝ) < K := by exact_mod_cast hK have hmreal : (0 : ℝ) < 2 * (m : ℝ) + 1 := by positivity have hnat : K ≤ 2 * m + 1 := by dsimp [m] omega have hnatreal : (K : ℝ) ≤ 2 * (m : ℝ) + 1 := by exact_mod_cast hnat have hprod : 2 * (K : ℝ) ≤ pi * (2 * (m : ℝ) + 1) := calc 2 * (K : ℝ) ≤ 2 * (2 * (m : ℝ) + 1) := mul_le_mul_of_nonneg_left hnatreal (by norm_num) _ ≤ pi * (2 * (m : ℝ) + 1) := mul_le_mul_of_nonneg_right Real.two_le_pi hmreal.le exact (div_le_div_iff₀ (mul_pos Real.pi_pos hmreal) hKreal).mpr (by simpa using hprod)

theorem bestUniformApproxErrorAbs_lower (K : ℕ) (hK : 0 < K) : (1 / 100 : ℝ) / (K : ℝ) ≤ bestUniformApproxErrorAbs K := by -- Symmetrizing a best approximant and using only a Markov derivative bound -- gives `K⁻²`, so a genuine inverse estimate is needed. A concrete route -- is the de la Vallée--Poussin certificate on `AddCircle pi`. For the -- normalized Fejér kernel `F_n(t) = n⁻¹ * ‖∑_{r < n} fourier r t‖²`, the -- kernel `V_n = 2 * F_(2*n) - F_n` has `L¹` norm at most `3` and Fourier -- multiplier exactly `1` on `|j| ≤ n`. Evaluation at the cusp minus -- convolution with `V_n` therefore has norm at most `4` and annihilates -- every even polynomial mode of degree at most `2*n`. The formula -- `fourierCoeff_sinCircle` makes its value on `|sin|` a positive tail; -- retaining only `2*n ≤ j < 4*n` gives a constant-over-`n` lower bound. -- Reduce odd `K` with `bestUniformApproxErrorAbs_two_mul_add_one`. -- Do not replace this with a coefficient-at-one-frequency estimate or with -- two shifted uniform grids: both give only `K⁻²` for `|cos|`. obtain ⟨p, hpdeg, hpbest⟩ := exists_bestPolynomialAbs K obtain ⟨q, hqeval, hqann⟩ := exists_fourierPoly_sinDouble p K hK hpdeg let residual : C(AddCircle pi, ℂ) := doubleSinCircle - q have hresidual_norm : ‖residual‖ ≤ uniformApproxErrorAbs p := by apply (ContinuousMap.norm_le_of_nonempty _).mpr intro z obtain ⟨t, ht, heq⟩ := AddCircle.eq_coe_Ioc z rw [← heq] change ‖doubleSinCircle (t : AddCircle pi) - q (t : AddCircle pi)‖ ≤ _ rw [doubleSinCircle_apply, hqeval] simp only [← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] exact ((uniformApproxErrorAbs_le_iff (p := p) (e := uniformApproxErrorAbs p)).mp (le_refl _)) (sin (2 * t)) ⟨Real.neg_one_le_sin _, Real.sin_le_one _⟩ have hfunctional_residual : cuspFunctionalCLM K hK residual = cuspFunctionalCLM K hK doubleSinCircle := by simp only [residual, map_sub, hqann, sub_zero] have hcertificate : 1 / (16 * (K : ℝ)) ≤ ‖cuspFunctionalCLM K hK residual‖ := by calc 1 / (16 * (K : ℝ)) ≤ -(cuspFunctionalCLM K hK doubleSinCircle).re := cuspFunctional_doubleSinCircle_lower K hK _ ≤ |-(cuspFunctionalCLM K hK doubleSinCircle).re| := le_abs_self _ _ = |(cuspFunctionalCLM K hK doubleSinCircle).re| := abs_neg _ _ ≤ ‖cuspFunctionalCLM K hK doubleSinCircle‖ := Complex.abs_re_le_norm _ _ = ‖cuspFunctionalCLM K hK residual‖ := by rw [hfunctional_residual] have herror : 1 / (16 * (K : ℝ)) ≤ 4 * uniformApproxErrorAbs p := hcertificate.trans ((cuspFunctional_norm_apply_le K hK residual).trans (mul_le_mul_of_nonneg_left hresidual_norm (by norm_num))) have hKR : (0 : ℝ) < K := by exact_mod_cast hK have h64 : 1 / (64 * (K : ℝ)) ≤ uniformApproxErrorAbs p := by have hid : 1 / (64 * (K : ℝ)) = (1 / (16 * (K : ℝ))) / 4 := by field_simp ring rw [hid] linarith rw [← hpbest] exact (by rw [div_div] apply (div_le_div_iff₀ (by positivity : 0 < (100 : ℝ) * K) (by positivity : 0 < (64 : ℝ) * K)).2 nlinarith : (1 / 100 : ℝ) / K ≤ 1 / (64 * K)).trans h64