fejer_sum_sub_f_eq_integral

theorem fejer_sum_sub_f_eq_integral {f : ℝ → ℝ} (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :    fejer_sum f n x - f x = (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, (f (x - t) - f x) * fejer_kernel n t := by      -- By definition of Fejér sum, we have      have h_def : fejer_sum f n x = (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, f (x - t) * fejer_kernel n t := by        convert fejer_sum_eq_integral_alt_v2 hf_int hf_per n x using 1;      simp +decide [ h_def, sub_mul ];      rw [ intervalIntegral.integral_sub ] <;> norm_num;      · field_simp;        rw [ show ∫ t in -Real.pi..Real.pi, fejer_kernel n t = Real.pi by              have := fejer_kernel_integral_one n;              rw [ div_mul_eq_mul_div, div_eq_iff ] at this <;> linarith [ Real.pi_pos ] ] ; ring;      · have h_integrable : IntervalIntegrable (fun t => f (x - t)) MeasureTheory.volume (-Real.pi) Real.pi := by          rw [ intervalIntegrable_iff_integrableOn_Ioc_of_le ( by linarith [ Real.pi_pos ] ) ] at *;          have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume := by            have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (-Real.pi) Real.pi) MeasureTheory.volume := by              rwa [ MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_congr_set MeasureTheory.Ioc_ae_eq_Icc ] at *;            -- Since $f$ is periodic with period $2\pi$, we can shift the interval of integration.            have h_shift : ∀ k : ℤ, MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (-Real.pi + k * 2 * Real.pi) (Real.pi + k * 2 * Real.pi)) MeasureTheory.volume := by              intro k;              have h_shift : ∀ k : ℤ, MeasureTheory.IntegrableOn (fun t => f (t - k * 2 * Real.pi)) (Set.Icc (-Real.pi + k * 2 * Real.pi) (Real.pi + k * 2 * Real.pi)) MeasureTheory.volume := by                intro k;                rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;                convert h_integrable.comp_sub_right ( k * 2 * Real.pi ) using 1;                ext; simp [Set.indicator];                split_ifs <;> ring_nf at * <;> aesop;              convert h_shift k using 1;              exact funext fun t => by simpa [ mul_assoc ] using Function.Periodic.int_mul hf_per k ( t - k * 2 * Real.pi ) ;            -- Choose $k$ such that $x - \pi \in [-\pi + k * 2 * \pi, \pi + k * 2 * \pi]$.            obtain ⟨k, hk⟩ : ∃ k : ℤ, x - Real.pi ∈ Set.Icc (-Real.pi + k * 2 * Real.pi) (Real.pi + k * 2 * Real.pi) := by              exact ⟨ ⌊ ( x - Real.pi + Real.pi ) / ( 2 * Real.pi ) ⌋, by nlinarith [ Int.floor_le ( ( x - Real.pi + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( x - Real.pi + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ], by nlinarith [ Int.lt_floor_add_one ( ( x - Real.pi + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( x - Real.pi + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] ⟩;            have h_shift : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (-Real.pi + k * 2 * Real.pi) (Real.pi + k * 2 * Real.pi)) MeasureTheory.volume := by              exact h_shift k;            have h_shift : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (x - Real.pi) (x + Real.pi)) MeasureTheory.volume := by              have h_subset : Set.Icc (x - Real.pi) (x + Real.pi) ⊆ Set.Icc (-Real.pi + k * 2 * Real.pi) (Real.pi + k * 2 * Real.pi) ∪ Set.Icc (-Real.pi + (k + 1) * 2 * Real.pi) (Real.pi + (k + 1) * 2 * Real.pi) := by                exact fun t ht => if h : t ≤ Real.pi + k * 2 * Real.pi then Or.inl ⟨ by linarith [ ht.1, hk.1 ], by linarith [ ht.2, hk.2 ] ⟩ else Or.inr ⟨ by linarith [ ht.1, hk.1 ], by linarith [ ht.2, hk.2 ] ⟩              have h_shift : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (-Real.pi + (k + 1) * 2 * Real.pi) (Real.pi + (k + 1) * 2 * Real.pi)) MeasureTheory.volume := by                convert ‹∀ k : ℤ, MeasureTheory.IntegrableOn ( fun t => f t ) ( Set.Icc ( -Real.pi + k * 2 * Real.pi ) ( Real.pi + k * 2 * Real.pi ) ) MeasureTheory.volume› ( k + 1 ) using 1 ; push_cast ; ring;              exact MeasureTheory.IntegrableOn.mono_set ( MeasureTheory.IntegrableOn.union ‹_› ‹_› ) h_subset;            exact h_shift;          have h_integrable : MeasureTheory.IntegrableOn (fun t => f (x - t)) (Set.Icc (-Real.pi) Real.pi) MeasureTheory.volume := by            rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;            convert h_integrable.comp_sub_left x using 1;            ext; simp [Set.indicator];            grind;          exact h_integrable.mono_set <| Set.Ioc_subset_Icc_self;        exact h_integrable.mul_continuousOn ( by exact Continuous.continuousOn <| by exact Continuous.mul ( continuous_const ) <| by exact continuous_finset_sum _ fun _ _ => continuous_const.add <| by exact continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp <| by continuity );      · apply_rules [ Continuous.intervalIntegrable ];        apply_rules [ Continuous.mul, continuous_const, continuous_const ];        refine' continuous_finset_sum _ fun i hi => _;        exact continuous_const.add <| continuous_finset_sum _ fun j hj => Real.continuous_cos.comp <| by continuity;