awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
⊢ (Summable (α := ℝ≥0) fun (k : ℕ) ↦
      HSub.hSub (α := ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ≥0) *
        f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable f

Tactic:
summable_schlomilch_iff hf (pow_pos zero_lt_two) (pow_right_strictMono₀ _root_.one_lt_two)
      two_ne_zero h_succ_diff

Premises used: pow_pos, two_ne_zero, one_lt_two, NNReal.summable_schlomilch_iff, zero_lt_two, pow_right_strictMono₀
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
h :
  ∀ (x : ℕ),
    HPow.hPow (α := ℝ≥0) 2 x =
      HSub.hSub (α := ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 (x + 1)) : ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 x) : ℝ≥0)
⊢ (Summable (α := ℝ≥0) fun (k : ℕ) ↦ HPow.hPow (α := ℝ≥0) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f

Tactic:
convert!
    summable_schlomilch_iff hf (pow_pos zero_lt_two) (pow_right_strictMono₀ _root_.one_lt_two)
      two_ne_zero h_succ_diff

Premises used: pow_pos, two_ne_zero, one_lt_two, NNReal.summable_schlomilch_iff, zero_lt_two, pow_right_strictMono₀
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
x : ℕ
⊢ HPow.hPow (α := ℝ≥0) 2 x =
    HSub.hSub (α := ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 (x + 1)) : ℝ≥0) (↑(HPow.hPow (α := ℕ) 2 x) : ℝ≥0)

Tactic:
simp [pow_succ, mul_two]

Premises used: pow_succ, mul_two
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ ∀ (i : ℕ), 0 ≤ f i

Tactic:
h_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
lift :
  ∀ (f : (i : ℕ) → ℝ≥0)
    (hf :
      ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → LE.le (α := ℝ) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) n) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) m)),
    (Summable (α := ℝ) fun (k : ℕ) ↦
        HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * (fun (i : ℕ) ↦ (↑(f i) : ℝ)) (u k)) ↔
      Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * f (u k)) ↔ Summable f

Tactic:
lift f to ℕ → ℝ≥0 using h_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → LE.le (α := ℝ) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) n) ((fun (i : ℕ) ↦ (↑(f i) : ℝ)) m)
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m

Tactic:
simp only [NNReal.coe_le_coe] at *

Premises used: NNReal.coe_le_coe
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
⊢ LE.le (α := ℝ≥0) (↑(u k) : ℝ≥0) (↑(u k.succ) : ℝ≥0)

Tactic:
have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
this : LE.le (α := ℝ≥0) (↑(u k) : ℝ≥0) (↑(u k.succ) : ℝ≥0)
⊢ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) = (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)

Tactic:
simp [NNReal.coe_sub this]

Premises used: NNReal.coe_sub
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ ∀ (k : ℕ),
    HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) =
      (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)

Tactic:
have (k : ℕ) : (u (k + 1) - (u k : ℝ)) = ((u (k + 1) : ℝ≥0) - (u k : ℝ≥0) : ℝ≥0) := by
    have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
    simp [NNReal.coe_sub this]
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
this :
  ∀ (k : ℕ),
    HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) =
      (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)
simp_rw :
  (Summable (α := ℝ) fun (k : ℕ) ↦
      (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ) * (↑(f (u k)) : ℝ)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) * (↑(f (u k)) : ℝ)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)

Tactic:
simp_rw [this]
-- Module: Mathlib.Analysis.PSeries
Goal:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : (i : ℕ) → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
this :
  ∀ (k : ℕ),
    HSub.hSub (α := ℝ) (↑(u (k + 1)) : ℝ) (↑(u k) : ℝ) =
      (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦
      (↑(HSub.hSub (α := ℝ≥0) (↑(u (k + 1)) : ℝ≥0) (↑(u k) : ℝ≥0)) : ℝ) * (↑(f (u k)) : ℝ)) ↔
    Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)

Tactic:
exact_mod_cast NNReal.summable_schlomilch_iff hf h_pos hu_strict hC_nonzero h_succ_diff

Premises used: NNReal.summable_schlomilch_iff
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ HSub.hSub (α := ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (n + 2)) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (n + 1)) ≤
    HSMul.hSMul (α := ℕ) 2
      (HSub.hSub (α := ℕ) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) (n + 1)) ((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x) n))

Tactic:
simp [pow_succ, mul_two, two_mul]

Premises used: pow_succ, two_mul, mul_two
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x

Tactic:
have h_succ_diff : SuccDiffBounded 2 (2 ^ ·) := by
    intro n
    simp [pow_succ, mul_two, two_mul]
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦
      HSub.hSub (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 (k + 1)) : ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) *
        f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable f

Tactic:
summable_schlomilch_iff_of_nonneg h_nonneg h_mono (pow_pos zero_lt_two)
      (pow_right_strictMono₀ one_lt_two) two_ne_zero h_succ_diff

Premises used: pow_pos, summable_schlomilch_iff_of_nonneg, two_ne_zero, one_lt_two, zero_lt_two, pow_right_strictMono₀
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
h :
  ∀ (x : ℕ),
    HPow.hPow (α := ℝ) 2 x = HSub.hSub (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 (x + 1)) : ℝ) (↑(HPow.hPow (α := ℕ) 2 x) : ℝ)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f

Tactic:
convert!
    summable_schlomilch_iff_of_nonneg h_nonneg h_mono (pow_pos zero_lt_two)
      (pow_right_strictMono₀ one_lt_two) two_ne_zero h_succ_diff

Premises used: pow_pos, summable_schlomilch_iff_of_nonneg, two_ne_zero, one_lt_two, zero_lt_two, pow_right_strictMono₀
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x
x : ℕ
⊢ HPow.hPow (α := ℝ) 2 x = HSub.hSub (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 (x + 1)) : ℝ) (↑(HPow.hPow (α := ℕ) 2 x) : ℝ)

Tactic:
simp [pow_succ, mul_two]

Premises used: pow_succ, mul_two
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : 0 ≤ᶠ[Filter.atTop] f
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b

Tactic:
rw [Filter.EventuallyLE, Filter.eventually_atTop] at h_nonneg

Premises used: Filter.EventuallyLE, Filter.eventually_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : 0 ≤ᶠ[Filter.atTop] f
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
h_nonneg₁ : ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b
⊢ ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k

Tactic:
rw [Filter.EventuallyLE, Filter.eventually_atTop] at h_nonneg

Premises used: Filter.EventuallyLE, Filter.eventually_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b
h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k
⊢ ∃ (a : ℕ), ∀ b ≥ a, f (b + 1) ≤ f b

Tactic:
rw [Filter.eventually_atTop] at h_mono

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_nonneg : ∃ (a : ℕ), ∀ b ≥ a, 0 b ≤ f b
h_mono : ∃ (a : ℕ), ∀ b ≥ a, f (b + 1) ≤ f b
rcases :
  ∀ (n : ℕ) (hn : ∀ b ≥ n, 0 b ≤ f b),
    (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f

Tactic:
rcases h_nonneg with ⟨n, hn⟩
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
h_mono : ∃ (a : ℕ), ∀ b ≥ a, f (b + 1) ≤ f b
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
rcases :
  ∀ (m : ℕ) (hm : ∀ b ≥ m, f (b + 1) ≤ f b),
    (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f

Tactic:
rcases h_mono with ⟨m, hm⟩
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))

Tactic:
summable_condensed_iff_of_nonneg (f := fun k ↦ f (max k (n + m))) _ _

Premises used: summable_condensed_iff_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
h₁ : Summable f ↔ Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))
convert_1 : ∀ (n_1 : ℕ), LE.le (α := ℝ) 0 ((fun (k : ℕ) ↦ f (max k (n + m))) n_1)
convert_2 :
  ∀ ⦃m_1 n_1 : ℕ⦄,
    0 < m_1 → m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔ Summable f

Tactic:
convert! summable_condensed_iff_of_nonneg (f := fun k ↦ f (max k (n + m))) _ _ using 1

Premises used: summable_condensed_iff_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  Filter.EventuallyEq (β := ℝ) Filter.atTop (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k))
    fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) ↔
    Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))

Tactic:
rw [summable_congr_atTop]

Premises used: summable_congr_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ LT.lt (α := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ Filter.Tendsto (β := ℕ) (fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) Filter.atTop Filter.atTop

Tactic:
have h_pow := tendsto_pow_atTop_atTop_of_one_lt (r := 2) (by simp)
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h_pow : Filter.Tendsto (β := ℕ) (fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) Filter.atTop Filter.atTop
a : ℕ
hk : n + m ≤ HPow.hPow (α := ℕ) 2 a
⊢ HPow.hPow (α := ℝ) 2 a * f (HPow.hPow (α := ℕ) 2 a) =
    HPow.hPow (α := ℝ) 2 a * f (max (HPow.hPow (α := ℕ) 2 a) (n + m))

Tactic:
simp [max_eq_left hk]

Premises used: max_eq_left
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h_pow : Filter.Tendsto (β := ℕ) (fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) Filter.atTop Filter.atTop
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n + m ≤ HPow.hPow (α := ℕ) 2 x) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  Eq (α := ℝ) ((fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k)) x)
                    ((fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))) x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : ℕ) (hk : n + m ≤ HPow.hPow (α := ℕ) 2 a),
    HPow.hPow (α := ℝ) 2 a * f (HPow.hPow (α := ℕ) 2 a) =
      HPow.hPow (α := ℝ) 2 a * f (max (HPow.hPow (α := ℕ) 2 a) (n + m))
⊢ Filter.EventuallyEq (β := ℝ) Filter.atTop (fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (HPow.hPow (α := ℕ) 2 k))
    fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * f (max (HPow.hPow (α := ℕ) 2 k) (n + m))

Tactic:
filter_upwards [h_pow.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]

Premises used: HAdd.hAdd, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h : f =ᶠ[Filter.atTop] fun (k : ℕ) ↦ f (max k (n + m))
⊢ Summable f ↔ Summable (α := ℝ) fun (k : ℕ) ↦ f (max k (n + m))

Tactic:
rw [summable_congr_atTop]

Premises used: summable_congr_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
a : ℕ
hk : n + m ≤ a
⊢ f a = f (max a (n + m))

Tactic:
simp [max_eq_left hk]

Premises used: max_eq_left
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ n + m ≤ x) x} x →
          Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ f x = (fun (k : ℕ) ↦ f (max k (n + m))) x) x} x}
      a
h₁ h₂ : ∀ (a : ℕ) (hk : n + m ≤ a), f a = f (max a (n + m))
⊢ f =ᶠ[Filter.atTop] fun (k : ℕ) ↦ f (max k (n + m))

Tactic:
filter_upwards [Filter.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]

Premises used: HAdd.hAdd, Filter.eventually_ge_atTop
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
⊢ ∀ (n_1 : ℕ), LE.le (α := ℝ) 0 ((fun (k : ℕ) ↦ f (max k (n + m))) n_1)

Tactic:
simp_all
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 : ℕ
convert_2 :
  ∀ ⦃n_1 : ℕ⦄,
    0 < m_1 → m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)
⊢ ∀ ⦃n_1 : ℕ⦄,
    0 < m_1 → m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)

Tactic:
_
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
convert_2 :
  0 < m_1 → m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)
⊢ 0 < m_1 → m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)

Tactic:
_
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
h : 0 < m_1
convert_2 : m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)
⊢ m_1 ≤ n_1 → LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)

Tactic:
_
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
h : 0 < m_1
h_1 : m_1 ≤ n_1
⊢ ∀ n_2 ≥ n + m, f (n_2 + 1) ≤ f n_2

Tactic:
grind
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
h : 0 < m_1
h_1 : m_1 ≤ n_1
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | n + m ≤ x} (max m_1 (n + m))

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
h : 0 < m_1
h_1 : m_1 ≤ n_1
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | n + m ≤ x} (max n_1 (n + m))

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
h : 0 < m_1
h_1 : m_1 ≤ n_1
⊢ max m_1 (n + m) ≤ max n_1 (n + m)

Tactic:
grind
-- Module: Mathlib.Analysis.PSeries
Goal:
f : ℕ → ℝ
n : ℕ
hn : ∀ b ≥ n, 0 b ≤ f b
m : ℕ
hm : ∀ b ≥ m, f (b + 1) ≤ f b
m_1 n_1 : ℕ
h : 0 < m_1
h_1 : m_1 ≤ n_1
⊢ LE.le (α := ℝ) ((fun (k : ℕ) ↦ f (max k (n + m))) n_1) ((fun (k : ℕ) ↦ f (max k (n + m))) m_1)

Tactic:
exact antitoneOn_nat_Ici_of_succ_le (k := n + m) (by grind) (by simp) (by simp) (by grind)

Premises used: antitoneOn_nat_Ici_of_succ_le
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
inl : ∀ (hp : 0 ≤ p), (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
inr : ∀ (hp : p < 0), (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p

Tactic:
rcases le_or_gt 0 p with hp | hp

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
inl :
  (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) p)⁻¹) ↔
    1 < p
inl₁ : ∀ (n : ℕ), 0 ≤ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
inl₂ : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑m : ℝ) p)⁻¹
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p

Tactic:
rw [← summable_condensed_iff_of_nonneg]

Premises used: summable_condensed_iff_of_nonneg
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
inl : ‖2 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p
⊢ (Summable (α := ℝ) fun (k : ℕ) ↦ HPow.hPow (α := ℝ) 2 k * (HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℕ) 2 k) : ℝ) p)⁻¹) ↔
    1 < p

Tactic:
simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_natCast, ← rpow_mul zero_lt_two.le, mul_comm _ p,
        rpow_mul zero_lt_two.le, rpow_natCast, ← inv_pow, ← mul_pow,
        summable_geometric_iff_norm_lt_one]

Premises used: LT.lt.le, inv_pow, summable_geometric_iff_norm_lt_one, mul_comm, Nat.cast_pow, zero_lt_two, Real.rpow_mul, mul_pow, Nat.cast_two, Real.rpow_natCast
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
inl : ‖HPow.hPow (α := ℝ) (β := ℝ) 2 1 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p
⊢ ‖2 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p

Tactic:
nth_rw 1 [← rpow_one 2]

Premises used: Real.rpow_one, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
inl : Eq (α := ℝ) 2 0 ∧ 1 - p ≠ 0 ∨ LT.lt (α := ℝ) 1 2 ∧ 1 - p < 0 ∨ LT.lt (α := ℝ) 2 1 ∧ 0 < 1 - p ↔ 1 < p
⊢ ‖HPow.hPow (α := ℝ) (β := ℝ) 2 1 * (HPow.hPow (α := ℝ) 2 p)⁻¹‖ < 1 ↔ 1 < p

Tactic:
rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs,
        abs_of_pos (rpow_pos_of_pos zero_lt_two _), rpow_lt_one_iff zero_lt_two.le]

Premises used: Real.rpow_pos_of_pos, LT.lt.le, division_def, Real.rpow_lt_one_iff, abs_of_pos, Real.rpow_sub, zero_lt_two, Real.norm_eq_abs
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
⊢ Eq (α := ℝ) 2 0 ∧ 1 - p ≠ 0 ∨ LT.lt (α := ℝ) 1 2 ∧ 1 - p < 0 ∨ LT.lt (α := ℝ) 2 1 ∧ 0 < 1 - p ↔ 1 < p

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ 0 ≤ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
inl : 0 < HPow.hPow (α := ℝ) (↑m : ℝ) p
inl₁ : LE.le (α := ℝ) 0 (↑m : ℝ)
inl₂ : 0 ≤ p
⊢ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹ ≤ (HPow.hPow (α := ℝ) (↑m : ℝ) p)⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
this : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
⊢ ¬1 < p

Tactic:
have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
this_1 : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
this : ¬1 < p
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p

Tactic:
simpa only [this, iff_false]

Premises used: iff_false
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
inr : ¬Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p

Tactic:
suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) by
      have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
      simpa only [this, iff_false]
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
inr : ∀ (k : ℕ) (hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1) (hk₀ : k ≠ 0), False
⊢ False

Tactic:
obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
      ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
          (eventually_cofinite_ne 0)).exists

Premises used: gt_mem_nhds, Filter.eventually_cofinite_ne, Filter.Eventually.and, Filter.Eventually.exists, zero_lt_one, Summable.tendsto_cofinite_zero, Filter.Tendsto.eventually, OfNat.ofNat
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
k : ℕ
hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1
hk₀ : k ≠ 0
inr : k = 0
⊢ False

Tactic:
apply hk₀
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
k : ℕ
hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ LT.lt (α := ℝ) 0 (↑k : ℝ)

Tactic:
rw [← pos_iff_ne_zero, ← @Nat.cast_pos ℝ] at hk₀

Premises used: Nat.cast_pos, pos_iff_ne_zero
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
hp : p < 0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹
k : ℕ
hk₁ : (HPow.hPow (α := ℝ) (↑k : ℝ) p)⁻¹ < 1
hk₀ : LT.lt (α := ℝ) 0 (↑k : ℝ)
⊢ k = 0

Tactic:
simpa [inv_lt_one₀ (rpow_pos_of_pos hk₀ _), one_lt_rpow_iff_of_pos hk₀, hp,
      hp.not_gt, hk₀] using hk₁

Premises used: Real.rpow_pos_of_pos, inv_lt_one₀, Real.one_lt_rpow_iff_of_pos, LT.lt.not_gt
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
rcases : ∀ (p : ℝ), (Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-p)) ↔ -p < -1
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ p < -1

Tactic:
rcases neg_surjective p with ⟨p, rfl⟩

Premises used: neg_surjective, rfl
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-p)) ↔ -p < -1

Tactic:
simp [rpow_neg]

Premises used: Real.rpow_neg
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℝ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p) ↔ 1 < p

Tactic:
simp
-- Module: Mathlib.Analysis.PSeries
Goal:
p : ℕ
⊢ (Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) p)⁻¹) ↔ 1 < p

Tactic:
simp only [← rpow_natCast, summable_nat_rpow_inv, Nat.one_lt_cast]

Premises used: Real.summable_nat_rpow_inv, Nat.one_lt_cast, Real.rpow_natCast