Lean: bound ∫⁻ of a radial function by shells ⌈‖x‖/r⌉₊ = k and a geometric series
To show ∫⁻ ofReal(exp(c‖x‖)) dμ < ⊤ from a tail bound, partition space by the measurable map κ x = ⌈‖x‖/r⌉₊ (Nat.measurable_ceil, needs import Mathlib.MeasureTheory.Function.Floor). The sets κ⁻¹'{k} are measurable, pairwise disjoint via (Set.disjoint_singleton.2 hij).preimage _, and their union is univ by ext; simp. Then rw [hU, Measure.restrict_univ], lintegral_iUnion, bound each term with setLIntegral_mono measurable_const + setLIntegral_const, and finish with ENNReal.tsum_le_tsum, ENNReal.tsum_mul_left, ENNReal.tsum_geometric and ENNReal.inv_lt_top.2 (tsub_pos_iff_lt.2 (ENNReal.ofReal_lt_one.2 hρ)). On a shell, Nat.le_ceil gives the upper bound and Nat.ceil_le (by contradiction + omega) the lower one. Also: MeasurableSet.const_smul₀ needs MeasurableSingletonClass; const_smul_of_ne_zero only needs MeasurableConstSMul.
Checked on Mathlib v4.35.0 and v4.36.0-rc2: every name exists.
Nat.measurable_ceilis in Mathlib/MeasureTheory/Function/Floor.lean and#checkworks with only that import. The instance remark is right:MeasurableSet.const_smul₀takes[MulActionWithZero G₀ α] [MeasurableConstSMul G₀ α] [MeasurableSingletonClass α]and works for anya, whileMeasurableSet.const_smul_of_ne_zerotakes[MulAction G₀ α] [MeasurableConstSMul G₀ α]plusha : a ≠ 0. Version caveat: on v4.36.0-rc2ENNReal.tsum_le_tsumis deprecated ('Use tsum_le_tsum instead'; the root version takesf ≤ gand still acceptsh : ∀ a, f a ≤ g a). It still compiles with a warning.ENNReal.tsum_mul_leftandENNReal.tsum_geometricare not deprecated on rc2.