Theorem: le_CarlesonOperatorReal'
Proof state before:
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)))
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Tactic:
calc ENNReal.ofNNReal ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊
  _ = ‖∫ y in ⋃ n, s n, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ := by
    congr
  _ ≤ ⨆ (i : ℕ), ↑‖∫ y in s i, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ := by
    apply le_iSup_of_tendsto
    rw [ENNReal.tendsto_coe]
    apply Tendsto.nnnorm this
  _ ≤ ⨆ (r : ℝ) (_ : 0 < r) (_ : r < 1), ↑‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ := by
    apply iSup_le
    intro n
    apply le_iSup_of_le (1 / (n + 2 : ℝ))
    apply le_iSup₂_of_le (by simp; linarith) (by rw [div_lt_iff] <;> linarith)
    rfl
  _ = ⨆ (r : ℝ) (_ : 0 < r) (_ : r < 1), ↑‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * (exp (I * (-(Int.ofNat N) * x)) * K x y * exp (I * N * y) + (starRingEnd ℂ) (exp (I * (-(Int.ofNat N) * x)) * K x y * exp (I * (Int.ofNat N) * y)))‖₊ := by
    apply iSup_congr
    intro r
    apply iSup_congr
    intro _
    apply iSup_congr
    intro _
    congr
    ext y
    rw [mul_assoc, dirichlet_Hilbert_eq]
    norm_cast
  _ ≤ ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1), ↑‖∫ 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)))‖₊ := by
    let F : ℤ → ENNReal := fun (n : ℤ) ↦ ⨆ (r : ℝ) (_ : 0 < r) (_ : r < 1), ↑‖∫ 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)))‖₊
    apply le_iSup F ((Int.ofNat N))
  _ ≤ ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1), (  ↑‖∫ 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
    apply iSup₂_mono
    intro n r
    apply iSup₂_mono
    intro rpos rle1
    norm_cast
    push_cast
    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]
  _ ≤ T' f x + T' ((starRingEnd ℂ) ∘ f) x := by
    rw [CarlesonOperatorReal', CarlesonOperatorReal']
    apply iSup₂_le
    intro n r
    apply iSup₂_le
    intro rpos rle1
    gcongr <;>
    . apply le_iSup₂_of_le n r
      apply le_iSup₂_of_le rpos rle1
      trivial
Proof state after:
no goals