linearizedCarlesonOperator_le_liminf_linearizedCarlesonOperator_of_tendsto

lemma linearizedCarlesonOperator_le_liminf_linearizedCarlesonOperator_of_tendsto  {Q : X → Θ X}  {l : Filter ℕ} [l.IsCountablyGenerated] [l.NeBot]  {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 : LocallyIntegrable bound)  (h_lim : ∀ᵐ (a : X), Filter.Tendsto (fun (n : ℕ) => F n a) l (nhds (f a))) :      linearizedCarlesonOperator Q K f x ≤ Filter.liminf (fun n ↦ linearizedCarlesonOperator Q K (F n) x) l := by  unfold linearizedCarlesonOperator  apply le_trans _ Filter.iSup_liminf_le_liminf_iSup  gcongr with R₁  apply le_trans _ Filter.iSup_liminf_le_liminf_iSup  gcongr with R₂  simp only [iSup_le_iff]  intro R₁_pos R₁_lt_R₂  simp_rw [iSup_pos R₁_pos, iSup_pos R₁_lt_R₂]  apply le_of_eq  symm  apply Filter.Tendsto.liminf_eq  apply Filter.Tendsto.enorm  apply tendsto_carlesonOperatorIntegrand_of_dominated_convergence R₁_pos bound hF_meas h_bound _    h_lim  apply IntegrableOn.mono_set _ Annulus.oo_subset_ball  apply IntegrableOn.mono_set _ ball_subset_closedBall  apply bound_integrable.integrableOn_isCompact (isCompact_closedBall _ _)