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)))
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]
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof 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]
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 * 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']
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)))
⊢ ⨆ 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)‖₊
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 * 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
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 * 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)‖₊
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 * 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
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 * 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)‖₊
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 * 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
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 * 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)‖₊
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 * 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
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 * 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)‖₊
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 * 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
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof 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
Proof 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)‖₊
Theorem: le_CarlesonOperatorReal'
Proof 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
Proof 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)‖₊
Theorem: le_CarlesonOperatorReal'
Proof 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
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤
    ENNReal.ofReal (δ * C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
calc ε * MeasureTheory.volume E
  _ = ∫⁻ _ in E, ε := by
    symm
    apply MeasureTheory.set_lintegral_const
  _ ≤ ∫⁻ x in E, T' f x := by
    apply MeasureTheory.set_lintegral_mono' measurableSetE hE
  _ = ENNReal.ofReal δ * ∫⁻ x in E, T' (fun x ↦ (1 / δ) * f x) x := by
    rw [← MeasureTheory.lintegral_const_mul']
    congr
    ext x
    rw [CarlesonOperatorReal'_mul δpos]
    congr
    exact ENNReal.ofReal_ne_top
  _ ≤ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume E) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹) := by
    gcongr
    apply rcarleson' measurableSetF measurableSetE
    intro x
    simp
    rw [_root_.abs_of_nonneg δpos.le, inv_mul_le_iff δpos]
    exact hf x
  _ = ENNReal.ofReal (δ * C1_2 4 2) * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume E) ^ (2 : ℝ)⁻¹ := by
    rw [ENNReal.ofReal_mul δpos.le]
    ring
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E = ∫⁻ (x : ℝ) in E, ε
Tactic:
symm
Proof state after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, ε = ε * MeasureTheory.volume E
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, ε = ε * MeasureTheory.volume E
Tactic:
apply MeasureTheory.set_lintegral_const
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, ε ≤ ∫⁻ (x : ℝ) in E, T' f x
Tactic:
apply MeasureTheory.set_lintegral_mono' measurableSetE hE
Proof state after:
no goals
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' f x = ENNReal.ofReal δ * ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x
Tactic:
rw [← MeasureTheory.lintegral_const_mul']
Proof state after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' f x = ∫⁻ (a : ℝ) in E, ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Theorem: rcarleson_exceptional_set_estimate
Proof state before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' f x = ∫⁻ (a : ℝ) in E, ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
congr
Proof state after:
case e_f
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ (fun x => T' f x) = fun a => ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤