internlm/Lean-Github huggingface dataset:
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)))
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                f y *
                  (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊ ≤
    ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                  f y *
                    (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                      (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊
Tactic:
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)))‖₊
Proof 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)))
F : ℤ → ENNReal :=
  fun n =>
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                f y *
                  (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                f y *
                  (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊ ≤
    ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                  f y *
                    (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                      (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊
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)))
F : ℤ → ENNReal :=
  fun n =>
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                f y *
                  (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                f y *
                  (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊ ≤
    ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                  f y *
                    (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                      (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊
Tactic:
apply le_iSup F ((Int.ofNat N))
Proof state after:
no goals
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)))
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1),
            ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                  f y *
                    (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                      (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ⨆ 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)‖₊
Tactic:
apply iSup₂_mono
Proof 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 *
                  (cexp (I * (-↑i * ↑x)) * K x y * cexp (I * ↑i * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑i * ↑x)) * K x y * cexp (I * ↑i * ↑y)))‖₊ ≤
      ⨆ (_ : 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)‖₊
Theorem: le_CarlesonOperatorReal'
Proof 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 *
                  (cexp (I * (-↑i * ↑x)) * K x y * cexp (I * ↑i * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑i * ↑x)) * K x y * cexp (I * ↑i * ↑y)))‖₊ ≤
      ⨆ (_ : 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)‖₊
Tactic:
intro n r
Proof 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 *
                (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ⨆ (_ : 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)‖₊
Theorem: le_CarlesonOperatorReal'
Proof 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 *
                (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ⨆ (_ : 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)‖₊
Tactic:
apply iSup₂_mono
Proof 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 *
                (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
⊢ 0 < r →
    r < 1 →
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
              f y *
                (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
intro rpos rle1
Proof 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 *
            (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
              (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f y *
            (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
              (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
norm_cast
Proof 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 *
          (cexp (I * ↑(↑(-n) * x)) * K x y * cexp (I * ↑n * ↑y) +
            (starRingEnd ℂ) (cexp (I * ↑(↑(-n) * x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y *
          (cexp (I * ↑(↑(-n) * x)) * K x y * cexp (I * ↑n * ↑y) +
            (starRingEnd ℂ) (cexp (I * ↑(↑(-n) * x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
push_cast
Proof 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 *
          (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
            (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ ≤
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
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)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y *
          (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) +
            (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) +
          f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr
Proof state after:
case 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) +
          (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))) =
    fun y =>
    f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) +
      f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case 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) +
          (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))) =
    fun y =>
    f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) +
      f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))
Tactic:
ext y
Proof state after:
case 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) +
        (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) =
    f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) +
      f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case 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) +
        (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) =
    f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) +
      f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))
Tactic:
rw [mul_add]
Proof state after:
no goals
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)))
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)) +
          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:
congr
Proof 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)) +
        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))