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

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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) ≤ ∫ (x : ℝ) in 0 ..ε, g x

Tactic:
exact (continuous_primitive h'_int 0).continuousOn.sInf_image_Icc_le <|
  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 : ℝ
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (x : ℝ) in 0 ..t, g x

Tactic:
conv_rhs =>
  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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤
    (∫ (x : ℝ) in 0 ..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • 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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤
    (∫ (x : ℝ) in 0 ..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x

Tactic:
rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε (hg.intervalIntegrable₀ hT 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
⊢ sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) ≤ ∫ (x : ℝ) in 0 ..ε, g x