czOperatorBound_inner_le

lemma czOperatorBound_inner_le (ha : 4 ≤ a) (hX : GeneralCase f (α' a α)) {i : ℕ} :    ∫⁻ x in (Ω f (α' a α))ᶜ, ((3 * czRadius hX i).toNNReal / edist x (czCenter hX i)) ^ (a : ℝ)⁻¹ /      volume (ball x (dist x (czCenter hX i))) ≤ 2 ^ (3 * a) := by  set r := 3 * czRadius hX i  set c := czCenter hX i  rcases le_or_gt r 0 with hr | hr  · simp_rw [Real.toNNReal_of_nonpos hr, coe_zero, ENNReal.zero_div]    rw [ENNReal.zero_rpow_of_pos (by rw [inv_pos, Nat.cast_pos]; exact zero_lt_four.trans_le ha)]    simp_rw [ENNReal.zero_div, lintegral_zero]; exact zero_le  calc    _ ≤ ∫⁻ x in (czBall6 hX i)ᶜ,        (r.toNNReal / edist x c) ^ (a : ℝ)⁻¹ / volume (ball x (dist x c)) := by      apply lintegral_mono_set; simp_rw [compl_subset_compl, Ω, hX, dite_true]      exact subset_iUnion ..    _ ≤ ∫⁻ x in (czBall6 hX i)ᶜ,        (r.toNNReal / edist x c) ^ (a : ℝ)⁻¹ / (volume (ball c (dist x c)) / 2 ^ a) := by      gcongr with x; apply div_le_of_le_mul      calc        _ ≤ volume (ball x (2 * dist x c)) :=          measure_mono (ball_subset_ball' (by rw [dist_comm, two_mul]))        _ ≤ _ := by          rw [mul_comm _ (2 ^ a)]          convert measure_ball_two_le_same (μ := volume) x (dist x c)          unfold defaultA; norm_cast    _ = 2 ^ a * ∫⁻ x in (czBall6 hX i)ᶜ,        (r.toNNReal / edist x c) ^ (a : ℝ)⁻¹ / volume (ball c (dist x c)) := by      rw [← lintegral_const_mul' _ _ (by finiteness)]; congr! 2 with x      rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (.inl (by finiteness)) (.inl (by positivity)),        ENNReal.mul_comm_div]    _ ≤ 2 ^ a * ∫⁻ x in ⋃ n, ball c (2 ^ (n + 1) * r) \ ball c (2 ^ n * r),        (r.toNNReal / edist x c) ^ (a : ℝ)⁻¹ / volume (ball c (dist x c)) := by      gcongr _ * ?_; refine lintegral_mono_set fun x mx ↦ ?_      rw [czBall6, mem_compl_iff, mem_ball, not_lt, show (6 : ℝ) = 2 * 3 by norm_num,        mul_assoc] at mx      change 2 * r ≤ dist x c at mx      rw [mem_iUnion]; use ⌊Real.logb 2 (dist x c / r)⌋₊; simp_rw [Set.mem_sdiff, mem_ball, not_lt]      have dxcpos : 0 < dist x c := lt_of_lt_of_le (by positivity) mx      have dxceq : dist x c = 2 ^ (Real.logb 2 (dist x c / r)) * r := by        rw [Real.rpow_logb zero_lt_two (by norm_num) (by positivity), div_mul_cancel₀ _ hr.ne']      constructor      · nth_rw 1 [dxceq, ← Real.rpow_natCast]; push_cast; gcongr        exact Real.rpow_lt_rpow_of_exponent_lt one_lt_two (Nat.lt_floor_add_one _)      · nth_rw 2 [dxceq]; rw [← Real.rpow_natCast]; gcongr        · exact one_le_two        · refine Nat.floor_le (Real.logb_nonneg one_lt_two ((one_le_div₀ hr).mpr ?_))          linarith only [hr, mx]    _ ≤ 2 ^ a * ∑' n, ∫⁻ x in ball c (2 ^ (n + 1) * r) \ ball c (2 ^ n * r),        (r.toNNReal / edist x c) ^ (a : ℝ)⁻¹ / volume (ball c (dist x c)) := by      gcongr; exact lintegral_iUnion_le _ _    _ ≤ 2 ^ a * ∑' n, ∫⁻ x in ball c (2 ^ (n + 1) * r) \ ball c (2 ^ n * r),        (2 ^ n)⁻¹ ^ (a : ℝ)⁻¹ / volume (ball c (2 ^ n * r)) := by      gcongr 2 ^ a * ∑' n, ?_ with n      refine setLIntegral_mono' (measurableSet_ball.diff measurableSet_ball) fun x mx ↦ ?_      simp_rw [Set.mem_sdiff, mem_ball, not_lt] at mx      gcongr      · change ENNReal.ofReal r / _ ≤ _        have dxcpos : 0 < dist x c := lt_of_lt_of_le (by positivity) mx.2        rw [le_inv_iff_mul_le, mul_comm, ← mul_div_assoc, show 2 = ENNReal.ofReal 2 by simp,          ← ofReal_pow zero_le_two, ← ofReal_mul (by positivity), edist_dist,          ← ofReal_div_of_pos dxcpos, ← ofReal_one]        apply ofReal_le_ofReal; rw [div_le_one dxcpos]; exact mx.2      · exact mx.2    _ = 2 ^ a * ∑' n : ℕ, 2 ^ (-n / a : ℝ) *        (volume (ball c (2 ^ (n + 1) * r) \ ball c (2 ^ n * r)) / volume (ball c (2 ^ n * r))) := by      congr! 3 with n; rw [setLIntegral_const, ← ENNReal.mul_div_right_comm, ← mul_div_assoc]      congr 2; rw [← rpow_natCast, ← rpow_neg, ← rpow_mul, ← div_eq_mul_inv]    _ ≤ 2 ^ a * ∑' n : ℕ, 2 ^ (-n / a : ℝ) * 2 ^ a := by      gcongr with n; apply div_le_of_le_mul      calc        _ ≤ volume (ball c (2 * (2 ^ n * r))) := by          rw [← mul_assoc 2, ← pow_succ']; exact measure_mono sdiff_subset        _ ≤ _ := by          convert measure_ball_two_le_same (μ := volume) c (2 ^ n * r)          unfold defaultA; norm_cast    _ ≤ 2 ^ a * 2 ^ a * 2 ^ a := by      rw [ENNReal.tsum_mul_right, ← mul_assoc]; gcongr      rw [← rpow_natCast]; exact geometric_series_estimate (by norm_cast; lia)    _ = _ := by norm_cast; ring