-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegrable {t : ℝ} (h₁f : Function.Periodic f T) (hT : 0 < T)
    (h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) (a₁ a₂ : ℝ) :
    IntervalIntegrable f MeasureTheory.volume a₁ a₂

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
⊢ t + ↑n₂ * T ≤ (t - ↑n₁ * T) ⊔ (t + ↑n₂ * T)

Tactic:
apply le_max_right

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
⊢ t + ↑n₂ * T = a (n₁ + n₂)

Tactic:
simp [a]

Result:
no goals

Proof state:
case h.e'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ t + (↑k + 1 - ↑n₁) * T = t + T + (↑k - ↑n₁) * T

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
⊢ IntervalIntegrable f volume (t - ↑n₁ * T) (t + ↑n₂ * T)

Tactic:
rw [(by ring : t - n₁ * T = a 0), (by simp [a] : t + n₂ * T = a (n₁ + n₂))]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
⊢ IntervalIntegrable f volume (a 0) (a (n₁ + n₂))

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
⊢ IntervalIntegrable f volume (a 0) (a (n₁ + n₂))

Tactic:
apply IntervalIntegrable.trans_iterate

Result:
case hint
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
⊢ ∀ k < n₁ + n₂, IntervalIntegrable f volume (a k) (a (k + 1))

Proof state:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)

Result:
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
⊢ IntervalIntegrable f volume a₁ a₂

Proof state:
case h.e'_3.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
x : ℝ
⊢ f x = f (x - (↑k - ↑n₁) * T)

Tactic:
simpa using (h₁f.sub_int_mul_eq (k - n₁)).symm

Result:
no goals

Proof state:
case h.e'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ f = fun x => f (x - (↑k - ↑n₁) * T)

Tactic:
funext x

Result:
case h.e'_3.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
x : ℝ
⊢ f x = f (x - (↑k - ↑n₁) * T)

Proof state:
case h.e'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ a (k + 1) = t + T + (↑k - ↑n₁) * T

Tactic:
simp [a, Nat.cast_add]

Result:
case h.e'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ t + (↑k + 1 - ↑n₁) * T = t + T + (↑k - ↑n₁) * T

Proof state:
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply IntervalIntegrable.mono_set _ this

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
⊢ IntervalIntegrable f volume (t - ↑n₁ * T) (t + ↑n₂ * T)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
⊢ t - ↑n₁ * T ≤ a₁ ⊓ a₂

Tactic:
linarith [(div_le_iff₀ hT).1 hn₁]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
⊢ IntervalIntegrable f volume (t - ↑n₁ * T) (t + ↑n₂ * T)

Tactic:
let a : ℕ → ℝ := fun n ↦ t + (n - n₁) * T

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
n₁ : ℕ
hn₁ : (t - a₁ ⊓ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (a₁ ⊔ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n => t + (↑n - ↑n₁) * T
⊢ IntervalIntegrable f volume (t - ↑n₁ * T) (t + ↑n₂ * T)