English
A function is integrable with respect to the counting measure if and only if its norm is summable.
Русский
Функция интегрируема относительно счетной меры тогда и только тогда, когда её норма суммируема.
LaTeX
$$Integrable f Measure.count ↔ Summable (‖f‖)$$
Lean4
/-- A function is integrable for the counting measure iff its norm is summable. -/
theorem integrable_count_iff : Integrable f Measure.count ↔ Summable (‖f ·‖) := by
-- Note: this proof would be much easier if we assumed `SecondCountableTopology G`. Without
-- this we have to justify the claim that `f` lands a.e. in a separable subset, which is true
-- (because summable functions have countable range) but slightly tedious to check.
rw [Integrable, hasFiniteIntegral_count_iff, and_iff_right_iff_imp]
intro hs
have hs' : (Function.support f).Countable := by
simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero] using hs.countable_support
letI : MeasurableSpace β := borel β
haveI : BorelSpace β := ⟨rfl⟩
refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩
· refine (measurable_zero.measurable_of_countable_ne ?_).aemeasurable
simpa only [Ne, Pi.zero_apply, eq_comm, Function.support] using hs'
· refine ⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩
suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
(((hs'.image f).union (countable_singleton 0)).mono this).isSeparable
grind [Function.mem_support]
