Source indexedtheorem · leanprover/lean4:v4.32.0

fourier_partial_sum_eq_integral

PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:312 to 332

Mathematical statement

Exact Lean statement

theorem fourier_partial_sum_eq_integral {f : ℝ → ℝ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)
    (h_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :
    fourier_partial_sum f n x = (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, f t * dirichlet_kernel n (x - t)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fourier_partial_sum_eq_integral {f : ℝ → ℝ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (h_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :    fourier_partial_sum f n x = (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, f t * dirichlet_kernel n (x - t) := by      unfold fourier_partial_sum dirichlet_kernel;      simp +decide [ mul_add, mul_comm, mul_left_comm, div_eq_inv_mul, Finset.mul_sum _ _ _, Finset.sum_add_distrib, intervalIntegral.integral_const_mul, fourier_coeff_cos, fourier_coeff_sin ];      rw [ intervalIntegral.integral_add, intervalIntegral.integral_finset_sum ] <;> norm_num;      · norm_num [ sub_mul, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, Finset.sum_add_distrib ];        norm_num [ Real.cos_sub, Real.sin_sub, mul_sub, ← mul_assoc, ← Finset.mul_sum _ _ _, ← Finset.sum_add_distrib ] ; ring_nf;        rw [ Finset.mul_sum _ _ _ ] ; refine' congr rfl ( Finset.sum_congr rfl fun i hi => _ ) ; rw [ intervalIntegral.integral_add ] <;> norm_num [ mul_assoc, mul_comm, mul_left_comm, ← intervalIntegral.integral_const_mul ] ; ring_nf;        · simp +decide only [mul_assoc, mul_comm, ← intervalIntegral.integral_const_mul,                        mul_left_comm];        · exact hf.mul_continuousOn ( Continuous.continuousOn ( by continuity ) );        · apply_rules [ IntervalIntegrable.mul_continuousOn, hf ];          fun_prop;      · intro i hi₁ hi₂; exact hf.mul_continuousOn ( Continuous.continuousOn ( Real.continuous_cos.comp ( by continuity ) ) ) ;      · exact hf.mul_const _;      · rw [ intervalIntegrable_iff_integrableOn_Ioc_of_le ( by linarith [ Real.pi_pos ] ) ] at *;        refine' MeasureTheory.integrable_finset_sum _ fun i hi => _;        refine' hf.norm.mono' _ _;        · exact hf.1.mul ( Continuous.aestronglyMeasurable ( Real.continuous_cos.comp ( by continuity ) ) );        · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Ioc ] with a ha using by rw [ norm_mul ] ; exact mul_le_of_le_one_right ( norm_nonneg _ ) ( Real.abs_cos_le_one _ ) ;