tendsto_carlesonOperatorIntegrand_of_dominated_convergence

lemma tendsto_carlesonOperatorIntegrand_of_dominated_convergence  (hR₁ : 0 < R₁)  {l : Filter ℕ} [l.IsCountablyGenerated]  {F : ℕ → X → ℂ} (bound : X → ℝ)  (hF_meas : ∀ᶠ (n : ℕ) in l, AEStronglyMeasurable (F n))  (h_bound : ∀ᶠ (n : ℕ) in l, ∀ᵐ (a : X), ‖F n a‖ ≤ bound a)  (bound_integrable : IntegrableOn (fun y ↦ bound y) (Annulus.oo x R₁ R₂) volume)  (h_lim : ∀ᵐ (a : X), Filter.Tendsto (fun (n : ℕ) => F n a) l (nhds (f a))) :    Filter.Tendsto (fun (n : ℕ) => carlesonOperatorIntegrand K θ R₁ R₂ (F n) x) l      (nhds (carlesonOperatorIntegrand K θ R₁ R₂ f x)) := by  unfold carlesonOperatorIntegrand  set bound' := (fun y ↦ ‖K x y * bound y * exp (I * θ y)‖)  apply MeasureTheory.tendsto_integral_filter_of_dominated_convergence (fun y ↦ ‖K x y * bound y * exp (I * θ y)‖)  · apply hF_meas.mp    have : Measurable (K x) := measurable_K_right x    filter_upwards with n hFn using by fun_prop  · apply h_bound.mp    apply Eventually.of_forall    intro n hn    simp only [Complex.norm_mul, norm_exp_I_mul_ofReal, mul_one, norm_real,      Real.norm_eq_abs]    apply ae_restrict_le    apply hn.mp    filter_upwards with y hy    gcongr    exact le_trans hy (le_abs_self _)  · exact (integrableOn_coi_inner_annulus' bound_integrable.ofReal hR₁).norm  · apply ae_restrict_le    apply h_lim.mp    filter_upwards with y hy    exact Filter.Tendsto.mul (Filter.Tendsto.mul tendsto_const_nhds hy) tendsto_const_nhds