102 lines
3.4 KiB
Plaintext
102 lines
3.4 KiB
Plaintext
import Mathlib.MeasureTheory.Integral.Periodic
|
||
|
||
|
||
theorem periodic_integrability₁
|
||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||
{f : ℝ → E}
|
||
{t T : ℝ}
|
||
{n : ℕ}
|
||
(h₁f : Function.Periodic f T)
|
||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||
IntervalIntegrable f MeasureTheory.volume t (t + n * T) := by
|
||
induction' n with n hn
|
||
simp
|
||
apply IntervalIntegrable.trans (b := t + n * T)
|
||
exact hn
|
||
|
||
let A := IntervalIntegrable.comp_sub_right h₂f (n * T)
|
||
have : f = fun x ↦ f (x - n * T) := by simp [Function.Periodic.sub_nat_mul_eq h₁f n]
|
||
simp_rw [← this] at A
|
||
have : (t + T + ↑n * T) = (t + ↑(n + 1) * T) := by simp; ring
|
||
simp_rw [this] at A
|
||
exact A
|
||
|
||
theorem periodic_integrability₂
|
||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||
{f : ℝ → E}
|
||
{t T : ℝ}
|
||
{n : ℕ}
|
||
(h₁f : Function.Periodic f T)
|
||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||
IntervalIntegrable f MeasureTheory.volume (t - n * T) t := by
|
||
induction' n with n hn
|
||
simp
|
||
--
|
||
apply IntervalIntegrable.trans (b := t - n * T)
|
||
--
|
||
have A := IntervalIntegrable.comp_add_right h₂f (((n + 1): ℕ) * T)
|
||
|
||
have : f = fun x ↦ f (x + ((n + 1) : ℕ) * T) := by
|
||
funext x
|
||
have : x = x + ↑(n + 1) * T - ↑(n + 1) * T := by ring
|
||
nth_rw 1 [this]
|
||
rw [Function.Periodic.sub_nat_mul_eq h₁f]
|
||
simp_rw [← this] at A
|
||
have : (t + T - ↑(n + 1) * T) = (t - ↑n * T) := by simp; ring
|
||
simp_rw [this] at A
|
||
exact A
|
||
--
|
||
exact hn
|
||
|
||
|
||
theorem periodic_integrability₃
|
||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||
{f : ℝ → E}
|
||
{t T : ℝ}
|
||
{n₁ n₂ : ℕ}
|
||
(h₁f : Function.Periodic f T)
|
||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||
IntervalIntegrable f MeasureTheory.volume (t - n₁ * T) (t + n₂ * T) := by
|
||
apply IntervalIntegrable.trans (b := t)
|
||
exact periodic_integrability₂ h₁f h₂f
|
||
exact periodic_integrability₁ h₁f h₂f
|
||
|
||
|
||
theorem periodic_integrability4
|
||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||
{f : ℝ → E}
|
||
{t T : ℝ}
|
||
{a₁ a₂ : ℝ}
|
||
(h₁f : Function.Periodic f T)
|
||
(hT : 0 < T)
|
||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||
IntervalIntegrable f MeasureTheory.volume a₁ a₂ := by
|
||
|
||
obtain ⟨n₁, hn₁⟩ : ∃ n₁ : ℕ, t - n₁ * T ≤ min a₁ a₂ := by
|
||
obtain ⟨n₁, hn₁⟩ := exists_nat_ge ((t -min a₁ a₂) / T)
|
||
use n₁
|
||
rw [sub_le_iff_le_add]
|
||
rw [div_le_iff₀ hT] at hn₁
|
||
rw [sub_le_iff_le_add] at hn₁
|
||
rw [add_comm]
|
||
exact hn₁
|
||
obtain ⟨n₂, hn₂⟩ : ∃ n₂ : ℕ, max a₁ a₂ ≤ t + n₂ * T := by
|
||
obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)
|
||
use n₂
|
||
rw [← sub_le_iff_le_add]
|
||
rw [div_le_iff₀ hT] at hn₂
|
||
linarith
|
||
|
||
have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by
|
||
apply Set.uIcc_subset_uIcc_iff_le.mpr
|
||
constructor
|
||
· calc min (t - ↑n₁ * T) (t + ↑n₂ * T)
|
||
_ ≤ (t - ↑n₁ * T) := by exact min_le_left (t - ↑n₁ * T) (t + ↑n₂ * T)
|
||
_ ≤ min a₁ a₂ := by exact hn₁
|
||
· calc max a₁ a₂
|
||
_ ≤ t + n₂ * T := by exact hn₂
|
||
_ ≤ max (t - ↑n₁ * T) (t + ↑n₂ * T) := by exact le_max_right (t - ↑n₁ * T) (t + ↑n₂ * T)
|
||
|
||
apply IntervalIntegrable.mono_set _ this
|
||
exact periodic_integrability₃ h₁f h₂f
|