rcarleson_exceptional_set_estimate

lemma rcarleson_exceptional_set_estimate {δ C : ℝ≥0} (Cpos : 0 < C) {f : ℝ → ℂ}  (hmf : Measurable f) {F : Set ℝ} (measurableSetF : MeasurableSet F)  (hf : ∀ x, ‖f x‖ ≤ C * F.indicator 1 x) {E : Set ℝ} (measurableSetE : MeasurableSet E)  (hE : ∀ x ∈ E, δ ≤ T f x) :    δ * volume E ≤ C * C10_0_1 4 2 * volume F ^ (2 : ℝ)⁻¹ * volume E ^ (2 : ℝ)⁻¹ := by  calc δ * volume E    _ = ∫⁻ _ in E, δ := by      symm      apply setLIntegral_const    _ ≤ ∫⁻ x in E, T f x := by      apply setLIntegral_mono' measurableSetE hE    _ = C * ∫⁻ x in E, T (fun x ↦ (1 / C) * f x) x := by      rw [← lintegral_const_mul']      swap; · exact ENNReal.coe_ne_top      congr with x      rw [carlesonOperatorReal_mul Cpos]      simp    _ ≤ C * (C10_0_1 4 2 * (volume E) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹) := by      gcongr      apply rcarleson measurableSetF measurableSetE _ (by fun_prop)      intro x      simp only [one_div, Complex.norm_mul, norm_inv, norm_real, norm_eq_abs, NNReal.abs_eq]      rw [inv_mul_le_iff₀ (by simp [Cpos])]      exact hf x    _ = C * C10_0_1 4 2 * (volume F) ^ (2 : ℝ)⁻¹ * (volume E) ^ (2 : ℝ)⁻¹ := by      ring