awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x)
| ∫ (x : ℝ) in 0..t, g x

Tactic:
rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne',
      ← integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]

Premises used: intervalIntegral.integral_add_adjacent_intervals, Int.fract_div_mul_self_add_zsmul_eq, LT.lt.ne', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
conv_rhs :
  sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊t / T⌋ (∫ (x : ℝ) in 0..T, g x) ≤
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x)
⊢ sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊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 hT.ne',
      ← integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]

Premises used: intervalIntegral.integral_add_adjacent_intervals, Int.fract_div_mul_self_add_zsmul_eq, LT.lt.ne', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
rw : LE.le (α := ℝ) (sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T)) (∫ (x : ℝ) in 0..ε, g x)
⊢ sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊t / T⌋ (∫ (x : ℝ) in 0..T, g x) ≤
    HAdd.hAdd (α := ℝ) (∫ (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.ne' h_int),
    hg.intervalIntegral_add_eq ε 0, zero_add, add_le_add_iff_right]

Premises used: Int.floor, Function.Periodic.intervalIntegrable₀, HDiv.hDiv, zero_add, LT.lt.ne', add_le_add_iff_right, OfNat.ofNat, Function.Periodic.intervalIntegral_add_zsmul_eq, Function.Periodic.intervalIntegral_add_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
⊢ LE.le (α := ℝ) (sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T)) (∫ (x : ℝ) in 0..ε, g x)

Tactic:
(continuous_primitive h'_int 0).continuousOn.sInf_image_Icc_le <|
    mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT)

Premises used: Int.fract_div_mul_self_mem_Ico, Continuous.continuousOn, ContinuousOn.sInf_image_Icc_le, Set.mem_Icc_of_Ico, OfNat.ofNat, intervalIntegral.continuous_primitive
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
⊢ LE.le (α := ℝ) (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)

Premises used: Int.fract_div_mul_self_mem_Ico, Continuous.continuousOn, ContinuousOn.sInf_image_Icc_le, Set.mem_Icc_of_Ico, OfNat.ofNat, intervalIntegral.continuous_primitive
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x)
| ∫ (x : ℝ) in 0..t, g x

Tactic:
rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne', ←
      integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]

Premises used: intervalIntegral.integral_add_adjacent_intervals, Int.fract_div_mul_self_add_zsmul_eq, LT.lt.ne', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
conv_lhs :
  HAdd.hAdd (α := ℝ) (∫ (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) + HSMul.hSMul (β := ℝ) ⌊t / T⌋ (∫ (x : ℝ) in 0..T, g x)
⊢ ∫ (x : ℝ) in 0..t, g x ≤
    sSup ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊t / T⌋ (∫ (x : ℝ) in 0..T, g x)

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

Premises used: intervalIntegral.integral_add_adjacent_intervals, Int.fract_div_mul_self_add_zsmul_eq, LT.lt.ne', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
rw : LE.le (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (sSup ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T))
⊢ HAdd.hAdd (α := ℝ) (∫ (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) + HSMul.hSMul (β := ℝ) ⌊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]

Premises used: Int.floor, HDiv.hDiv, zero_add, add_le_add_iff_right, OfNat.ofNat, Function.Periodic.intervalIntegral_add_zsmul_eq, Function.Periodic.intervalIntegral_add_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (sSup ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T))

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

Premises used: ContinuousOn.le_sSup_image_Icc, Int.fract_div_mul_self_mem_Ico, Continuous.continuousOn, Set.mem_Icc_of_Ico, OfNat.ofNat, intervalIntegral.continuous_primitive
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
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₂ := ⋯
ε : ℝ := Int.fract (t / T) * T
⊢ LE.le (α := ℝ) (∫ (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))

Premises used: ContinuousOn.le_sSup_image_Icc, Int.fract_div_mul_self_mem_Ico, Continuous.continuousOn, Set.mem_Icc_of_Ico, OfNat.ofNat, intervalIntegral.continuous_primitive
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
⊢ IntervalIntegrable g volume 0 T

Tactic:
have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
apply :
  Tendsto (β := ℝ)
    (fun (n : ℝ) ↦
      sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊n / T⌋ (∫ (x : ℝ) in 0..T, g x))
    atTop atTop
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atTop atTop

Tactic:
apply tendsto_atTop_mono (hg.sInf_add_zsmul_le_integral_of_pos h_int hT)

Premises used: Function.Periodic.sInf_add_zsmul_le_integral_of_pos, Filter.tendsto_atTop_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / T⌋ (∫ (x : ℝ) in 0..T, g x)) atTop atTop
⊢ Tendsto (β := ℝ)
    (fun (n : ℝ) ↦
      sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊n / T⌋ (∫ (x : ℝ) in 0..T, g x))
    atTop atTop

Tactic:
apply atTop.tendsto_atTop_add_const_left (sInf <| (fun t => ∫ x in 0..t, g x) '' Icc 0 T)

Premises used: Filter.tendsto_atTop_add_const_left, intervalIntegral, Filter.atTop, Set.Icc, MeasureTheory.MeasureSpace.volume, Set.image, OfNat.ofNat, InfSet.sInf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
apply : Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / T⌋ (∫ (x : ℝ) in 0..T, g x)) atTop atTop

Tactic:
apply Tendsto.atTop_zsmul_const h₀

Premises used: Filter.Tendsto.atTop_zsmul_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atTop atTop

Tactic:
tendsto_floor_atTop.comp (tendsto_id.atTop_mul_const (inv_pos.mpr hT))

Premises used: Iff.mpr, Filter.Tendsto.atTop_mul_const, Filter.tendsto_id, tendsto_floor_atTop, inv_pos, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atTop atTop

Tactic:
exact tendsto_floor_atTop.comp (tendsto_id.atTop_mul_const (inv_pos.mpr hT))

Premises used: Iff.mpr, Filter.Tendsto.atTop_mul_const, Filter.tendsto_id, tendsto_floor_atTop, inv_pos, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
apply :
  Tendsto (β := ℝ)
    (fun (n : ℝ) ↦
      sSup ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊n / T⌋ (∫ (x : ℝ) in 0..T, g x))
    atBot atBot
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atBot atBot

Tactic:
apply tendsto_atBot_mono (hg.integral_le_sSup_add_zsmul_of_pos h_int hT)

Premises used: Filter.tendsto_atBot_mono, Function.Periodic.integral_le_sSup_add_zsmul_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / T⌋ (∫ (x : ℝ) in 0..T, g x)) atBot atBot
⊢ Tendsto (β := ℝ)
    (fun (n : ℝ) ↦
      sSup ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + HSMul.hSMul (β := ℝ) ⌊n / T⌋ (∫ (x : ℝ) in 0..T, g x))
    atBot atBot

Tactic:
apply atBot.tendsto_atBot_add_const_left (sSup <| (fun t => ∫ x in 0..t, g x) '' Icc 0 T)

Premises used: intervalIntegral, Filter.tendsto_atBot_add_const_left, Set.Icc, MeasureTheory.MeasureSpace.volume, Filter.atBot, Set.image, OfNat.ofNat, SupSet.sSup
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
apply : Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atBot atBot
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / T⌋ (∫ (x : ℝ) in 0..T, g x)) atBot atBot

Tactic:
apply Tendsto.atBot_zsmul_const h₀

Premises used: Filter.Tendsto.atBot_zsmul_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atBot atBot

Tactic:
tendsto_floor_atBot.comp (tendsto_id.atBot_mul_const (inv_pos.mpr hT))

Premises used: Iff.mpr, Filter.tendsto_id, inv_pos, tendsto_floor_atBot, Filter.Tendsto.comp, Filter.Tendsto.atBot_mul_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atBot atBot

Tactic:
exact tendsto_floor_atBot.comp (tendsto_id.atBot_mul_const (inv_pos.mpr hT))

Premises used: Iff.mpr, Filter.tendsto_id, inv_pos, tendsto_floor_atBot, Filter.Tendsto.comp, Filter.Tendsto.atBot_mul_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
h₀ : ∀ (x : ℝ), 0 < g x
hT : 0 < T
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atTop atTop

Tactic:
hg.tendsto_atTop_intervalIntegral_of_pos (intervalIntegral_pos_of_pos h_int h₀ hT) hT

Premises used: intervalIntegral.intervalIntegral_pos_of_pos, Function.Periodic.tendsto_atTop_intervalIntegral_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
h₀ : ∀ (x : ℝ), 0 < g x
hT : 0 < T
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atBot atBot

Tactic:
hg.tendsto_atBot_intervalIntegral_of_pos (intervalIntegral_pos_of_pos h_int h₀ hT) hT

Premises used: intervalIntegral.intervalIntegral_pos_of_pos, Function.Periodic.tendsto_atBot_intervalIntegral_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
h₀ : ∀ (x : ℝ), 0 < g x
hT : 0 < T
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atBot atBot

Tactic:
exact hg.tendsto_atBot_intervalIntegral_of_pos (intervalIntegral_pos_of_pos h_int h₀ hT) hT

Premises used: intervalIntegral.intervalIntegral_pos_of_pos, Function.Periodic.tendsto_atBot_intervalIntegral_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : IntervalIntegrable f volume a (b + c)
hab : a ≤ b
hc : 0 ≤ c
simp : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ c⁻¹ * (f (x + c) - f x)) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ slope f x (x + c)) volume a b

Tactic:
simp only [slope, add_sub_cancel_left, vsub_eq_sub, smul_eq_mul]

Premises used: add_sub_cancel_left, slope, smul_eq_mul, vsub_eq_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : IntervalIntegrable f volume a (b + c)
hab : a ≤ b
hc : 0 ≤ c
⊢ uIcc a b ⊆ uIcc (a - c) (b + c - c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : IntervalIntegrable f volume a (b + c)
hab : a ≤ b
hc : 0 ≤ c
⊢ uIcc a b ⊆ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : IntervalIntegrable f volume a (b + c)
hab : a ≤ b
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ c⁻¹ * (f (x + c) - f x)) volume a b

Tactic:
exact hf.comp_add_right c |>.mono_set (by grind [uIcc]) |>.sub (hf.mono_set (by grind [uIcc]))
    |>.const_mul (c := c⁻¹)

Premises used: IntervalIntegrable.mono_set, IntervalIntegrable.comp_add_right, IntervalIntegrable.sub, Inv.inv, IntervalIntegrable.const_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc : 0 ≤ c
linarith : b + c < a → a - b + (0 - c) + (b + c - a) = 0
⊢ a ≤ b + c

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc : 0 ≤ c
inl : ∀ (hc : 0 = c), ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
inr : ∀ (hc : 0 < c), ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a

Tactic:
rcases eq_or_lt_of_le hc with hc | hc

Premises used: eq_or_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
inl : f a ≤ f b
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a

Tactic:
simp only [← hc, add_zero, slope_same, intervalIntegral.integral_zero, sub_nonneg]

Premises used: intervalIntegral.integral_zero, add_zero, sub_nonneg, slope_same
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
inl : a ∈ Icc a (b + c)
inl₁ : b ∈ Icc a (b + c)
inl₂ : a ≤ b
⊢ f a ≤ f b

Tactic:
apply hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
⊢ a ∈ Icc a (b + c)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
⊢ b ∈ Icc a (b + c)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
⊢ a ≤ b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
linarith : b + c < a → a - b + (0 - c) + (b + c - a) = 0
⊢ a ≤ b + c

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
⊢ MonotoneOn f (uIcc a (b + c))

Tactic:
rw [← uIcc_of_le (by linarith)] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf₁ : MonotoneOn f (uIcc a (b + c))
⊢ a ≤ b

Tactic:
rw [← uIcc_of_le (by linarith)] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf₁ : MonotoneOn f (uIcc a (b + c))
hab₁ : a ≤ b
⊢ 0 ≤ c

Tactic:
rw [← uIcc_of_le (by linarith)] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf₁ : MonotoneOn f (uIcc a (b + c))
hab₁ : a ≤ b
hc₁ : 0 ≤ c
⊢ 0 < c

Tactic:
rw [← uIcc_of_le (by linarith)] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
⊢ IntervalIntegrable f volume a (b + c)

Tactic:
have hf' := hf.intervalIntegrable (μ := volume)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
inr : c⁻¹ * ∫ (x : ℝ) in a..b, f (x + c) - f x ≤ f (b + c) - f a
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a

Tactic:
simp only [slope, add_sub_cancel_left, vsub_eq_sub, smul_eq_mul,
    intervalIntegral.integral_const_mul]

Premises used: add_sub_cancel_left, slope, smul_eq_mul, vsub_eq_sub, intervalIntegral.integral_const_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ uIcc a b ⊆ uIcc (a - c) (b + c - c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ uIcc a b ⊆ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ uIcc (a + c) (b + c) ⊆ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ uIcc (a + c) a ⊆ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
inr : c⁻¹ * HSub.hSub (α := ℝ) (∫ (x : ℝ) in b..b + c, f x) (∫ (x : ℝ) in a..a + c, f x) ≤ f (b + c) - f a
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (x + c) - f x ≤ f (b + c) - f a

Tactic:
rw [intervalIntegral.integral_sub
        (hf'.comp_add_right c |>.mono_set (by grind [uIcc]))
        (hf'.mono_set (by grind [uIcc])),
      intervalIntegral.integral_comp_add_right,
      intervalIntegral.integral_interval_sub_interval_comm'
        (hf'.mono_set (by grind [uIcc]))
        (hf'.mono_set (by grind [uIcc]))
        (hf'.mono_set (by grind [uIcc]))]

Premises used: IntervalIntegrable.mono_set, IntervalIntegrable.comp_add_right, intervalIntegral.integral_interval_sub_interval_comm', intervalIntegral.integral_sub, intervalIntegral.integral_comp_add_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
linarith : b + c < b → 0 - c + (b + c - b) = 0
⊢ b ≤ b + c

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ uIcc b (b + c) ⊆ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f (b + c)) volume b (b + c)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
x_1 : ℝ
h : x_1 ∈ Icc b (b + c)
x : x_1 ∈ uIcc a (b + c)
x₁ : b + c ∈ uIcc a (b + c)
a₁ : x_1 ≤ b + c
⊢ f x_1 ≤ (fun (x : ℝ) ↦ f (b + c)) x_1

Tactic:
apply hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
x : ℝ
h : x ∈ Icc b (b + c)
⊢ x ∈ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
x : ℝ
h : x ∈ Icc b (b + c)
⊢ b + c ∈ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc