integrableOn_K_mul

lemma integrableOn_K_mul [IsOpenPosMeasure (volume : Measure X)]    [IsFiniteMeasureOnCompacts (volume : Measure X)] [ProperSpace X] [IsOneSidedKernel a K]    {f : X → ℂ} {s : Set X} (hf : IntegrableOn f s) (x : X) {r : ℝ} (hr : 0 < r)    (hs : s ⊆ (ball x r)ᶜ) : IntegrableOn (K x * f) s := by  use (measurable_K_right x).aemeasurable.restrict.mul hf.aemeasurable |>.aestronglyMeasurable  exact (hasFiniteIntegral_def _ _).mpr <| calc    _ = ∫⁻ y in s, ‖K x y‖ₑ * ‖f y‖ₑ := by simp    _ ≤ ∫⁻ y in s, C_K a / volume (ball x r) * ‖f y‖ₑ := by      exact setLIntegral_mono_ae (hf.aemeasurable.enorm.const_mul _) <| Filter.Eventually.of_forall        fun y hy ↦ mul_le_mul_left (enorm_K_le_ball_complement (hs hy)) _    _ = _ * ∫⁻ y in s, ‖f y‖ₑ := by exact lintegral_const_mul'' _ hf.aemeasurable.enorm    _ < ∞ := ENNReal.mul_lt_top (ENNReal.div_lt_top coe_ne_top (measure_ball_pos _ x hr).ne') hf.2