Integrals of periodic functions #
In this file we prove that ∫ x in b..b + a, f x = ∫ x in c..c + a, f x for any (not necessarily
measurable) function periodic function with period a.
theorem
is_add_fundamental_domain_Ioc
{a : ℝ}
(ha : 0 < a)
(b : ℝ)
(μ : measure_theory.measure ℝ . "volume_tac") :
measure_theory.is_add_fundamental_domain ↥(add_subgroup.zmultiples a) (set.Ioc b (b + a)) μ
theorem
function.periodic.interval_integral_add_eq_of_pos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
{f : ℝ → E}
{a : ℝ}
(hf : function.periodic f a)
(ha : 0 < a)
(b c : ℝ) :
An auxiliary lemma for a more general function.periodic.interval_integral_add_eq.
theorem
function.periodic.interval_integral_add_eq
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
[measurable_space E]
[borel_space E]
[complete_space E]
[topological_space.second_countable_topology E]
{f : ℝ → E}
{a : ℝ}
(hf : function.periodic f a)
(b c : ℝ) :
If f is a periodic function with period a, then its integral over [b, b + a] does not
depend on b.