Several 'bespoke' facts about limsup and liminf on ENNReal / NNReal needed in SteinsLemma

theorem exists_strictMono_seq_le (y : NNReal) (f : NNReal → ℕ → ENNReal) (hf : ∀ x > 0, Filter.liminf (f x) Filter.atTop ≤ ↑y) : ∃ (n : ℕ → ℕ), StrictMono n ∧ ∀ (k : ℕ), f (↑k + 1)⁻¹ (n k) ≤ ↑y + ↑(↑k + 1)⁻¹

theorem exists_seq_bound (y : NNReal) (f : NNReal → ℕ → ENNReal) (hf : ∀ x > 0, Filter.limsup (f x) Filter.atTop ≤ ↑y) : ∃ (M : ℕ → ℕ), StrictMono M ∧ ∀ (k n : ℕ), n ≥ M k → f (↑k + 1)⁻¹ n ≤ ↑y + (↑k + 1)⁻¹

theorem exists_liminf_zero_of_forall_liminf_le (y : NNReal) (f : NNReal → ℕ → ENNReal) (hf : ∀ x > 0, Filter.liminf (f x) Filter.atTop ≤ ↑y) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.liminf (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem exists_liminf_zero_of_forall_liminf_le_with_UB (y : NNReal) (f : NNReal → ℕ → ENNReal) {z : NNReal} (hz : 0 < z) (hf : ∀ x > 0, Filter.liminf (f x) Filter.atTop ≤ ↑y) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ (∀ (x : ℕ), g x < z) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.liminf (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem exists_limsup_zero_of_forall_limsup_le (y : NNReal) (f : NNReal → ℕ → ENNReal) (hf : ∀ x > 0, Filter.limsup (f x) Filter.atTop ≤ ↑y) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.limsup (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem tendsto_of_block_sequence {α : Type u_1} [TopologicalSpace α] {x : ℕ → α} {T : ℕ → ℕ} (hT : StrictMono T) {L : α} (hx : Filter.Tendsto x Filter.atTop (nhds L)) (g : ℕ → α) (hg : ∀ (k n : ℕ), n ∈ Set.Ico (T k) (T (k + 1)) → g n = x k) : Filter.Tendsto g Filter.atTop (nhds L)

theorem exists_increasing_sequence_with_property (M : ℕ → ℕ) (P : ℕ → ℕ → Prop) (hP : ∀ (k L : ℕ), ∃ n ≥ L, P k n) : ∃ (T : ℕ → ℕ), StrictMono T ∧ (∀ (k : ℕ), T k ≥ M k) ∧ ∀ (k : ℕ), ∃ n ∈ Set.Ico (T k) (T (k + 1)), P k n

theorem liminf_le_of_block_sequence_witnesses {α : Type u_1} (y : NNReal) (f : α → ℕ → ENNReal) (T : ℕ → ℕ) (hT : StrictMono T) (x g : ℕ → α) (hg : ∀ (k n : ℕ), n ∈ Set.Ico (T k) (T (k + 1)) → g n = x k) (hwit : ∀ (k : ℕ), ∃ n ∈ Set.Ico (T k) (T (k + 1)), f (x k) n ≤ ↑y + ↑(↑k + 1)⁻¹) : Filter.liminf (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem limsup_le_of_block_sequence_bound {α : Type u_1} (y : NNReal) (f : α → ℕ → ENNReal) (T : ℕ → ℕ) (hT : StrictMono T) (x g : ℕ → α) (hg : ∀ (k n : ℕ), n ∈ Set.Ico (T k) (T (k + 1)) → g n = x k) (hbound : ∀ (k n : ℕ), n ∈ Set.Ico (T k) (T (k + 1)) → f (x k) n ≤ ↑y + ↑(↑k + 1)⁻¹) : Filter.limsup (fun (n : ℕ) => f (g n) n) Filter.atTop ≤ ↑y

theorem exists_liminf_zero_of_forall_liminf_limsup_le_with_UB (y₁ y₂ : NNReal) (f₁ f₂ : NNReal → ℕ → ENNReal) {z : NNReal} (hz : 0 < z) (hf₁ : ∀ x > 0, Filter.liminf (f₁ x) Filter.atTop ≤ ↑y₁) (hf₂ : ∀ x > 0, Filter.limsup (f₂ x) Filter.atTop ≤ ↑y₂) : ∃ (g : ℕ → NNReal), (∀ (x : ℕ), g x > 0) ∧ (∀ (x : ℕ), g x < z) ∧ Filter.Tendsto g Filter.atTop (nhds 0) ∧ Filter.liminf (fun (n : ℕ) => f₁ (g n) n) Filter.atTop ≤ ↑y₁ ∧ Filter.limsup (fun (n : ℕ) => f₂ (g n) n) Filter.atTop ≤ ↑y₂

theorem extracted_limsup_inequality (z : ENNReal) (hz : z ≠ ⊤) (y x : ℕ → ENNReal) (h_lem5 : ∀ (n : ℕ), x n ≤ y n + z) : Filter.limsup (fun (n : ℕ) => x n / ↑n) Filter.atTop ≤ Filter.limsup (fun (n : ℕ) => y n / ↑n) Filter.atTop

theorem Filter.tendsto_sub_atTop_iff_nat {α : Type u_1} {f : ℕ → α} {l : Filter α} (k : ℕ) : Tendsto (fun (n : ℕ) => f (n - k)) atTop l ↔ Tendsto f atTop l

Like Filter.tendsto_add_atTop_iff_nat, but with nat subtraction.

theorem ENNReal.tendsto_sub_const_nhds_zero_iff {α : Type u_1} {l : Filter α} {f : α → ENNReal} {a : ENNReal} : Filter.Tendsto (fun (x : α) => f x - a) l (nhds 0) ↔ Filter.limsup f l ≤ a

Sort of dual to ENNReal.tendsto_const_sub_nhds_zero_iff. Takes a substantially different form though, since we don't actually have equality of the limits, or even the fact that the other one converges, which is why we need to use limsup.