estimate_10_1_3

lemma estimate_10_1_3 (ha : 4 ≤ a) {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (hx : dist x x' ≤ r) :    ‖∫ (y : X) in (ball x (2*r))ᶜ, K x y * g y - K x' y * g y‖ₑ ≤    2 ^ (a ^ 3 + 2 * a) * globalMaximalFunction volume 1 g x := by  simp_rw [← mul_sub_right_distrib]  trans ∫⁻ (y : X) in (ball x (2*r))ᶜ, ‖(K x y - K x' y) * g y‖ₑ  · apply enorm_integral_le_lintegral_enorm  simp only [enorm_mul]  trans ∫⁻ (y : X) in (ball x (2*r))ᶜ, ((edist x x' / edist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y)) * ‖g y‖ₑ  · apply setLIntegral_mono_ae (by fun_prop) (.of_forall _)    intro y h    refine mul_le_mul' (enorm_K_sub_le' ?_) (by rfl)    trans 2 * r    · gcongr    rw [mem_compl_iff, mem_ball, dist_comm] at h    exact le_of_not_gt h  let dom_i (i : ℕ) := Annulus.co x (2 ^ (i + 1) * r) (2 ^ (i + 2) * r)  have rw_dom : (ball x (2*r))ᶜ = ⋃ (i : ℕ) , dom_i i:= by    have := Annulus.iUnion_co_map_succ_eq_ci (x := x) (f := fun i ↦ 2 ^ (i + 1) * r)    simp only [Nat.succ_eq_succ, Nat.succ_eq_add_one, Nat.add_assoc] at this    rw [this]    · have : 2 * r = 2 ^ (0 + 1) * r := by ring      rw [this, Annulus.ci_eq, Nat.bot_eq_zero]    · intro n      gcongr <;> simp    · apply Filter.not_bddAbove_of_tendsto_atTop (l := Filter.atTop)      apply Filter.tendsto_atTop_atTop_of_monotone      · exact (pow_right_mono₀ Nat.one_le_ofNat).comp Order.succ_mono|>.mul_const (le_of_lt hr)      intro b      use Nat.ceil (b / r)      rw [← div_le_iff₀ hr]      trans (Nat.ceil (b / r) : ℝ)      · apply Nat.le_ceil      · norm_cast        trans Nat.ceil (b / r) + 1        · exact Nat.le_add_right ⌈b / r⌉₊ 1        · exact le_of_lt (Nat.lt_pow_self (le_refl 2))  trans ∑' (i : ℕ), ∫⁻ (y : X) in dom_i i, ((edist x x' / edist x y) ^ (a : ℝ)⁻¹ * (C_K a / vol x y)) * ‖g y‖ₑ  · rw [rw_dom]    apply lintegral_iUnion_le  -- Writing negative powers as positive powers of 1/2 to enable working with i : ℕ instead of -i : ℤ  trans ∑' (i : ℕ), 2 ^ (a ^ 3 + a) * (1 / (2 : ℝ≥0) ) ^ ((i + 1) * (a : ℝ)⁻¹) * globalMaximalFunction volume 1 g x  · apply Summable.tsum_le_tsum    case hf | hg => apply ENNReal.summable    intro i    have est_edist : ∀y ∈ dom_i i, (edist x x' / edist x y) ≤ (1 / (2 : ℝ≥0)) ^ (i + 1) := by      unfold dom_i Annulus.co      simp_rw [← Ico_def, mem_setOf]      intro y hdist      trans edist x x' / (2 ^ (i + 1) * r.toNNReal)      · gcongr        rw [edist_dist, ENNReal.le_ofReal_iff_toReal_le]        case ha => norm_cast; apply coe_ne_top        case hb => exact dist_nonneg        simp_rw [toReal_mul, toReal_pow, toReal_ofNat, coe_toReal, Real.coe_toNNReal', max_eq_left hr.le, hdist.left]      rw [ENNReal.div_le_iff_le_mul]      case hb0 => right; apply pow_ne_top; simp      case hbt => left; exact (mul_ne_top (pow_ne_top ofNat_ne_top) coe_ne_top)      rw [← mul_assoc, pow_mul_pow_eq_one]      case a =>        simp only [coe_ofNat, one_div]        apply ENNReal.inv_mul_cancel <;> simp      simp only [one_mul, edist_le_coe, nndist_dist]      exact Real.toNNReal_le_toNNReal hx    have est_vol : ∀y ∈ dom_i i, vol x y ≥ volume (ball x (2 ^ (i + 1) * r)) := by      unfold dom_i Annulus.co      simp_rw [← Ico_def, mem_setOf]      apply fun y h ↦ measure_mono (ball_subset_ball h.left)    trans ∫⁻ (y : X) in dom_i i, (1 / (2 : ℝ≥0)) ^ ((i + 1) * (a : ℝ)⁻¹) * (C_K a / volume (ball x (2 ^ (i + 1) * r))) * ‖g y‖ₑ    · apply setLIntegral_mono_ae (by fun_prop) (.of_forall _)      intro y hy      gcongr      · rw [rpow_mul]        apply rpow_le_rpow _ (by positivity)        · apply (est_edist y hy).trans_eq          simp [rpow_add, rpow_natCast, pow_succ]      · exact est_vol y hy    rw [lintegral_const_mul'' _ hg.aemeasurable.restrict.enorm]    trans (1 / (2 : ℝ≥0)) ^ ((i + 1) * (a : ℝ)⁻¹) * (C_K ↑a / volume (ball x (2 ^ (i + 1) * r))) *        ∫⁻ (y : X) in ball x (2 ^ (i + 2) * r), ‖g y‖ₑ    · gcongr _ * ?_      apply lintegral_mono_set      unfold dom_i      rw [Annulus.co_eq]      exact inter_subset_left    rw [_laverage_mul_measure_ball]    nth_rw 5 [mul_comm]    rw [← mul_assoc]    trans (1 / (2 : ℝ≥0)) ^ ((i + 1) * (a : ℝ)⁻¹) * (C_K ↑a / volume (ball x (2 ^ (i + 1) * r))) *        volume (ball x (2 ^ (i + 2) * r)) * globalMaximalFunction volume 1 g x    · apply mul_le_mul'      case h₁ => rfl      apply laverage_le_globalMaximalFunction      simp only [dist_self, Nat.ofNat_pos, pow_pos, mul_pos_iff_of_pos_left, hr]    apply mul_le_mul' _ (by rfl)    rw [mul_assoc, mul_comm]    apply mul_le_mul' _ (by rfl)    trans C_K a / volume (ball x (2 ^ (i + 1) * r)) * (defaultA a * volume (ball x (2 ^ (i + 1) * r)))    · gcongr      rw [pow_succ]      nth_rw 2 [mul_comm]      rw [mul_assoc]      apply measure_ball_two_le_same    apply le_of_eq    rw [div_eq_mul_inv]    nth_rw 4 [mul_comm]    rw [mul_assoc]    nth_rw 2 [← mul_assoc]    nth_rw 3 [mul_comm]    rw [ENNReal.mul_inv_cancel (measure_ball_pos volume x (by positivity)).ne.symm measure_ball_lt_top.ne]    simp_rw [C_K, defaultA, one_mul, pow_add]    norm_cast  have : (2 : ℝ≥0∞) ^ (a ^ 3 + 2 * a) = 2 ^ (a ^ 3 + a) * 2 ^ a := by ring  rw [ENNReal.tsum_mul_right, ENNReal.tsum_mul_left, this]  gcongr  simp_rw [coe_ofNat, one_div, inv_rpow, ← rpow_neg, ← div_eq_mul_inv]  trans ∑' (i : ℕ), 2 ^ (-i / (a : ℝ))  · apply Summable.tsum_le_tsum    case hf | hg => apply ENNReal.summable    intro i    apply rpow_le_rpow_of_exponent_le Nat.one_le_ofNat    rw [neg_div, neg_le_neg_iff, div_le_div_iff_of_pos_right (by positivity)]    simp only [le_add_iff_nonneg_right, zero_le_one]  rw [← rpow_natCast]  exact geometric_series_estimate (by norm_cast; lia)