continuous_carlesonOperatorIntegrand

lemma continuous_carlesonOperatorIntegrand (mf : Measurable f) (nf : (‖f ·‖) ≤ 1) (hR₁ : 0 < R₁) :    Continuous (carlesonOperatorIntegrand K · R₁ R₂ f x) := by  rcases le_or_gt R₂ R₁ with hR₂ | hR₂  · unfold carlesonOperatorIntegrand; rw [Annulus.oo_eq_empty (by simp [hR₂])]    simp_rw [setIntegral_empty]; exact continuous_const  lift R₁ to ℝ≥0 using hR₁.le  lift R₂ to ℝ≥0 using (hR₁.trans hR₂).le  rw [NNReal.coe_pos] at hR₁; rw [NNReal.coe_lt_coe] at hR₂  have R₂pos := hR₁.trans hR₂  rw [continuous_iff]; intro ϑ ε εpos  let C₁ := As (defaultA a) (dist o x + R₂ + dist o x)  have C₁pos : 0 < C₁ := by unfold C₁ As; norm_cast; positivity  have C₂pos : 0 < C3_0_1 a R₁ R₂ := by rw [C3_0_1]; positivity  refine ⟨ε / (C₁ * C3_0_1 a R₁ R₂), by positivity, fun θ db ↦ ?_⟩  calc    _ ≤ _ := dist_carlesonOperatorIntegrand_le mf nf hR₁    _ ≤ C3_0_1 a R₁ R₂ * C₁ * dist θ ϑ := by rw [mul_assoc]; gcongr; apply cdist_le_dist; positivity    _ < _ := by rwa [← lt_div_iff₀' (by positivity), mul_comm]