English
If κ is a finite kernel and f is everywhere finite, then the kernel with density κ f is s-finite.
Русский
Если κ – конечное ядро, а функция f(a,b) конечна для всех a,b, то ядро с плотностью κ f является s-финитным.
LaTeX
$$$\\operatorname{IsSFiniteKernel}\\bigl(\\mathrm{withDensity}(\\kappa, f)\\bigr)$$$
Lean4
/-- Auxiliary lemma for `IsSFiniteKernel.withDensity`.
If a kernel `κ` is finite, then `withDensity κ f` is s-finite. -/
theorem isSFiniteKernel_withDensity_of_isFiniteKernel (κ : Kernel α β) [IsFiniteKernel κ]
(hf_ne_top : ∀ a b, f a b ≠ ∞) : IsSFiniteKernel (withDensity κ f) := by
-- We already have that for `f` bounded from above and a `κ` a finite kernel,
-- `withDensity κ f` is finite. We write any function as a countable sum of bounded
-- functions, and decompose an s-finite kernel as a sum of finite kernels. We then use that
-- `withDensity` commutes with sums for both arguments and get a sum of finite kernels.
by_cases hf : Measurable (Function.uncurry f)
swap; · rw [withDensity_of_not_measurable _ hf]; infer_instance
let fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (n + 1) - min (f a b) n
have h_le : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ n :=
by
intro a b n hn
have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn
rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this
· refine this.trans (le_of_eq ?_)
rw [ENNReal.ofReal_natCast]
· norm_cast
exact zero_le _
have h_zero : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0 :=
by
intro a b n hn
suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by simp_rw [fs, this.1, this.2, tsub_self (f a b)]
exact ⟨min_eq_left ((h_le a b n hn).trans (le_add_of_nonneg_right zero_le_one)), min_eq_left (h_le a b n hn)⟩
have hf_eq_tsum : f = ∑' n, fs n :=
by
have h_sum_a : ∀ a, Summable fun n => fs n a :=
by
refine fun a => Pi.summable.mpr fun b => ?_
suffices ∀ n, n ∉ Finset.range ⌈(f a b).toReal⌉₊ → fs n a b = 0 from summable_of_ne_finset_zero this
intro n hn_notMem
rw [Finset.mem_range, not_lt] at hn_notMem
exact h_zero a b n hn_notMem
ext a b : 2
rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a), ENNReal.tsum_eq_liminf_sum_nat]
have h_finset_sum : ∀ n, ∑ i ∈ Finset.range n, fs i a b = min (f a b) n := fun n ↦ by
induction n with
| zero => simp
| succ n hn =>
rw [Finset.sum_range_succ, hn]
simp [fs]
simp_rw [h_finset_sum]
refine (Filter.Tendsto.liminf_eq ?_).symm
refine Filter.Tendsto.congr' ?_ tendsto_const_nhds
rw [Filter.EventuallyEq, Filter.eventually_atTop]
exact ⟨⌈(f a b).toReal⌉₊, fun n hn => (min_eq_left (h_le a b n hn)).symm⟩
rw [hf_eq_tsum, withDensity_tsum _ fun n : ℕ => _]
swap; · fun_prop
refine isSFiniteKernel_sum (hκs := fun n => ?_)
suffices IsFiniteKernel (withDensity κ (fs n)) by infer_instance
refine
isFiniteKernel_withDensity_of_bounded _ (ENNReal.coe_ne_top : ↑n + 1 ≠ ∞) fun a b =>
?_
-- After https://github.com/leanprover/lean4/pull/2734, we need to do beta reduction before `norm_cast`
beta_reduce
norm_cast
calc
fs n a b ≤ min (f a b) (n + 1) := tsub_le_self
_ ≤ n + 1 := (min_le_right _ _)
_ = ↑(n + 1) := by norm_cast