edist_carlesonOperatorIntegrand_le

lemma edist_carlesonOperatorIntegrand_le    {R₁ R₂ : ℝ≥0} (mf : Measurable f) (nf : (‖f ·‖) ≤ 1) (hR₁ : 0 < R₁) :    edist (carlesonOperatorIntegrand K θ R₁ R₂ f x) (carlesonOperatorIntegrand K ϑ R₁ R₂ f x) ≤    C3_0_1 a R₁ R₂ * edist_{x, dist o x + R₂} θ ϑ := by  rcases le_or_gt R₂ R₁ with hR₂ | hR₂  · iterate 2 rw [carlesonOperatorIntegrand, Annulus.oo_eq_empty (by simp [hR₂]), setIntegral_empty]    rw [edist_self]; exact zero_le  calc    _ = ‖∫ y in Annulus.oo x R₁ R₂, K x y * f y * (exp (I * θ y) - exp (I * ϑ y))‖ₑ := by      rw [edist_eq_enorm_sub, carlesonOperatorIntegrand, carlesonOperatorIntegrand, ← integral_sub]      rotate_left      · exact integrableOn_coi_inner_annulus mf nf hR₁      · exact integrableOn_coi_inner_annulus mf nf hR₁      congr! 3 with y; rw [mul_sub]    _ ≤ ∫⁻ y in Annulus.oo x R₁ R₂, ‖K x y‖ₑ * ‖f y‖ₑ * ‖exp (I * θ y) - exp (I * ϑ y)‖ₑ := by      simp_rw [← enorm_mul]; exact enorm_integral_le_lintegral_enorm _    _ ≤ ∫⁻ y in Annulus.oo x R₁ R₂, C_K a / vol x y * edist_{x, dist o x + R₂} θ ϑ := by      refine setLIntegral_mono' Annulus.measurableSet_oo fun y my ↦ ?_      rw [mul_assoc]; refine mul_le_mul' (enorm_K_le_vol_inv _ _) ?_      rw [← one_mul (edist_{x, dist o x + R₂} θ ϑ)]; gcongr      · rw [← enorm_norm, ← enorm_one (G := ℝ)]; exact Real.enorm_le_enorm (norm_nonneg _) (nf y)      · rw [edist_dist, le_ofReal_iff_toReal_le (by finiteness) dist_nonneg, toReal_enorm]        calc          _ = ‖exp (I * (θ y - ϑ y - θ o + ϑ o : ℝ)) - 1‖ := by            rw [cancelPt_eq_zero, sub_zero, cancelPt_eq_zero, add_zero, Complex.ofReal_sub,              ← mul_one ‖_ - 1‖, ← norm_exp_I_mul_ofReal (ϑ y), ← norm_mul, sub_one_mul,              ← Complex.exp_add, ← mul_add, sub_add_cancel]          _ ≤ ‖θ y - ϑ y - θ o + ϑ o‖ := Real.norm_exp_I_mul_ofReal_sub_one_le          _ ≤ _ := by            rw [Annulus.oo, mem_setOf, mem_Ioo] at my            apply oscillation_le_cdist            · rw [mem_ball']; exact my.2.trans_le (le_add_of_nonneg_left dist_nonneg)            · rw [mem_ball, lt_add_iff_pos_right]; exact hR₁.trans hR₂    _ = C_K a * edist_{x, dist o x + R₂} θ ϑ * ∫⁻ y in Annulus.oo x R₁ R₂, (vol x y)⁻¹ := by      simp_rw [ENNReal.div_eq_inv_mul]      iterate 2 rw [lintegral_mul_const' _ _ (by finiteness)]      rw [mul_rotate]    _ ≤ C_K a * edist_{x, dist o x + R₂} θ ϑ * ↑((2 * R₂ / R₁) ^ a) := by      gcongr; exact lintegral_inv_vol_le hR₁ hR₂    _ = _ := by      rw [← mul_rotate, ← coe_mul, mul_comm (_ ^ _), C3_0_1, C_K, ← Nat.cast_pow,        NNReal.rpow_natCast]