Theorem: CarlesonOperatorReal'_le_CarlesonOperator' (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
⊢ T' ≤ CarlesonOperator' K {x | ∃ n, θ n = x}
Tactic:
intro f x
State after:
f : ℝ → ℂ
x : ℝ
⊢ T' f x ≤ CarlesonOperator' K {x | ∃ n, θ n = x} f x

State before:
f : ℝ → ℂ
x : ℝ
⊢ T' f x ≤ CarlesonOperator' K {x | ∃ n, θ n = x} f x
Tactic:
rw [CarlesonOperator', CarlesonOperatorReal']
State after:
f : ℝ → ℂ
x : ℝ
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
f : ℝ → ℂ
x : ℝ
⊢ ⨆ n,
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
State after:
case h
f : ℝ → ℂ
x : ℝ
⊢ ∀ (i : ℤ),
    ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h
f : ℝ → ℂ
x : ℝ
⊢ ∀ (i : ℤ),
    ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro n
State after:
case h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
State after:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ∀ (i : ℝ),
    ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
⊢ ∀ (i : ℝ),
    ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro r
State after:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
State after:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ 0 < r →
    ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
⊢ 0 < r →
    ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro rpos
State after:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply iSup_le
State after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ r < 1 →
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
⊢ r < 1 →
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
      ⨆ Q ∈ {x | ∃ n, θ n = x},
        ⨆ R₁,
          ⨆ R₂,
            ⨆ (_ : 0 < R₁),
              ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
intro rle1
State after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊

State before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ Q ∈ {x | ∃ n, θ n = x},
      ⨆ R₁,
        ⨆ R₂,
          ⨆ (_ : 0 < R₁),
            ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * Q y).exp‖₊
Tactic:
apply le_iSup₂_of_le (θ n) (by simp)
State after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ R₁,
      ⨆ R₂,
        ⨆ (_ : 0 < R₁),
          ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * (θ n) y).exp‖₊

State before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ R₁,
      ⨆ R₂,
        ⨆ (_ : 0 < R₁),
          ⨆ (_ : R₁ < R₂), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo R₁ R₂}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
apply le_iSup₂_of_le r 1
State after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊

State before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
apply le_iSup₂_of_le rpos rle1
State after:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊

State before:
case h.h.h.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
apply le_of_eq
State after:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊

State before:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (θ n) y).exp‖₊
Tactic:
rw [integer_linear, ContinuousMap.coe_mk]
State after:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (↑n * ↑y)).exp‖₊

State before:
case h.h.h.h.a
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, K x y * f y * (Complex.I * (↑n * ↑y)).exp‖₊
Tactic:
congr
State after:
case h.h.h.h.a.e_a.e_a.e_f
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun y => K x y * f y * (Complex.I * (↑n * ↑y)).exp

State before:
case h.h.h.h.a.e_a.e_a.e_f
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ (fun y => f y * K x y * (Complex.I * ↑n * ↑y).exp) = fun y => K x y * f y * (Complex.I * (↑n * ↑y)).exp
Tactic:
ext y
State after:
case h.h.h.h.a.e_a.e_a.e_f.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = K x y * f y * (Complex.I * (↑n * ↑y)).exp

State before:
case h.h.h.h.a.e_a.e_a.e_f.h
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
y : ℝ
⊢ f y * K x y * (Complex.I * ↑n * ↑y).exp = K x y * f y * (Complex.I * (↑n * ↑y)).exp
Tactic:
ring_nf
State after:
no goals

State before:
f : ℝ → ℂ
x : ℝ
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
⊢ θ n ∈ {x | ∃ n, θ n = x}
Tactic:
simp
State after:
no goals