liminf_eq_ciSup_ciInf — Mathlib

English

A limsup expression with a basis again uses a conditional expression (ITE) to describe the exact form.

Русский

Выражение лимсуп через базис снова использует условие ITE.

LaTeX

$$limsup f v = if ∃ j, s j = ∅ then sInf univ else if ∀ j, ¬BddAbove (range (i ↦ f i)) then sInf ∅ else ⨅ j, ⨆ i, f i$$

Lean4

/-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are
not bounded below. -/
theorem liminf_eq_ciSup_ciInf {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)]
    [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty)
    (H : ∃ (j : Subtype p), BddBelow (range (fun (i : s j) ↦ f i))) :
    liminf f v = ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i := by
  classical
  rcases H with ⟨j0, hj0⟩
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j)
  have A :
    ⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i) = ⋃ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) :=
    by
    apply Subset.antisymm
    · apply iUnion_subset (fun j ↦ ?_)
      by_cases hj : j ∈ m
      · have : j = liminf_reparam f s p j := by simp only [m, liminf_reparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j
      · simp only [m, mem_setOf_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
        simp only [hj, empty_subset]
    · apply iUnion_subset (fun j ↦ ?_)
      exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminf_reparam f s p j)
  have B :
    ∀ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) = Iic (⨅ (i : s (liminf_reparam f s p j)), f i) :=
    by
    intro j
    apply (Iic_ciInf _).symm
    change liminf_reparam f s p j ∈ m
    by_cases Hj : j ∈ m
    · simpa only [m, liminf_reparam, if_pos Hj] using Hj
    · simp only [m, liminf_reparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m :=
        by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ | hZ
      · exact hZ
      · exact (hZ j0 hj0).elim
  simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]

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