-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem integral_le_sSup_add_zsmul_of_pos (h_int : IntervalIntegrable g MeasureSpace.volume 0 T)
    (hT : 0 < T) (t : ℝ) :
    (∫ x in (0)..t, g x) ≤
      sSup ((fun t => ∫ x in (0)..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ x in (0)..T, g x

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
⊢ ∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Tactic:
let ε := Int.fract (t / T) * T

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0 ..ε, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T)

Tactic:
exact (continuous_primitive h'_int 0).continuousOn.le_sSup_image_Icc
  (mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT))

Result:
no goals

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ (∫ (x : ℝ) in 0 ..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x ≤
    sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Tactic:
rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε h'_int, hg.intervalIntegral_add_eq ε 0, zero_add,
  add_le_add_iff_right]

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0 ..ε, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T)

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
⊢ ∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Tactic:
let h'_int := hg.intervalIntegrable₀ hT h_int

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
⊢ ∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Tactic:
conv_lhs =>
  rw [← Int.fract_div_mul_self_add_zsmul_eq T t (by linarith), ←
    integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ (∫ (x : ℝ) in 0 ..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x ≤
    sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg hT h_int
ε : ℝ := Int.fract (t / T) * T
⊢ T ≠ 0

Tactic:
linarith

Result:
no goals