estimate_10_1_4

lemma estimate_10_1_4 {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (hx : dist x x' ≤ r) :    (∫⁻ (y : X) in (ball x' r)ᶜ ∩ ball x (2*r), ‖K x' y * g y‖ₑ) ≤    2 ^ (a ^ 3 + 2 * 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 x    trans x ∈ (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 but for x'  trans C_K ↑a / volume (ball x' r) * (globalMaximalFunction volume 1 g x * volume (ball x' (4 * r)))  · apply mul_le_mul' le_rfl    trans ∫⁻ (a : X) in ball x' (4 * r), ‖g a‖ₑ    · apply lintegral_mono_set      trans ball x (2 * r)      · exact inter_subset_right      · exact ball_subset (by linarith)    rw [_laverage_mul_measure_ball]    apply mul_le_mul' ?_ le_rfl    exact laverage_le_globalMaximalFunction (by linarith)  nth_rw 2 [mul_comm]  rw [← mul_assoc]  apply mul_le_mul' ?_ le_rfl  trans C_K ↑a / volume (ball x' r) * ((defaultA a) ^ 2 * volume (ball x' r))  · exact mul_le_mul' le_rfl (measure_ball_four_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