estimate_10_1_2

lemma estimate_10_1_2 {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) :    (∫⁻ (y : X) in (ball x r)ᶜ ∩ ball x (2*r), ‖K x y * g y‖ₑ) ≤    2 ^ (a ^ 3 + a) * globalMaximalFunction volume 1 g x := by  simp only [enorm_mul]  trans ∫⁻ (y : X) in (ball x r)ᶜ ∩ ball x (2*r), C_K ↑a / volume (ball x r) * ‖g y‖ₑ  · apply setLIntegral_mono_ae (by fun_prop) (.of_forall _)    intro y    trans y ∈ (ball x r)ᶜ    · exact fun a ↦ mem_of_mem_inter_left a    exact fun h ↦ mul_le_mul' (enorm_K_le_ball_complement h) (by rfl)  rw [lintegral_const_mul'' _ hg.aemeasurable.restrict.enorm] -- LHS = 10.1.5  trans C_K a / volume (ball x r) * (globalMaximalFunction volume 1 g x * volume (ball x (2 * r)))  · gcongr    trans ∫⁻ (a : X) in ball x (2*r), ‖g a‖ₑ    · exact lintegral_mono_set inter_subset_right    rw [_laverage_mul_measure_ball]    gcongr    apply laverage_le_globalMaximalFunction    rw [dist_self]    exact mul_pos zero_lt_two hr  nth_rw 2 [mul_comm]  rw [← mul_assoc]  gcongr  trans C_K a / volume (ball x r) * (defaultA a * volume (ball x r))  · gcongr    apply measure_ball_two_le_same  -- Somehow simp doesn't do it  apply le_of_eq  nth_rw 2 [mul_comm]  rw [← mul_assoc, div_eq_mul_inv]  nth_rw 2 [mul_assoc]  simp_rw [mul_comm, ENNReal.mul_inv_cancel (measure_ball_pos volume x hr).ne.symm measure_ball_lt_top.ne, C_K]  norm_cast  ring