Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.hf.hp
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
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ ∀ x_1 ∈ {y | dist x y ∈ Set.Ioo r 1}, ‖cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)‖ ≤ ?m.492969

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
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ ℝ
Tactic:
intro y hy
Proof state after:
case e_a.hf.hp
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
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
y : ℝ
hy : y ∈ {y | dist x y ∈ Set.Ioo r 1}
⊢ ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ ?m.492969

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
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ ℝ