English
For f: Nat→α→ENNReal, the map n↦ iSup_{k} iSup_{x} f_k x is monotone in n.
Русский
Для f: Nat→α→ENNReal отображение монотонно по n.
LaTeX
$$$$ \\text{Monotone in } n: \\; n \\mapsto \\big( a \\mapsto iSup_{k} iSup_{x} f_k(a) \\big) \\text{ is monotone}. $$$$
Lean4
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right_of_ne_top`, which has no hypothesis on `μ` but requires finite `ν`. -/
theorem rnDeriv_smul_right_of_ne_top' (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ℝ≥0∞} (hr : r ≠ 0)
(hr_ne_top : r ≠ ∞) : ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ :=
by
have h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ :=
by
refine rnDeriv_smul_right' ν μ ?_
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
simp [hr, hr_ne_top]
rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top, ← ENNReal.toNNReal_inv, ENNReal.smul_def,
ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h
