English
The Haar measure on AddCircle is the unique translation-invariant probability measure normalized so that the total mass is 1.
Русский
Мера Хаара на AddCircle — единственная мера с инвариантностью по сдвигам и нормировкой общей массы равной 1.
LaTeX
$$$$ \\text{volume} = \\text{HaarAddCircle} $$$$
Lean4
/-- Express Fourier coefficients of `f` on an interval in terms of those of its derivative. -/
theorem fourierCoeffOn_of_hasDeriv_right {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0)
(hf : ContinuousOn f [[a, b]]) (hff' : ∀ x, x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x)
(hf' : IntervalIntegrable f' volume a b) :
fourierCoeffOn hab f n =
1 / (-2 * π * I * n) * (fourier (-n) (a : AddCircle (b - a)) * (f b - f a) - (b - a) * fourierCoeffOn hab f' n) :=
by
rw [← ofReal_sub]
have hT : Fact (0 < b - a) := ⟨by linarith⟩
simp_rw [fourierCoeffOn_eq_integral, smul_eq_mul, real_smul, ofReal_div, ofReal_one]
conv => pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm])
rw [integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right hf
(fun x _ ↦ has_antideriv_at_fourier_neg hT hn x |>.continuousAt |>.continuousWithinAt) hff'
(fun x _ ↦ has_antideriv_at_fourier_neg hT hn x |>.hasDerivWithinAt) hf'
(((map_continuous (fourier (-n))).comp (AddCircle.continuous_mk' _)).intervalIntegrable _ _)]
have : ∀ u v w : ℂ, u * ((b - a : ℝ) / v * w) = (b - a : ℝ) / v * (u * w) := by intros; ring
conv in intervalIntegral _ _ _ _ => congr; ext; rw [this]
rw [(by ring : ((b - a : ℝ) : ℂ) / (-2 * π * I * n) = ((b - a : ℝ) : ℂ) * (1 / (-2 * π * I * n)))]
have s2 : (b : AddCircle (b - a)) = (a : AddCircle (b - a)) := by simpa using coe_add_period (b - a) a
rw [s2, intervalIntegral.integral_const_mul, ← sub_mul, mul_sub, mul_sub]
congr 1
· conv_lhs => rw [mul_comm, mul_div, mul_one]
rw [div_eq_iff (ofReal_ne_zero.mpr hT.out.ne')]
ring
· ring
