enorm_setIntegral_annulus_le

lemma enorm_setIntegral_annulus_le {x : X} {R₁ R₂ : ℝ} {s : ℤ} (nf : (‖f ·‖) ≤ F.indicator 1) :    ‖∫ y in Annulus.oo x R₁ R₂, Ks s x y * f y * exp (I * Q x y)‖ₑ ≤    C2_1_3 a * globalMaximalFunction volume 1 (F.indicator (1 : X → ℝ)) x := by  calc    _ ≤ ∫⁻ y in Annulus.oo x R₁ R₂, ‖Ks s x y‖ₑ * ‖f y‖ₑ * ‖exp (I * Q x y)‖ₑ := by      simp_rw [← enorm_mul]; exact enorm_integral_le_lintegral_enorm _    _ = ∫⁻ y in Annulus.oo x R₁ R₂ ∩ ball x (D ^ s), ‖Ks s x y‖ₑ * ‖f y‖ₑ := by      simp_rw [enorm_exp_I_mul_ofReal, mul_one]      rw [← lintegral_inter_add_sdiff (B := ball x (D ^ s)) _        (Annulus.oo x R₁ R₂) measurableSet_ball]      conv_rhs => rw [← add_zero (lintegral ..)]      congr 1      refine setLIntegral_eq_zero (Annulus.measurableSet_oo.diff measurableSet_ball) fun y my ↦ ?_      suffices Ks s x y = 0 by rw [this, enorm_zero, zero_mul, Pi.zero_apply]      contrapose! my; replace my := dist_mem_Ioo_of_Ks_ne_zero my      rw [Set.mem_sdiff, not_and_or, not_not]; right      rw [mem_Ioo, ← mem_ball'] at my; exact (ball_subset_ball (half_le_self (by positivity))) my.2    _ ≤ ∫⁻ y in ball x (D ^ s), ‖Ks s x y‖ₑ * ‖f y‖ₑ := lintegral_mono_set inter_subset_right    _ ≤ ∫⁻ y in ball x (D ^ s),        C2_1_3 a / volume (ball x (D ^ s)) * ‖F.indicator (1 : X → ℝ) y‖ₑ := by      gcongr with y      · exact enorm_Ks_le      · simp_rw [enorm_le_iff_norm_le, norm_indicator_eq_indicator_norm, Pi.one_apply, norm_one]        exact nf y    _ = C2_1_3 a * ⨍⁻ y in ball x (D ^ s), ‖F.indicator (1 : X → ℝ) y‖ₑ ∂volume := by      rw [lintegral_const_mul']; swap      · exact div_ne_top coe_ne_top (measure_ball_pos _ x (defaultD_pow_pos a _)).ne'      rw [setLAverage_eq, div_eq_mul_inv, ENNReal.div_eq_inv_mul, mul_assoc]    _ ≤ _ := by      gcongr; exact laverage_le_globalMaximalFunction (by rw [dist_self, defaultD]; positivity)