Le Carleson Operator Real

lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-π) (3 * π)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :    ‖∫ (y : ℝ) in x - π..x + π, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ    ≤ T g x + T (conj ∘ g) x := by  rw [domain_reformulation hg hx]  set s : ℕ → Set ℝ := fun n ↦ {y | dist x y ∈ Set.Ioo (1 / (n + 2 : ℝ)) 1} with sdef  have hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n := by    ext y    constructor    · intro hy      rw [Set.mem_setOf_eq, Set.mem_Ioo] at hy      obtain ⟨n, hn⟩ := exists_nat_gt (1 / dist x y)      rw [Set.mem_iUnion]      use n      rw [sdef, Set.mem_setOf_eq, one_div]      refine ⟨?_, hy.2⟩      rw [inv_lt_comm₀ (by linarith) hy.1, inv_eq_one_div]      apply lt_trans hn      linarith    · intro hy      simp only [Set.mem_iUnion] at hy      rcases hy with ⟨n, hn⟩      rw [sdef] at hn      simp only [one_div, Set.mem_Ioo, Set.mem_setOf_eq] at hn      refine ⟨lt_trans' hn.1 ?_, hn.2⟩      norm_num      linarith  have : Tendsto (fun i => ∫ y in s i, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))          atTop (𝓝 (∫ y in ⋃ n, s n, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) := by    apply tendsto_setIntegral_of_monotone    · exact fun n ↦ annulus_measurableSet    · intro n m nlem y hy      rw [sdef] at *      simp only [one_div, Set.mem_Ioo, Set.mem_setOf_eq] at *      refine ⟨lt_of_le_of_lt ?_ hy.1, hy.2⟩      rw [inv_le_inv₀]      on_goal 1 => norm_cast      all_goals linarith    · rw [← hs]      --uses that dirichletKernel' is bounded      exact intervalIntegrable_mul_dirichletKernel'_specific hx hg  calc    _ = ‖∫ y in ⋃ n, s n, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ := by congr    _ ≤ ⨆ (i : ℕ), ↑‖∫ y in s i, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖ₑ :=      le_iSup_of_tendsto this.enorm    _ ≤ ⨆ (r : ℝ) (_ : 0 < r) (_ : r < 1), ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g 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 only [one_div, inv_pos]; linarith)        (by rw [div_lt_iff₀] <;> linarith)      rfl    _ = ⨆ (r : ℝ) (_ : 0 < r) (_ : r < 1), ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * (exp (I * (-(Int.ofNat N) * x)) * K x y * exp (I * N * y) + conj (exp (I * (-(Int.ofNat N) * x)) * K x y * exp (I * (Int.ofNat N) * y)))‖ₑ := by      gcongr      congr with y      congr      rw [Dirichlet_Hilbert_eq]      simp only [Complex.ofReal_sub, mul_comm, mul_neg, ← mul_assoc, k, map_mul, ← exp_conj,        map_neg, conj_I, map_sub, conj_ofReal, map_natCast, neg_neg, map_div₀, map_one,        Int.ofNat_eq_natCast, Int.cast_natCast, K, ← Complex.exp_add, map_add]      ring_nf    _ ≤ ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1), ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * (exp (I * (-n * x)) * K x y * exp (I * n * y) + conj (exp (I * (-n * x)) * K x y * exp (I * n * y)))‖ₑ := by      let F : ℤ → ℝ≥0∞ := fun (n : ℤ) ↦ ⨆ (r : ℝ) (_ : 0 < r) (_ : r < 1), ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * (exp (I * (-n * x)) * K x y * exp (I * n * y) + conj (exp (I * (-n * x)) * K x y * exp (I * n * y)))‖ₑ      exact le_iSup F ((Int.ofNat N))    _ ≤ ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1),        (‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * K x y * exp (I * n * y)‖ₑ        + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, (conj ∘ g) y * K x y * exp (I * n * y)‖ₑ) := by      gcongr with n r rpos rle1      norm_cast      push_cast      calc        _ = ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * (exp (I * (-n * x)) * K x y * exp (I * n * y)) + g y * conj (exp (I * (-n * x)) * K x y * exp (I * n * y))‖ₑ := by          congr with y          rw [mul_add]        _ = ‖(∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * (exp (I * (-n * x)) * K x y * exp (I * n * y)))            + ∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * conj (exp (I * (-n * x)) * K x y * exp (I * n * y))‖ₑ := by          congr          -- Integrability follows from r > 0          have measurable₁ : Measurable fun x_1 ↦ (I * (-↑n * ↑x)).exp * K x x_1 * (I * ↑n * ↑x_1).exp := by            apply Measurable.mul (Measurable.mul _ Hilbert_kernel_measurable.of_uncurry_left) <;>              fun_prop          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 [mul_comm]                  norm_cast                  rw [norm_exp_ofReal_mul_I]                · exact Hilbert_kernel_bound                · rw [mul_assoc, mul_comm]                  norm_cast                  rw [norm_exp_ofReal_mul_I]              _ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by                rw [one_mul, mul_one, ← Real.dist_eq]                gcongr          have integrable₁ := integrable_annulus hx hg rpos.le rle1          rw [integral_add]          · conv => pattern ((g _) * _); rw [mul_comm]            apply Integrable.bdd_mul integrable₁ measurable₁.aestronglyMeasurable            · rw [ae_restrict_iff' annulus_measurableSet]              on_goal 1 => apply Eventually.of_forall              exact fun _ hy ↦ boundedness₁ hy.1.le          · conv => pattern ((g _) * _); rw [mul_comm]            apply Integrable.bdd_mul integrable₁ (by fun_prop)            · rw [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}, g y * (exp (I * (-n * x)) * K x y * exp (I * n * y))‖ₑ            + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * conj (exp (I * (-n * x)) * K x y * exp (I * n * y))‖ₑ := by          apply enorm_add_le        _ =   ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, exp (I * (-n * x)) * (g y * K x y * exp (I * n * y))‖ₑ            + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, exp (I * (-n * x)) * ((conj ∘ g) y * K x y * exp (I * n * y))‖ₑ := by            congr 1            · congr! 3 with y; ring            · rw [← RCLike.enorm_conj, ← integral_conj]              congr! 3 with _ y              simp              ring        _ =   ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, g y * K x y * exp (I * n * y)‖ₑ            + ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, (conj ∘ g) y * K x y * exp (I * n * y)‖ₑ := by          congr 1 <;>          rw [integral_const_mul, enorm_mul, show (-n * x : ℂ) = ((-n * x : ℝ) : ℂ) by norm_cast,            enorm_exp_I_mul_ofReal, one_mul]    _ ≤ T g x + T (conj ∘ g) x := by      simp_rw [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