Theorem: le_CarlesonOperatorReal' (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
case e_a.hg
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})
⊢ MeasureTheory.Integrable (fun y => (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) * f y)
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Tactic:
apply MeasureTheory.Integrable.bdd_mul' integrable₁
State after:
case e_a.hg.hf
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})
⊢ MeasureTheory.AEStronglyMeasurable
    (fun x_1 => (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})

case e_a.hg.hf_bound
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 : ℝ) ∂MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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})
⊢ ℝ

State before:
case e_a.hg.hf
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})
⊢ MeasureTheory.AEStronglyMeasurable
    (fun x_1 => (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})

case e_a.hg.hf_bound
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 : ℝ) ∂MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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:
. apply Measurable.aestronglyMeasurable
  apply Measurable.comp continuous_star.measurable measurable₁
State after:
case e_a.hg.hf_bound
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 : ℝ) ∂MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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})
⊢ ℝ

State before:
case e_a.hg.hf_bound
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 : ℝ) ∂MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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:
. rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
  apply eventually_of_forall
  intro y hy
  rw [RCLike.norm_conj]
  exact boundedness₁ hy.1.le
State after:
no goals

State before:
case e_a.hg.hf
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})
⊢ MeasureTheory.AEStronglyMeasurable
    (fun x_1 => (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Tactic:
apply Measurable.aestronglyMeasurable
State after:
case e_a.hg.hf.hf
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})
⊢ Measurable fun x_1 => (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))

State before:
case e_a.hg.hf.hf
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})
⊢ Measurable fun x_1 => (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))
Tactic:
apply Measurable.comp continuous_star.measurable measurable₁
State after:
no goals

State before:
case e_a.hg.hf_bound
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 : ℝ) ∂MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150
Tactic:
rw [MeasureTheory.ae_restrict_iff' annulus_measurableSet]
State after:
case e_a.hg.hf_bound
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 : ℝ),
    x_1 ∈ {y | dist x y ∈ Set.Ioo r 1} →
      ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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})
⊢ ℝ

State before:
case e_a.hg.hf_bound
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 : ℝ),
    x_1 ∈ {y | dist x y ∈ Set.Ioo r 1} →
      ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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:
apply eventually_of_forall
State after:
case e_a.hg.hf_bound.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},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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})
⊢ ℝ

State before:
case e_a.hg.hf_bound.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},
    ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1))‖ ≤ ?m.494150

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
State after:
case e_a.hg.hf_bound.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}
⊢ ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖ ≤ ?m.494150

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})
⊢ ℝ

State before:
case e_a.hg.hf_bound.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}
⊢ ‖(starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖ ≤ ?m.494150

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:
rw [RCLike.norm_conj]
State after:
case e_a.hg.hf_bound.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.494150

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})
⊢ ℝ

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})
⊢ ℝ

State before:
case e_a.hg.hf_bound.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.494150

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})
⊢ ℝ

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:
exact boundedness₁ hy.1.le
State after:
no goals

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)))
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))) +
        ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f 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 * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
apply nnnorm_add_le
State after:
no goals

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)))
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))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr 1
State after:
case e_a
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))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊

case e_a
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 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊

State before:
case e_a
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))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊

case e_a
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 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
. congr
  ext y
  ring
State after:
case e_a
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 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊

State before:
case e_a
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 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
. rw [←nnnorm_star, ←starRingEnd_apply, ←integral_conj]
  congr
  ext y
  simp
  ring
State after:
no goals

State before:
case e_a
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))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr
State after:
case e_a.e_a.e_f
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
⊢ (fun y => f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) = fun y =>
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))

State before:
case e_a.e_a.e_f
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
⊢ (fun y => f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) = fun y =>
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))
Tactic:
ext y
State after:
case e_a.e_a.e_f.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 : ℝ
⊢ f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))

State before:
case e_a.e_a.e_f.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 : ℝ
⊢ f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))
Tactic:
ring
State after:
no goals

State before:
case e_a
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 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
rw [←nnnorm_star, ←starRingEnd_apply, ←integral_conj]
State after:
case e_a
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
⊢ ‖∫ (x_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊

State before:
case e_a
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
⊢ ‖∫ (x_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr
State after:
case e_a.e_a.e_f
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
⊢ (fun x_1 => (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))) =
    fun y => cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))

State before:
case e_a.e_a.e_f
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
⊢ (fun x_1 => (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))) =
    fun y => cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))
Tactic:
ext y
State after:
case e_a.e_a.e_f.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 : ℝ
⊢ (starRingEnd ℂ) (f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) =
    cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))

State before:
case e_a.e_a.e_f.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 : ℝ
⊢ (starRingEnd ℂ) (f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) =
    cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))
Tactic:
simp
State after:
case e_a.e_a.e_f.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 : ℝ
⊢ (starRingEnd ℂ) (f y) * (cexp (-(I * (↑n * ↑x))) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (-(I * (↑n * ↑x))) * ((starRingEnd ℂ) (f y) * K x y * cexp (I * ↑n * ↑y))

State before:
case e_a.e_a.e_f.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 : ℝ
⊢ (starRingEnd ℂ) (f y) * (cexp (-(I * (↑n * ↑x))) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (-(I * (↑n * ↑x))) * ((starRingEnd ℂ) (f y) * K x y * cexp (I * ↑n * ↑y))
Tactic:
ring
State after:
no goals

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)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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:
rw [← NNReal.coe_inj]
State after:
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}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
        ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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)‖₊)

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)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑(‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
        ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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:
push_cast
State after:
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}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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)‖

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)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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:
norm_cast
State after:
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}, cexp (I * ↑(↑(-n) * x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * ↑(↑(-n) * x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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)‖

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)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * ↑(↑(-n) * x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * ↑(↑(-n) * x)) * ((⇑(starRingEnd ℂ) ∘ f) y * 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:
congr 1 <;>
. rw [MeasureTheory.integral_mul_left, norm_mul, norm_eq_abs, mul_comm I, abs_exp_ofReal_mul_I, one_mul]
State after:
no goals

State before:
case e_a
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},
        cexp (I * ↑(↑(-n) * x)) * ((⇑(starRingEnd ℂ) ∘ 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:
rw [MeasureTheory.integral_mul_left, norm_mul, norm_eq_abs, mul_comm I, abs_exp_ofReal_mul_I, one_mul]
State after:
no goals

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)))
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (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)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Tactic:
rw [CarlesonOperatorReal', CarlesonOperatorReal']
State after:
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,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (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)‖₊ ≤
    (⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
      ⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊

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)))
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (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)‖₊ ≤
    (⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
      ⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
apply iSup₂_le
State after:
case 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)))
⊢ ∀ (i : ℤ) (j : ℝ),
    ⨆ (_ : 0 < j),
        ⨆ (_ : j < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo j 1}, f y * K x y * cexp (I * ↑i * ↑y)‖₊ +
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo j 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑i * ↑y)‖₊ ≤
      (⨆ n,
          ⨆ r,
            ⨆ (_ : 0 < r),
              ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
        ⨆ n,
          ⨆ r,
            ⨆ (_ : 0 < r),
              ⨆ (_ : r < 1),
                ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊

State before:
case 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)))
⊢ ∀ (i : ℤ) (j : ℝ),
    ⨆ (_ : 0 < j),
        ⨆ (_ : j < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo j 1}, f y * K x y * cexp (I * ↑i * ↑y)‖₊ +
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo j 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑i * ↑y)‖₊ ≤
      (⨆ n,
          ⨆ r,
            ⨆ (_ : 0 < r),
              ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
        ⨆ n,
          ⨆ r,
            ⨆ (_ : 0 < r),
              ⨆ (_ : r < 1),
                ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
intro n r
State after:
case 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 : ℝ
⊢ ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (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)‖₊ ≤
    (⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
      ⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊

State before:
case 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 : ℝ
⊢ ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (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)‖₊ ≤
    (⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
      ⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
apply iSup₂_le
State after:
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 : ℝ
⊢ 0 < r →
    r < 1 →
      ↑‖∫ (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)‖₊ ≤
        (⨆ n,
            ⨆ r,
              ⨆ (_ : 0 < r),
                ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
          ⨆ n,
            ⨆ r,
              ⨆ (_ : 0 < r),
                ⨆ (_ : r < 1),
                  ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊

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 : ℝ
⊢ 0 < r →
    r < 1 →
      ↑‖∫ (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)‖₊ ≤
        (⨆ n,
            ⨆ r,
              ⨆ (_ : 0 < r),
                ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
          ⨆ n,
            ⨆ r,
              ⨆ (_ : 0 < r),
                ⨆ (_ : r < 1),
                  ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
intro rpos rle1
State after:
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 * 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)‖₊ ≤
    (⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
      ⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊

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 * 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)‖₊ ≤
    (⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊) +
      ⨆ n,
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
gcongr <;>
. apply le_iSup₂_of_le n r
  apply le_iSup₂_of_le rpos rle1
  trivial
State after:
no goals

State before:
case h.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}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊ ≤
    ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
apply le_iSup₂_of_le n r
State after:
case h.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}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊ ≤
    ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊

State before:
case h.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}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊ ≤
    ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
apply le_iSup₂_of_le rpos rle1
State after:
case h.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}, (⇑(starRingEnd ℂ) ∘ 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)‖₊

State before:
case h.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}, (⇑(starRingEnd ℂ) ∘ 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:
trivial
State after:
no goals