awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)
have h₀ : Int.negSucc n • T + (n + 1) • T = 0
Tactic: have h₀ : Int.negSucc n • T + (n + 1) • T = 0 := by simp; linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
⊢ ∫ (x : ℝ) in 0..Int.negSucc n • T, f x = -HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x)
have negSucc : ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
Tactic: rw [integral_symm, ← (hf.nsmul (n + 1)).funext, neg_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
have negSucc₂ : ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
Tactic: simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
negSucc₂ :
  ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
have negSucc₃ : ∫ (x : ℝ) in 0..0 + (n + 1) • T, f x = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
Tactic: simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
negSucc₂ :
  ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₃ :
  ∫ (x : ℝ) in 0..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
have negSucc₄ : ∫ (x : ℝ) in 0..(n + 1) • T, f x = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
Tactic: simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
negSucc₂ :
  ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₃ :
  ∫ (x : ℝ) in 0..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₄ :
  ∫ (x : ℝ) in 0..(n + 1) • T, f x = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
have negSucc₅ : HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
Tactic: simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
negSucc₂ :
  ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₃ :
  ∫ (x : ℝ) in 0..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₄ :
  ∫ (x : ℝ) in 0..(n + 1) • T, f x = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
negSucc₅ :
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
have negSucc₆ : HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..(n + 1) • T + T, f x)
Tactic: simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst_1 : NormedSpace ℝ E
hf : Periodic f T
t : ℝ
h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f volume t₁ t₂
this : ∀ (m : ℕ), ∫ (x : ℝ) in 0..m • T, f x = HSMul.hSMul (β := E) m (∫ (x : ℝ) in 0..T, f x)
n : ℕ
h₀ : Int.negSucc n • T + (n + 1) • T = 0
negSucc negSucc₁ :
  ∫ (x : ℝ) in Int.negSucc n • T..0, f (x + (n + 1) • T) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f (x + (n + 1) • T))
negSucc₂ :
  ∫ (x : ℝ) in Int.negSucc n • T + (n + 1) • T..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₃ :
  ∫ (x : ℝ) in 0..0 + (n + 1) • T, f x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0 + (n + 1) • T..T + (n + 1) • T, f x)
negSucc₄ :
  ∫ (x : ℝ) in 0..(n + 1) • T, f x = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
negSucc₅ :
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..T + (n + 1) • T, f x)
negSucc₆ :
  HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in (n + 1) • T..(n + 1) • T + T, f x)
⊢ ∫ (x : ℝ) in Int.negSucc n • T..0, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x =
    HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, (fun (x : ℝ) ↦ f (x + (n + 1) • T)) x)
have negSucc₇ : HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..T, f x) = HSMul.hSMul (β := E) (n + 1) (∫ (x : ℝ) in 0..0 + T, f x)
Tactic: simp_rw [integral_comp_add_right, h₀, zero_add, this (n + 1), add_comm T,
      hf.intervalIntegral_add_eq ((n + 1) • T) 0, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
| ∫ (x : ℝ) in 0..t, g x
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • 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 _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 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
have 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)
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 _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 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)
have rw : LE.le (α := ℝ) (sInf ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T)) (∫ (x : ℝ) in 0..ε, 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
| ∫ (x : ℝ) in 0..t, g x
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • 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 _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ ∫ (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)
have 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)
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 _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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
⊢ 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)
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in 0..ε, g x) (sSup ((fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T))
Tactic: rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε h'_int, hg.intervalIntegral_add_eq ε 0, zero_add,
    add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atTop atTop
have h_int : IntervalIntegrable g volume 0 T
Tactic: have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atTop atTop
have 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
Tactic: apply tendsto_atTop_mono (hg.sInf_add_zsmul_le_integral_of_pos h_int hT)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 (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
have apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / T⌋ (∫ (x : ℝ) in 0..T, g x)) atTop atTop
have apply : Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atTop atTop
Tactic: apply Tendsto.atTop_zsmul_const h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..T, g x)
hT : 0 < T
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atBot atBot
have h_int : IntervalIntegrable g volume 0 T
Tactic: have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 (t : ℝ) ↦ ∫ (x : ℝ) in 0..t, g x) atBot atBot
have 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
Tactic: apply tendsto_atBot_mono (hg.integral_le_sSup_add_zsmul_of_pos h_int hT)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 (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
have apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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 : ℝ) ↦ HSMul.hSMul (β := ℝ) ⌊x / T⌋ (∫ (x : ℝ) in 0..T, g x)) atBot atBot
have apply : Tendsto (β := ℤ) (fun (x : ℝ) ↦ ⌊x / T⌋) atBot atBot
Tactic: apply Tendsto.atBot_zsmul_const h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : IntervalIntegrable f volume a (b + c)
hab : a ≤ b
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ slope f x (x + c)) volume a b
have simp : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ c⁻¹ * (f (x + c) - f x)) volume a b
Tactic: simp only [slope, add_sub_cancel_left, vsub_eq_sub, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc : 0 ≤ c
⊢ a ≤ b + c
have linarith : b + c < a → a - b + (0 - c) + (b + c - a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc : 0 ≤ c
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
have inl : ∀ (hc : 0 = c), ∫ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
have inr : ∀ (hc : 0 < c), ∫ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
have inl : f a ≤ f b
Tactic: simp only [← hc, add_zero, slope_same, intervalIntegral.integral_zero, sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 = c
⊢ f a ≤ f b
have inl : a ∈ Icc a (b + c)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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)
⊢ f a ≤ f b
have inl₁ : b ∈ Icc a (b + c)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
⊢ a ≤ b + c
have linarith : b + c < a → a - b + (0 - c) + (b + c - a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
have hf₁ : MonotoneOn f (uIcc a (b + c))
Tactic: rw [← uIcc_of_le (by linarith)] at hf
Cleared hypotheses: hf, hab, hc_1, hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
have hf' : IntervalIntegrable f volume a (b + c)
Tactic: have hf' := hf.intervalIntegrable (μ := volume)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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 : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
have inr : c⁻¹ * ∫ (x : ℝ) in a..b, f (x + c) - f x ≤ f (b + c) - f a
Tactic: simp only [slope, add_sub_cancel_left, vsub_eq_sub, smul_eq_mul,
    intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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)
⊢ c⁻¹ * ∫ (x : ℝ) in a..b, f (x + c) - f x ≤ f (b + c) - f a
have inr : c⁻¹ * HSub.hSub (α := ℝ) (∫ (x : ℝ) in b..b + c, f x) (∫ (x : ℝ) in a..a + 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]))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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)
⊢ b ≤ b + c
have linarith : b + c < b → 0 - c + (b + c - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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)
⊢ f x ≤ (fun (x : ℝ) ↦ f (b + c)) x
have x : x ∈ uIcc a (b + c)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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)
⊢ f x_1 ≤ (fun (x : ℝ) ↦ f (b + c)) x_1
have x₁ : b + c ∈ uIcc a (b + c)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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)
⊢ f x_1 ≤ (fun (x : ℝ) ↦ f (b + c)) x_1
have a₁ : x_1 ≤ b + c
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
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 : ℝ) in b..b + c, f x ≤ c * f (b + c)
have grw : ∫ (u : ℝ) in b..b + c, f (b + c) ≤ c * f (b + c)
Tactic: grw [intervalIntegral.integral_mono_on (g := fun _ ↦ f (b + c))
          (by linarith)
          (hf'.mono_set (by grind [uIcc]))
          (by simp)
          (by intros; apply hf <;> grind [uIcc])]