Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y *
          (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
            (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
calc ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (exp (I * (-n * x)) * K x y * exp (I * n * y) + (starRingEnd ℂ) (exp (I * (-n * x)) * K x y * exp (I * n * y)))‖₊
  _ = ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (exp (I * (-n * x)) * K x y * exp (I * n * y)) + f y * (starRingEnd ℂ) (exp (I * (-n * x)) * K x y * exp (I * n * y))‖₊ := by
    congr
    ext y
    rw [mul_add]
  _ = ‖ (∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (exp (I * (-n * x)) * K x y * exp (I * n * y)))
       + ∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (starRingEnd ℂ) (exp (I * (-n * x)) * K x y * exp (I * n * y))‖₊ := by
    congr
    have measurable₁ : Measurable fun x_1 ↦ (I * (-↑n * ↑x)).exp * K x x_1 * (I * ↑n * ↑x_1).exp := by
      apply Measurable.mul
      apply Measurable.mul
      measurability
      apply Measurable.of_uncurry_left
      exact Hilbert_kernel_measurable
      measurability
    have boundedness₁ {y : ℝ} (h : r ≤ dist x y) : ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by
      calc ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖
        _ = ‖(I * (-↑n * ↑x)).exp‖ * ‖K x y‖ * ‖(I * ↑n * ↑y).exp‖ := by
          rw [norm_mul, norm_mul]
        _ ≤ 1 * (2 ^ (2 : ℝ) / (2 * |x - y|)) * 1 := by
          gcongr
          . rw [norm_eq_abs, mul_comm]
            norm_cast
            rw [abs_exp_ofReal_mul_I]
          . apply Hilbert_kernel_bound
          . rw [norm_eq_abs, mul_assoc, mul_comm]
            norm_cast
            rw [abs_exp_ofReal_mul_I]
        _ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by
          rw [one_mul, mul_one, ← Real.dist_eq]
          gcongr
    have integrable₁ := (integrable_annulus hx hf rpos.le rle1)
    rw [MeasureTheory.integral_add]
    . conv => pattern ((f _) * _); rw [mul_comm]
      apply MeasureTheory.Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable
      . rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
        apply eventually_of_forall
        intro y hy
        exact boundedness₁ hy.1.le
    . conv => pattern ((f _) * _); rw [mul_comm]
      apply MeasureTheory.Integrable.bdd_mul' integrable₁
      . apply Measurable.aestronglyMeasurable
        apply Measurable.comp continuous_star.measurable measurable₁
      . rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
        apply eventually_of_forall
        intro y hy
        rw [RCLike.norm_conj]
        exact boundedness₁ hy.1.le
  _ ≤   ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (exp (I * (-n * x)) * K x y * exp (I * n * y))‖₊
      + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (starRingEnd ℂ) (exp (I * (-n * x)) * K x y * exp (I * n * y))‖₊ := by
    apply nnnorm_add_le
  _ =   ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, exp (I * (-n * x)) * (f y * K x y * exp (I * n * y))‖₊
      + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, exp (I * (-n * x)) * (((starRingEnd ℂ) ∘ f) y *  K x y * exp (I * n * y))‖₊ := by
      congr 1
      . congr
        ext y
        ring
      . rw [←nnnorm_star, ←starRingEnd_apply, ←integral_conj]
        congr
        ext y
        simp
        ring
  _ =   ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * exp (I * n * y)‖₊
      + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, ((starRingEnd ℂ) ∘ f) y * K x y * exp (I * n * y)‖₊ := by
    rw [← NNReal.coe_inj]
    push_cast
    norm_cast
    congr 1 <;>
    . rw [MeasureTheory.integral_mul_left, norm_mul, norm_eq_abs, mul_comm I, abs_exp_ofReal_mul_I, one_mul]
Proof state after:
no goals