integrableOn_K_mul_f

lemma integrableOn_K_mul_f {x' : X} (hf : BoundedCompactSupport f volume) {r : ℝ≥0∞} (hr : 0 < r) :    IntegrableOn (fun y ↦ K x' y * f y) (EAnnulus.ci x' r) := by  by_cases supp_f : (support f).Nonempty; swap  · simp [Function.support_eq_empty_iff.mp <| Set.not_nonempty_iff_eq_empty.mp supp_f]  by_cases r_top : r = ⊤  · simp [r_top]  have ⟨x'', hx''⟩ := supp_f  have ⟨C, hC⟩ := Metric.isBounded_iff.mp hf.isBoundedSupport  have : support (fun y ↦ f y * K x' y) ⊆ closedBall x' (dist x' x'' + C) := by    intro y hy    have : y ∈ support f := by contrapose! hy; simp [hy]    exact mem_closedBall'.mp <| (dist_triangle x' x'' y).trans <| add_le_add_right (hC hx'' this) _  simp_rw [mul_comm (K x' _), IntegrableOn, ← integrableOn_iff_integrable_of_support_subset this]  apply hf.restrict.restrict.integrable_mul  rw [Measure.restrict_restrict measurableSet_closedBall, inter_comm, ← IntegrableOn]  convert integrableOn_K_Icc (K := K) (R := dist x' x'' + C) (r.toReal_pos hr.ne.symm r_top) using 1  ext y  simp [edist_dist, dist_comm y, EAnnulus.ci, ENNReal.le_ofReal_iff_toReal_le r_top dist_nonneg]