liminf_reparam — Mathlib

English

Dually, limsup can be written as an infimum of sups across a basis.

Русский

Дуально лимсуп записывается как инфimum уплотнений над базисом.

LaTeX

$$limsup f v = ⨅ j, ⨆ i, f i$$

Lean4

/-- Given an indexed family of sets `s j` over `j : Subtype p` and a function `f`, then
`liminf_reparam j` is equal to `j` if `f` is bounded below on `s j`, and otherwise to some
index `k` such that `f` is bounded below on `s k` (if there exists one).
To ensure good measurability behavior, this index `k` is chosen as the minimal suitable index.
This function is used to write down a liminf in a measurable way,
in `Filter.HasBasis.liminf_eq_ciSup_ciInf` and `Filter.HasBasis.liminf_eq_ite`. -/
noncomputable def liminf_reparam (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)]
    [Nonempty (Subtype p)] (j : Subtype p) : Subtype p :=
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  let g : ℕ → Subtype p := (exists_surjective_nat _).choose
  have Z : ∃ n, g n ∈ m ∨ ∀ j, j ∉ m := by
    by_cases H : ∃ j, j ∈ m
    · rcases H with ⟨j, hj⟩
      rcases (exists_surjective_nat (Subtype p)).choose_spec j with ⟨n, rfl⟩
      exact ⟨n, Or.inl hj⟩
    · push_neg at H
      exact ⟨0, Or.inr H⟩
  if j ∈ m then j else g (Nat.find Z)

Похожие утверждения