Source indexedlemma · leanprover/lean4:v4.32.0

cancel_main'

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:1394 to 1402

Mathematical statement

Exact Lean statement

lemma cancel_main' {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hf0 : f 0 = 0) (hg : 0 ≤ g)
    (hf' : ∀ n, cumsum f n ≤ C * n) (hg' : Antitone g) (n : ℕ) :
    cumsum (f * g) n ≤ C * cumsum g n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cancel_main' {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hf0 : f 0 = 0) (hg : 0 ≤ g)    (hf' : ∀ n, cumsum f n ≤ C * n) (hg' : Antitone g) (n : ℕ) :    cumsum (f * g) n ≤ C * cumsum g n := by  match n with  | 0 => simp [cumsum]  | 1 => specialize hg 0 ; specialize hf' 1 ; simp only [cumsum, Finset.range_one,    Finset.sum_singleton, hf0, Nat.cast_one, mul_one, Pi.zero_apply, Pi.mul_apply, zero_mul,    ge_iff_le] at hf' hg ⊢ ; positivity  | n + 2 => convert! cancel_aux' hf hg hf' hg' (n + 2) using 1 ; simp [cumsum_succ] ; ring