Documentation

BV.Summatory

noncomputable def Nat.Icc (x y : ℝ) :

Equations

Nat.Icc x y = if x ≤ y ∧ 0 ≤ y then Finset.Icc ⌈x⌉₊ ⌊y⌋₊ else ∅

Instances For

@[simp]

theorem Nat.mem_Icc (x : ℝ) {y : ℝ} (n : ℕ) :

n ∈ Icc x y ↔ x ≤ ↑n ∧ ↑n ≤ y

theorem Nat.mem_Icc_zero {x : ℝ} (n : ℕ) :

n ∈ Icc 0 x ↔ ↑n ≤ x

theorem Nat.Icc_zero_nonempty {x : ℝ} (hx : 0 ≤ x) :

(Icc 0 x).Nonempty

@[simp]

theorem card_natIcc (x : ℝ) {y : ℝ} (hy : 0 ≤ y) :

(Nat.Icc x y).card = ⌊y⌋₊ + 1 - ⌈x⌉₊

@[simp]

theorem card_natIcc_zero (x : ℝ) (hx : 0 ≤ x) :

(Nat.Icc 0 x).card = ⌊x⌋₊ + 1

@[simp]

theorem Nat.Icc_eq_empty_of_neg (x : ℝ) {y : ℝ} (hy : y < 0) :

@[simp]

theorem Nat.Icc_eq_empty_of_lt (x : ℝ) {y : ℝ} (hy : y < x) :

theorem Nat.Icc_mono_left {x₁ x₂ y : ℝ} (hx : x₁ ≤ x₂) :

Icc x₂ y ⊆ Icc x₁ y

theorem Nat.Icc_mono_right {x y₁ y₂ : ℝ} (hy : y₁ ≤ y₂) :

Icc x y₁ ⊆ Icc x y₂

noncomputable def summatory {R : Type u_1} [AddCommMonoid R] (f : ℕ → R) (x : ℝ) :

R

Equations

summatory f x = ∑ i ∈ Nat.Icc 1 x, f i

Instances For

theorem summatory_nonneg {R : Type u_1} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] (f : ℕ → R) (x : ℝ) (hf : ∀ (n : ℕ), ↑n ≤ x → 0 ≤ f n) :

0 ≤ summatory f x

theorem summatory_of_neg {R : Type u_1} [AddCommMonoid R] {f : ℕ → R} {x : ℝ} (hx : x < 0) :

summatory f x = 0

theorem summatory_of_nonpos {R : Type u_1} [AddCommMonoid R] {f : ℕ → R} {x : ℝ} (hx : x ≤ 0) :

summatory f x = 0

theorem summatory_apply {R : Type u_1} [AddCommMonoid R] {f : ℕ → R} {x : ℝ} :

summatory f x = ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, f n

theorem summatory_eq_zero {R : Type u_1} [AddCommMonoid R] {f : ℕ → R} {x : ℝ} (hf : ∀ (n : ℕ), 0 < n → ↑n ≤ x → f n = 0) :

summatory f x = 0

theorem summatory_congr {R : Type u_1} [AddCommMonoid R] {f g : ℕ → R} {x y : ℝ} (hxy : x = y) (h : ∀ (n : ℕ), 0 < n → ↑n ≤ x → f n = g n) :

summatory f x = summatory g y

theorem summatory_le_summatory {R : Type u_1} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] {f g : ℕ → R} {x : ℝ} (h : ∀ (n : ℕ), 0 < n → ↑n ≤ x → f n ≤ g n) :

summatory f x ≤ summatory g x

theorem summatory_congr_fun {R : Type u_1} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] {f g : ℕ → R} {x : ℝ} (h : ∀ (n : ℕ), 0 < n → ↑n ≤ x → f n = g n) :

summatory f x = summatory g x

theorem summatory_eq_summatory_of_lt_of_eq_zero {R : Type u_1} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] (f : ℕ → R) (x y : ℝ) (hxy : x ≤ y) (hf : ∀ (n : ℕ), x < ↑n ∧ ↑n ≤ y → f n = 0) :

summatory f x = summatory f y

theorem summatory_add_distrib {R : Type u_1} [AddCommMonoid R] {f g : ℕ → R} {x : ℝ} :

summatory (fun (n : ℕ) => f n + g n) x = summatory f x + summatory g x

theorem summatory_sub_distrib {R : Type u_1} [AddCommGroup R] {f g : ℕ → R} {x : ℝ} :

summatory (fun (n : ℕ) => f n - g n) x = summatory f x - summatory g x

theorem summatory_neg {R : Type u_1} [AddCommGroup R] {f : ℕ → R} {x : ℝ} :

summatory (fun (n : ℕ) => -f n) x = -summatory f x

theorem mul_summatory {R : Type u_1} [Semiring R] {f : ℕ → R} {c : R} {x : ℝ} :

summatory (fun (n : ℕ) => c * f n) x = c * summatory f x

theorem summatory_mul {R : Type u_1} [Semiring R] {f : ℕ → R} {c : R} {x : ℝ} :

summatory (fun (n : ℕ) => f n * c) x = summatory f x * c

@[simp]

theorem summatory_zero {R : Type u_1} [AddCommMonoid R] {x : ℝ} :

summatory (fun (x : ℕ) => 0) x = 0

@[simp]

theorem map_summatory {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] {G : Type u_3} [FunLike G M N] [AddMonoidHomClass G M N] (g : G) (f : ℕ → M) (x : ℝ) :

g (summatory (fun (n : ℕ) => f n) x) = summatory (fun (n : ℕ) => g (f n)) x

theorem norm_summatory_le {M : Type u_1} [SeminormedAddCommGroup M] (f : ℕ → M) (x : ℝ) :

‖summatory f x‖ ≤ summatory (fun (n : ℕ) => ‖f n‖) x

def summatory_positivity :

Mathlib.Meta.Positivity.PositivityExt

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem summatory_le_UB {R : Type u_1} {f : ℕ → R} [NormedAddCommGroup R] [Lattice R] [IsOrderedAddMonoid R] (x : ℝ) (hx : 0 ≤ x) (M : ℝ) (hf : ∀ (n : ℕ), ↑n ≤ x → ‖f n‖ ≤ M) :

‖summatory f x‖ ≤ x * M

theorem summatory_le_support_mul_UB {R : Type u_1} {f : ℕ → R} [NormedAddCommGroup R] [Lattice R] [IsOrderedAddMonoid R] (x S : ℝ) (hS : 0 ≤ S) (M : ℝ) (hf : ∀ (n : ℕ), ↑n ≤ S → ‖f n‖ ≤ M) (hf_support : ∀ (n : ℕ), ↑n > S → f n = 0) :

‖summatory f x‖ ≤ S * M

theorem aeStronglyMeasurable_summatory {R : Type u_1} [NormedAddCommGroup R] [MeasurableSpace R] {f : ℕ → R} :

MeasureTheory.AEStronglyMeasurable (summatory f) MeasureTheory.volume

theorem measurable_summatory {R : Type u_1} [NormedAddCommGroup R] [MeasurableSpace R] {f : ℕ → R} :

Measurable (summatory f)

theorem summatory_tendsTo_right {R : Type u_1} [NormedAddCommGroup R] {f : ℕ → R} (x : ℝ) :

Filter.Tendsto (summatory f) (nhdsWithin x (Set.Ici x)) (nhds (summatory f x))

theorem measurable_summatory_const {X : Type u_1} {R : Type u_2} [MeasurableSpace X] [NormedAddCommGroup R] [MeasurableSpace R] [MeasurableAdd₂ R] {f : X → ℕ → R} (hf : ∀ (n : ℕ), Measurable fun (x : X) => f x n) (N : ℝ) :

Measurable fun (t : X) => summatory (f t) N

theorem aeStronglyMeasurable_summatory_const {X : Type u_1} {R : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup R] {f : X → ℕ → R} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fun (x : X) => f x n) μ) (N : ℝ) :

MeasureTheory.AEStronglyMeasurable (fun (t : X) => summatory (f t) N) μ

theorem summatory_tendsTo_left {R : Type u_1} [NormedAddCommGroup R] {f : ℕ → R} (x : ℝ) :

Filter.Tendsto (summatory f) (nhdsWithin x (Set.Iio x)) (nhds (∑ n ∈ Finset.Ioo 0 ⌈x⌉₊, f n))

theorem summatory_isLocallyBounded {R : Type u_1} [NormedAddCommGroup R] {f : ℕ → R} :

IsLocallyBounded (summatory f)

theorem monotone_summatory (g : ℕ → ℝ) (hg : ∀ (n : ℕ), 0 ≤ g n) :

Monotone (summatory g)

theorem summatory_locallyIntegrable (f : ℕ → ℝ) :

MeasureTheory.LocallyIntegrable (summatory f) MeasureTheory.volume

theorem summatory_locallyIntegrable_complex (f : ℕ → ℂ) :

MeasureTheory.LocallyIntegrable (summatory f) MeasureTheory.volume