def RealAnalysis.Infp (a : ℕ → ℝ) (p : ℝ → Prop) : Prop

Equations

• RealAnalysis.Infp a p = ∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ p (a n)

noncomputable def RealAnalysis.mkSubseq (a : ℕ → ℝ) (p : ℝ → Prop) (n : ℕ) : ℕ

Equations

• RealAnalysis.mkSubseq a p 0 = Nat.find! fun (x : ℕ) => p (a x)
• RealAnalysis.mkSubseq a p n_2.succ = RealAnalysis.mkSubseq a p n_2 + 1 + Nat.find! fun (x : ℕ) => p (a (RealAnalysis.mkSubseq a p n_2 + 1 + x))

theorem RealAnalysis.absConv_drop_of {a : ℕ → ℝ} {N : ℕ} (h : AbsConv a) : AbsConv fun (x : ℕ) => a (N + x)

theorem RealAnalysis.absConv_drop_iff {a : ℕ → ℝ} {N : ℕ} : (AbsConv fun (x : ℕ) => a (N + x)) ↔ AbsConv a

theorem RealAnalysis.absConv_neg {a : ℕ → ℝ} : AbsConv (-a) ↔ AbsConv a

theorem RealAnalysis.infp_iff_infinite {a : ℕ → ℝ} {p : ℝ → Prop} : Infp a p ↔ {n : ℕ | p (a n)}.Infinite

theorem RealAnalysis.subseq_mkSubseq {a : ℕ → ℝ} {p : ℝ → Prop} : Subseq (mkSubseq a p)

theorem RealAnalysis.exi_add_of_infp {a : ℕ → ℝ} {p : ℝ → Prop} {N : ℕ} (h : Infp a p) : ∃ (n : ℕ), p (a (N + n))

theorem RealAnalysis.exi_of_infp {a : ℕ → ℝ} {p : ℝ → Prop} (h : Infp a p) : ∃ (n : ℕ), p (a n)

theorem RealAnalysis.mkSubseq_spec {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} (h : Infp a p) : p (a (mkSubseq a p n))

theorem RealAnalysis.apply_of_mkSubseq_eq {a : ℕ → ℝ} {p : ℝ → Prop} {n k : ℕ} (h : Infp a p) (h₁ : mkSubseq a p k = n) : p (a n)

theorem RealAnalysis.infp_drop_of {a : ℕ → ℝ} {p : ℝ → Prop} {N : ℕ} (h : Infp a p) : Infp (fun (x : ℕ) => a (N + x)) p

theorem RealAnalysis.infp_of_drop {a : ℕ → ℝ} {p : ℝ → Prop} {N : ℕ} (h : Infp (fun (x : ℕ) => a (N + x)) p) : Infp a p

theorem RealAnalysis.infp_drop_iff {a : ℕ → ℝ} {p : ℝ → Prop} {N : ℕ} : Infp (fun (x : ℕ) => a (N + x)) p ↔ Infp a p

theorem RealAnalysis.exi_mkSubseq_eq_of_apply {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} (h : Infp a p) (h₁ : p (a n)) : ∃ (k : ℕ), mkSubseq a p k = n

theorem RealAnalysis.apply_iff_exi_mkSubseq_eq {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} (h : Infp a p) : p (a n) ↔ ∃ (k : ℕ), mkSubseq a p k = n

theorem RealAnalysis.exi_subseq_of_infp {a : ℕ → ℝ} {p : ℝ → Prop} (h : Infp a p) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ ∀ (n : ℕ), p (a n) ↔ ∃ (k : ℕ), σ k = n

theorem RealAnalysis.infp_of_imp {a : ℕ → ℝ} {p₁ p₂ : ℝ → Prop} (h₁ : Infp a p₁) (h₂ : ∀ (n : ℕ), p₁ (a n) → p₂ (a n)) : Infp a p₂

theorem RealAnalysis.exi_gt_of_monoLe_and_not_converges {a : ℕ → ℝ} (h₁ : monoLe a) (h₂ : ¬converges a) (L : ℝ) : ∃ (N : ℕ), L < a N

theorem RealAnalysis.exi_lt_of_monoGe_and_not_converges {a : ℕ → ℝ} (h₁ : monoGe a) (h₂ : ¬converges a) (L : ℝ) : ∃ (N : ℕ), a N < L

theorem RealAnalysis.monoLe_series_of_nonneg {a : ℕ → ℝ} (h : ∀ (n : ℕ), 0 ≤ a n) : monoLe (series a)

theorem RealAnalysis.monoGe_series_of_nonpos {a : ℕ → ℝ} (h : ∀ (n : ℕ), a n ≤ 0) : monoGe (series a)

theorem RealAnalysis.monoLt_series_of_pos {a : ℕ → ℝ} (h : ∀ (n : ℕ), 0 < a n) : monoLt (series a)

theorem RealAnalysis.monoGt_series_of_neg {a : ℕ → ℝ} (h : ∀ (n : ℕ), a n < 0) : monoGt (series a)

theorem RealAnalysis.subseq_nat_succ_le {σ : ℕ → ℕ} {n : ℕ} (h : Subseq σ) : σ n + 1 ≤ σ (n + 1)

theorem RealAnalysis.subseq_nat_eq_succ_of_subseq_eq_succ {σ : ℕ → ℕ} {n m : ℕ} (h₁ : Subseq σ) (h₂ : σ n = σ m + 1) : n = m + 1

theorem RealAnalysis.subseq_card_filter_range_eq {a : ℕ → ℝ} {p : ℝ → Prop} {σ : ℕ → ℕ} {n k : ℕ} [hp : DecidablePred p] (h₁ : Subseq σ) (h₂ : ∀ (n : ℕ), p (a n) ↔ ∃ (k : ℕ), σ k = n) (h₃ : σ k = n) : {k ∈ Finset.range n | p (a k)}.card = k

theorem RealAnalysis.exi_fn_series_of_subseq_cover {a : ℕ → ℝ} {p : ℝ → Prop} {σ₁ σ₂ : ℕ → ℕ} {F : ℝ → ℝ} (h₁ : Subseq σ₁) (h₂ : Subseq σ₂) (h₃ : ∀ (n : ℕ), p (a n) ↔ ∃ (k : ℕ), σ₁ k = n) (h₄ : ∀ (n : ℕ), ¬p (a n) ↔ ∃ (k : ℕ), σ₂ k = n) : ∃ (f : ℕ → ℕ) (g : ℕ → ℕ), (∀ (n : ℕ), f n + g n = n) ∧ (∀ (i j : ℕ), i ≤ j → f i ≤ f j) ∧ (∀ (i j : ℕ), i ≤ j → g i ≤ g j) ∧ (Infp a p → ∀ (n : ℕ), ∃ (k : ℕ), n ≤ f k) ∧ ((Infp a fun (x : ℝ) => ¬p x) → ∀ (n : ℕ), ∃ (k : ℕ), n ≤ g k) ∧ ∀ (n : ℕ), series (fun (x : ℕ) => F (a x)) n = series (fun (x : ℕ) => F (a (σ₁ x))) (f n) + series (fun (x : ℕ) => F (a (σ₂ x))) (g n)

theorem RealAnalysis.not_of_lt_mkSubseq_zero {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} (h : n < mkSubseq a p 0) : ¬p (a n)

@[simp]

theorem RealAnalysis.mkSubseq_lt_mkSubseq_succ {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} : mkSubseq a p n < mkSubseq a p (n + 1)

@[simp]

theorem RealAnalysis.mkSubseq_le_mkSubseq_succ {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} : mkSubseq a p n ≤ mkSubseq a p (n + 1)

theorem RealAnalysis.not_of_between_mkSubseq {a : ℕ → ℝ} {p : ℝ → Prop} {k : ℕ} (n : ℕ) (H : Infp a p) (h₁ : mkSubseq a p n < k) (h₂ : k < mkSubseq a p (n + 1)) : ¬p (a k)

theorem RealAnalysis.filter_range_mkSubseq_succ {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} [hp : DecidablePred p] (H : Infp a p) : List.filter (fun (x : ℕ) => decide (p (a x))) (List.range (mkSubseq a p (n + 1))) = List.filter (fun (x : ℕ) => decide (p (a x))) (List.range (mkSubseq a p n)) ++ [mkSubseq a p n]