Documentation

KolmogorovExtension4.AuxLemmas

theorem Finset.sUnion_disjiUnion {α : Type u_1} {β : Type u_2} {f : αFinset (Set β)} (I : Finset α) (hf : (↑I).PairwiseDisjoint f) :
⋃₀ (I.disjiUnion f hf) = aI, ⋃₀ (f a)
theorem Finset.sum_image_le_of_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq α] [OrderedAddCommMonoid β] [SMulPosMono β] {J : Finset ι} {g : ια} {f : αβ} (hf : uFinset.image g J, 0 f u) :
uFinset.image g J, f u uJ, f (g u)
theorem Finset.sum_image_of_disjoint {ι : Type u_3} {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] [DecidableEq α] [AddCommMonoid β] {g : αβ} (hg_bot : g = 0) {f : ια} {I : Finset ι} (hf_disj : (↑I).PairwiseDisjoint f) :
sFinset.image f I, g s = iI, g (f i)
theorem Finset.prod_image_of_disjoint {ι : Type u_3} {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] [DecidableEq α] [CommMonoid β] {g : αβ} (hg_bot : g = 1) {f : ια} {I : Finset ι} (hf_disj : (↑I).PairwiseDisjoint f) :
sFinset.image f I, g s = iI, g (f i)
theorem MeasurableSet.accumulate {α : Type u_1} :
∀ {x : MeasurableSpace α} {s : Set α}, (∀ (n : ), MeasurableSet (s n))∀ (n : ), MeasurableSet (Set.Accumulate s n)
theorem Set.disjoint_accumulate {α : Type u_1} {s : Set α} (hs : Pairwise (Disjoint on s)) {i : } {j : } (hij : i < j) :
theorem Set.accumulate_succ {α : Type u_1} (s : Set α) (n : ) :
Set.Accumulate s (n + 1) = Set.Accumulate s n s (n + 1)
@[simp]
theorem accumulate_zero_nat {α : Type u_1} (s : Set α) :
theorem NNReal.exists_seq_pos_summable_eq (x : NNReal) (hx : 0 < x) :
∃ (f : NNReal), (∀ (n : ), 0 < f n) Summable f ∑' (n : ), f n = x

Given x > 0, there is a sequence of positive reals summing to x.

theorem NNReal.exists_seq_pos_summable_lt (x : NNReal) (hx : 0 < x) :
∃ (f : NNReal), (∀ (n : ), 0 < f n) Summable f ∑' (n : ), f n < x

Given x > 0, there is a sequence of positive reals summing to something less than x.

theorem ENNReal.exists_seq_pos_eq (x : ENNReal) (hx : 0 < x) :
∃ (f : ENNReal), (∀ (n : ), 0 < f n) ∑' (n : ), f n = x

Given some x > 0, there is a sequence of positive reals summing to x.

theorem ENNReal.exists_seq_pos_lt (x : ENNReal) (hx : 0 < x) :
∃ (f : ENNReal), (∀ (n : ), 0 < f n) ∑' (n : ), f n < x

Given some x > 0, there is a sequence of positive reals summing to something less than x.

theorem ENNReal.tendsto_atTop_zero_const_sub_iff (f : ENNReal) (a : ENNReal) (ha : a ) (hfa : ∀ (n : ), f n a) :
Filter.Tendsto (fun (n : ) => a - f n) Filter.atTop (nhds 0) Filter.Tendsto (fun (n : ) => f n) Filter.atTop (nhds a)
theorem ENNReal.tendsto_atTop_zero_iff_of_antitone (f : ENNReal) (hf : Antitone f) :
Filter.Tendsto f Filter.atTop (nhds 0) ∀ (ε : ENNReal), 0 < ε∃ (n : ), f n ε
theorem ENNReal.tendsto_atTop_zero_iff_of_antitone' (f : ENNReal) (hf : Antitone f) :
Filter.Tendsto f Filter.atTop (nhds 0) ∀ (ε : ENNReal), 0 < ε∃ (n : ), f n < ε