czOperator_welldefined

lemma czOperator_welldefined {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (x : X) :    IntegrableOn (fun y => K x y * g y) (ball x r)ᶜ volume := by  let Kxg := fun y ↦ K x y * g y  have mKxg : AEStronglyMeasurable Kxg := by    have : Measurable (K x) := measurable_K_right x    fun_prop  have tmp_Kxg {M : ℝ≥0} : ∀ y, ¬‖Kxg y‖ ≤ M → y ∈ support Kxg := by    intro y    contrapose!    rw [notMem_support]    intro hy    rw [hy, norm_zero]    simp only [NNReal.zero_le_coe]  have bdd_Kxg : ∃ (M : ℝ), ∀ᵐ y ∂(volume.restrict ((ball x r)ᶜ ∩ support Kxg)), ‖Kxg y‖ ≤ M := by    obtain ⟨M, hM⟩ := czOperator_bound (K := K) hg hr x    use M    rw [ae_iff, Measure.restrict_apply₀']    · conv =>        arg 1; arg 2;        rw [← inter_assoc]        refine (left_eq_inter.mpr ?_).symm        exact inter_subset_left.trans <| setOf_subset.mpr tmp_Kxg      rw [← Measure.restrict_apply₀' (by measurability), ← ae_iff]      exact hM    · apply NullMeasurableSet.inter      · exact measurableSet_ball.compl.nullMeasurableSet      · exact mKxg.nullMeasurableSet_support  obtain ⟨M, hM⟩ := bdd_Kxg  apply IntegrableOn.of_inter_support measurableSet_ball.compl  apply Measure.integrableOn_of_bounded ?_ mKxg hM  apply ne_top_of_le_ne_top (hg.measure_support_lt.ne)  gcongr  trans support Kxg  · exact inter_subset_right  · exact support_mul_subset_right (K x) g