English
For i, f, a with hf measurable, the supremum over n of approx i f n evaluated at a equals the supremum over k with i_k ≤ f(a) of i_k.
Русский
Пусть i и f удовлетворяют меримости; тогда sup_n (approx i f n)(a) = sup_{k: i_k ≤ f(a)} i_k.
LaTeX
$$$ \bigsqcup_{n} (approx\ i\ f\ n)(a) = \bigsqcup_{k\, :\, i_k \le f(a)} i_k $$$
Lean4
theorem iSup_approx_apply [TopologicalSpace β] [CompleteLattice β] [OrderClosedTopology β] [Zero β] [MeasurableSpace β]
[OpensMeasurableSpace β] (i : ℕ → β) (f : α → β) (a : α) (hf : Measurable f) (h_zero : (0 : β) = ⊥) :
⨆ n, (approx i f n : α →ₛ β) a = ⨆ (k) (_ : i k ≤ f a), i k :=
by
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun k => iSup_le fun hk => ?_)
· rw [approx_apply a hf, h_zero]
refine Finset.sup_le fun k _ => ?_
split_ifs with h
· exact le_iSup_of_le k (le_iSup (fun _ : i k ≤ f a => i k) h)
· exact bot_le
· refine le_iSup_of_le (k + 1) ?_
rw [approx_apply a hf]
have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)
refine le_trans (le_of_eq ?_) (Finset.le_sup this)
rw [if_pos hk]
