-- 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:
case left
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) ≤ a₁ ⊓ a₂

Tactic:
calc min (t - n₁ * T) (t + n₂ * T)
_ ≤ (t - n₁ * T) := by apply min_le_left
_ ≤ min a₁ a₂ := by 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₂
⊢ a₁ ⊔ a₂ ≤ t + ↑n₂ * T

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

Result:
no goals

Proof state:
case right
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₂
⊢ a₁ ⊔ a₂ ≤ (t - ↑n₁ * T) ⊔ (t + ↑n₂ * T)

Tactic:
calc max a₁ a₂
_ ≤ t + n₂ * T := by linarith [(div_le_iff₀ hT).1 hn₂]
_ ≤ max (t - n₁ * T) (t + n₂ * T) := by 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₂
⊢ uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)

Tactic:
rw [Set.uIcc_subset_uIcc_iff_le]

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₂
⊢ (t - ↑n₁ * T) ⊓ (t + ↑n₂ * T) ≤ a₁ ⊓ a₂ ∧ a₁ ⊔ a₂ ≤ (t - ↑n₁ * T) ⊔ (t + ↑n₂ * T)

Proof state:
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))

Tactic:
intro k hk

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 : ℕ
hk : k < n₁ + n₂
⊢ IntervalIntegrable f volume (a k) (a (k + 1))

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₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂

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

Result:
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₂

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) ≤ a₁ ⊓ a₂ ∧ a₁ ⊔ a₂ ≤ (t - ↑n₁ * T) ⊔ (t + ↑n₂ * T)

Tactic:
constructor

Result:
case left
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) ≤ a₁ ⊓ a₂

case right
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₂
⊢ a₁ ⊔ a₂ ≤ (t - ↑n₁ * T) ⊔ (t + ↑n₂ * T)

Proof state:
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 : ℕ
hk : k < n₁ + n₂
⊢ IntervalIntegrable f volume (a k) (a (k + 1))

Tactic:
convert (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T)) using 1

Result:
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)

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

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 min_le_left

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 0

Tactic:
ring

Result:
no goals