Projects.RealAnalysis.ConditionalConvergence

source

def RealAnalysis.CondConv (a : ℕ → ℝ) :

Prop

Equations

RealAnalysis.CondConv a = (RealAnalysis.converges (RealAnalysis.series a) ∧ ¬RealAnalysis.AbsConv a)

Instances For

source

noncomputable def RealAnalysis.CondConv.σp (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.σp a = RealAnalysis.mkSubseq a fun (x : ℝ) => 0 ≤ x

Instances For

source

noncomputable def RealAnalysis.CondConv.σn (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.σn a = RealAnalysis.mkSubseq a fun (x : ℝ) => x < 0

Instances For

source

noncomputable def RealAnalysis.CondConv.ap (a : ℕ → ℝ) (n : ℕ) :

ℝ

Equations

RealAnalysis.CondConv.ap a n = a (RealAnalysis.CondConv.σp a n)

Instances For

source

noncomputable def RealAnalysis.CondConv.an (a : ℕ → ℝ) (n : ℕ) :

ℝ

Equations

RealAnalysis.CondConv.an a n = a (RealAnalysis.CondConv.σn a n)

Instances For

source

noncomputable def RealAnalysis.CondConv.M (a : ℕ → ℝ) :

ℝ

Equations

RealAnalysis.CondConv.M a = RealAnalysis.limit (RealAnalysis.series a)

Instances For

source

def RealAnalysis.CondConv.fgCnd (F : ℝ → ℝ) (a : ℕ → ℝ) (f g : ℕ → ℕ) :

Prop

Equations

RealAnalysis.CondConv.fgCnd F a f g = ((∀ (n : ℕ), f n + g n = n) ∧ (∀ (i j : ℕ), i ≤ j → f i ≤ f j) ∧ (∀ (i j : ℕ), i ≤ j → g i ≤ g j) ∧ (∀ (n : ℕ), ∃ (k : ℕ), n ≤ f k) ∧ (∀ (n : ℕ), ∃ (k : ℕ), n ≤ g k) ∧ ∀ (n : ℕ), RealAnalysis.series (fun (x : ℕ) => F (a x)) n = RealAnalysis.series (fun (x : ℕ) => F (RealAnalysis.CondConv.ap a x)) (f n) + RealAnalysis.series (fun (x : ℕ) => F (RealAnalysis.CondConv.an a x)) (g n))

Instances For

source

noncomputable def RealAnalysis.CondConv.fAux (F : ℝ → ℝ) (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.fAux F a = Classical.epsilon fun (f : ℕ → ℕ) => ∃ (g : ℕ → ℕ), RealAnalysis.CondConv.fgCnd F a f g

Instances For

source

noncomputable def RealAnalysis.CondConv.gAux (F : ℝ → ℝ) (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.gAux F a = Classical.epsilon fun (g : ℕ → ℕ) => RealAnalysis.CondConv.fgCnd F a (RealAnalysis.CondConv.fAux F a) g

Instances For

source

noncomputable def RealAnalysis.CondConv.f (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.f a = RealAnalysis.CondConv.fAux id a

Instances For

source

noncomputable def RealAnalysis.CondConv.g (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.g a = RealAnalysis.CondConv.gAux id a

Instances For

source

noncomputable def RealAnalysis.CondConv.f' (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.f' a = RealAnalysis.CondConv.fAux abs a

Instances For

source

noncomputable def RealAnalysis.CondConv.g' (a : ℕ → ℝ) :

ℕ → ℕ

Equations

RealAnalysis.CondConv.g' a = RealAnalysis.CondConv.gAux abs a

Instances For

source

theorem RealAnalysis.CondConv.converges_series {a : ℕ → ℝ} (H : CondConv a) :

converges (series a)

source

theorem RealAnalysis.CondConv.not_absConv {a : ℕ → ℝ} (H : CondConv a) :

¬AbsConv a

source

theorem RealAnalysis.CondConv.drop {a : ℕ → ℝ} (H : CondConv a) {N : ℕ} :

CondConv fun (x : ℕ) => a (N + x)

source

theorem RealAnalysis.CondConv.drop_iff {a : ℕ → ℝ} {N : ℕ} :

(CondConv fun (x : ℕ) => a (N + x)) ↔ CondConv a

source

theorem RealAnalysis.CondConv.neg_iff {a : ℕ → ℝ} :

CondConv (-a) ↔ CondConv a

source

theorem RealAnalysis.CondConv.infp_pos {a : ℕ → ℝ} (H : CondConv a) :

Infp a fun (x : ℝ) => 0 < x

source

theorem RealAnalysis.CondConv.infp_neg {a : ℕ → ℝ} (H : CondConv a) :

Infp a fun (x : ℝ) => x < 0

source

theorem RealAnalysis.CondConv.infp_nonneg {a : ℕ → ℝ} (H : CondConv a) :

Infp a fun (x : ℝ) => 0 ≤ x

source

theorem RealAnalysis.CondConv.infp_nonpos {a : ℕ → ℝ} (H : CondConv a) :

Infp a fun (x : ℝ) => x ≤ 0

source

theorem RealAnalysis.CondConv.subseq_σp (a : ℕ → ℝ) :

Subseq (σp a)

source

theorem RealAnalysis.CondConv.subseq_σn (a : ℕ → ℝ) :

Subseq (σn a)

source

theorem RealAnalysis.CondConv.tendsTo_series {a : ℕ → ℝ} (H : CondConv a) :

tendsTo (series a) (M a)

source

theorem RealAnalysis.CondConv.σp_spec {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

0 ≤ a n ↔ ∃ (k : ℕ), σp a k = n

source

theorem RealAnalysis.CondConv.σn_spec {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

a n < 0 ↔ ∃ (k : ℕ), σn a k = n

source

theorem RealAnalysis.CondConv.σp_spec' {a : ℕ → ℝ} (H : CondConv a) (n : ℕ) :

0 ≤ a n ↔ ∃ (k : ℕ), σp a k = n

source

theorem RealAnalysis.CondConv.σn_spec' {a : ℕ → ℝ} (H : CondConv a) (n : ℕ) :

a n < 0 ↔ ∃ (k : ℕ), σn a k = n

source

theorem RealAnalysis.CondConv.ap_nonneg {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

0 ≤ ap a n

source

theorem RealAnalysis.CondConv.an_neg {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

an a n < 0

source

theorem RealAnalysis.CondConv.an_nonpos {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

an a n ≤ 0

source

theorem RealAnalysis.CondConv.ap_fn_nonneg {a : ℕ → ℝ} (H : CondConv a) :

0 ≤ ap a

source

theorem RealAnalysis.CondConv.an_fn_neg {a : ℕ → ℝ} (H : CondConv a) :

an a < 0

source

theorem RealAnalysis.CondConv.an_fn_nonpos {a : ℕ → ℝ} (H : CondConv a) :

an a ≤ 0

source

theorem RealAnalysis.CondConv.abs_ap {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

|ap a n| = ap a n

source

theorem RealAnalysis.CondConv.abs_an {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

|an a n| = -an a n

source

theorem RealAnalysis.CondConv.abs_ap_fn {a : ℕ → ℝ} (H : CondConv a) :

|ap a| = ap a

source

theorem RealAnalysis.CondConv.abs_an_fn {a : ℕ → ℝ} (H : CondConv a) :

|an a| = -an a

source

theorem RealAnalysis.CondConv.series_ap_nonneg {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

0 ≤ series (ap a) n

source

theorem RealAnalysis.CondConv.series_an_nonpos {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

series (an a) n ≤ 0

source

theorem RealAnalysis.CondConv.series_ap_fn_nonneg {a : ℕ → ℝ} (H : CondConv a) :

0 ≤ series (ap a)

source

theorem RealAnalysis.CondConv.series_an_fn_nonpos {a : ℕ → ℝ} (H : CondConv a) :

series (an a) ≤ 0

source

theorem RealAnalysis.CondConv.exi_fgCnd {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} :

∃ (f : ℕ → ℕ) (g : ℕ → ℕ), fgCnd F a f g

source

theorem RealAnalysis.CondConv.fgCnd_fAux_gAux {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} :

fgCnd F a (fAux F a) (gAux F a)

source

theorem RealAnalysis.CondConv.fAux_add_gAux {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} {n : ℕ} :

fAux F a n + gAux F a n = n

source

theorem RealAnalysis.CondConv.fAux_le_of_le {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} {i j : ℕ} (h : i ≤ j) :

fAux F a i ≤ fAux F a j

source

theorem RealAnalysis.CondConv.gAux_le_of_le {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} {i j : ℕ} (h : i ≤ j) :

gAux F a i ≤ gAux F a j

source

theorem RealAnalysis.CondConv.exi_fAux_ge {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} {n : ℕ} :

∃ (k : ℕ), n ≤ fAux F a k

source

theorem RealAnalysis.CondConv.exi_gAux_ge {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} {n : ℕ} :

∃ (k : ℕ), n ≤ gAux F a k

source

theorem RealAnalysis.CondConv.series_eq_fAux_add_gAux {a : ℕ → ℝ} (H : CondConv a) {F : ℝ → ℝ} {n : ℕ} :

series (fun (x : ℕ) => F (a x)) n = series (fun (x : ℕ) => F (ap a x)) (fAux F a n) + series (fun (x : ℕ) => F (an a x)) (gAux F a n)

source

theorem RealAnalysis.CondConv.fgCnd_f_g {a : ℕ → ℝ} (H : CondConv a) :

fgCnd id a (f a) (g a)

source

theorem RealAnalysis.CondConv.f_add_g {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

f a n + g a n = n

source

theorem RealAnalysis.CondConv.f_le_of_le {a : ℕ → ℝ} (H : CondConv a) {i j : ℕ} (h : i ≤ j) :

f a i ≤ f a j

source

theorem RealAnalysis.CondConv.g_le_of_le {a : ℕ → ℝ} (H : CondConv a) {i j : ℕ} (h : i ≤ j) :

g a i ≤ g a j

source

theorem RealAnalysis.CondConv.exi_f_ge {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

∃ (k : ℕ), n ≤ f a k

source

theorem RealAnalysis.CondConv.exi_g_ge {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

∃ (k : ℕ), n ≤ g a k

source

theorem RealAnalysis.CondConv.series_eq_f_add_g {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

series a n = series (ap a) (f a n) + series (an a) (g a n)

source

theorem RealAnalysis.CondConv.fgCnd_f'_g' {a : ℕ → ℝ} (H : CondConv a) :

fgCnd abs a (f' a) (g' a)

source

theorem RealAnalysis.CondConv.f'_add_g' {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

f' a n + g' a n = n

source

theorem RealAnalysis.CondConv.f'_le_of_le {a : ℕ → ℝ} (H : CondConv a) {i j : ℕ} (h : i ≤ j) :

f' a i ≤ f' a j

source

theorem RealAnalysis.CondConv.g'_le_of_le {a : ℕ → ℝ} (H : CondConv a) {i j : ℕ} (h : i ≤ j) :

g' a i ≤ g' a j

source

theorem RealAnalysis.CondConv.exi_f'_ge {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

∃ (k : ℕ), n ≤ f' a k

source

theorem RealAnalysis.CondConv.exi_g'_ge {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

∃ (k : ℕ), n ≤ g' a k

source

theorem RealAnalysis.CondConv.series_eq_f'_add_g' {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

series |a| n = series |ap a| (f' a n) + series |an a| (g' a n)

source

theorem RealAnalysis.CondConv.monoLe_series_ap {a : ℕ → ℝ} (H : CondConv a) :

monoLe (series (ap a))

source

theorem RealAnalysis.CondConv.monoGt_series_an {a : ℕ → ℝ} (H : CondConv a) :

monoGt (series (an a))

source

theorem RealAnalysis.CondConv.monoGe_series_an {a : ℕ → ℝ} (H : CondConv a) :

monoGe (series (an a))

source

theorem RealAnalysis.CondConv.not_converges_series_ap_or_an {a : ℕ → ℝ} (H : CondConv a) :

¬converges (series (ap a)) ∨ ¬converges (series (an a))

source

theorem RealAnalysis.CondConv.not_converges_series_ap {a : ℕ → ℝ} (H : CondConv a) :

¬converges (series (ap a))

source

theorem RealAnalysis.CondConv.not_converges_series_an {a : ℕ → ℝ} (H : CondConv a) :

¬converges (series (an a))

source

theorem RealAnalysis.CondConv.exi_ap_gt {a : ℕ → ℝ} (H : CondConv a) (L : ℝ) :

∃ (n : ℕ), L < series (ap a) n

source

theorem RealAnalysis.CondConv.exi_an_lt {a : ℕ → ℝ} (H : CondConv a) (L : ℝ) :

∃ (n : ℕ), series (an a) n < L

source

theorem RealAnalysis.CondConv.neg_of_lt_σp_zero {a : ℕ → ℝ} {n : ℕ} (h : n < σp a 0) :

a n < 0

source

theorem RealAnalysis.CondConv.nonneg_of_lt_σn_zero {a : ℕ → ℝ} {n : ℕ} (h : n < σn a 0) :

0 ≤ a n

source

theorem RealAnalysis.CondConv.sum_map_filter_range_σp {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

(List.map a (List.filter (fun (x : ℕ) => decide (0 ≤ a x)) (List.range (σp a n)))).sum = series (ap a) n

source

theorem RealAnalysis.CondConv.sum_map_filter_range_σn {a : ℕ → ℝ} (H : CondConv a) {n : ℕ} :

(List.map a (List.filter (fun (x : ℕ) => decide (a x < 0)) (List.range (σn a n)))).sum = series (an a) n

source

theorem RealAnalysis.CondConv.exi_ap_map_range_gt {a : ℕ → ℝ} (H : CondConv a) (L : ℝ) :

∃ (n : ℕ), L < (List.map a (List.filter (fun (x : ℕ) => decide (0 ≤ a x)) (List.range n))).sum

source

theorem RealAnalysis.CondConv.exi_an_map_range_lt {a : ℕ → ℝ} (H : CondConv a) (L : ℝ) :

∃ (n : ℕ), (List.map a (List.filter (fun (x : ℕ) => decide (a x < 0)) (List.range n))).sum < L

source

theorem RealAnalysis.CondConv.tendsTo_zero {a : ℕ → ℝ} (H : CondConv a) :

tendsTo a 0

source

theorem RealAnalysis.CondConv.bounds_tendsTo_zero {a : ℕ → ℝ} (H : CondConv a) :

tendsTo (bounds a) 0

source

theorem RealAnalysis.CondConv.exi_ap_map_range_drop_gt {a : ℕ → ℝ} (H : CondConv a) (L : ℝ) (k : ℕ) :

∃ (n : ℕ), L < (List.map a (List.filter (fun (x : ℕ) => decide (0 ≤ a x)) (List.map (fun (x : ℕ) => k + x) (List.range n)))).sum

source

theorem RealAnalysis.CondConv.exi_an_map_range_drop_lt {a : ℕ → ℝ} (H : CondConv a) (L : ℝ) (k : ℕ) :

∃ (n : ℕ), (List.map a (List.filter (fun (x : ℕ) => decide (a x < 0)) (List.map (fun (x : ℕ) => k + x) (List.range n)))).sum < L

source

theorem RealAnalysis.CondConv.exi_add_ap_map_range_drop_gt {a : ℕ → ℝ} (H : CondConv a) (s L : ℝ) (k : ℕ) :

∃ (n : ℕ), L < s + (List.map a (List.filter (fun (x : ℕ) => decide (0 ≤ a x)) (List.map (fun (x : ℕ) => k + x) (List.range n)))).sum

source

theorem RealAnalysis.CondConv.exi_add_an_map_range_drop_lt {a : ℕ → ℝ} (H : CondConv a) (s L : ℝ) (k : ℕ) :

∃ (n : ℕ), s + (List.map a (List.filter (fun (x : ℕ) => decide (a x < 0)) (List.map (fun (x : ℕ) => k + x) (List.range n)))).sum < L