English
For a sequence f_n with measurable properties and almost everywhere monotone, the equality ∫ iInf f = iInf ∫ f holds under finiteness at 0.
Русский
При измеримой последовательности f_n с почти везде монотонностью выполняется ∫ iInf f = iInf ∫ f при конечности на нуле.
LaTeX
$$$(h\\_meas : ∀ n, AEMeasurable (f_n) μ) \\rightarrow (h\\_anti : ∀ᵐ a, Antitone (fun i => f_i a)) \\rightarrow (h\\_fin : ∫⁻ a, f_0 a ∂μ ≠ ∞) \\Rightarrow ∫⁻ a, iInf n, f_n a ∂μ = iInf n, ∫⁻ a, f_n a ∂μ$$$
Lean4
theorem lintegral_iInf' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AEMeasurable (f n) μ)
(h_anti : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) (h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) :
∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ :=
by
simp_rw [← iInf_apply]
let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Antitone f'
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_anti
have h_ae_seq_mono : Antitone (aeSeq h_meas p) := by
intro n m hnm x
by_cases hx : x ∈ aeSeqSet h_meas p
· exact aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm
· simp only [aeSeq, hx, if_false]
exact le_rfl
rw [lintegral_congr_ae (aeSeq.iInf h_meas hp).symm]
simp_rw [iInf_apply]
rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono]
· congr
exact funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n)
· rwa [lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)]
