internlm/Lean-Github huggingface dataset:
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof state before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
this :
  1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
⊢ partialFourierSum f N x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
exact partialFourierSum_eq_conv_dirichletKernel h
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof state before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
congr 1
Proof state after:
case e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof state before:
case e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
apply intervalIntegral.integral_congr_ae
Proof state after:
case e_a.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι 0 (2 * Real.pi) → f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof state before:
case e_a.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι 0 (2 * Real.pi) → f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Tactic:
apply MeasureTheory.ae_imp_of_ae_restrict
Proof state after:
case e_a.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)),
    f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof state before:
case e_a.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)),
    f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Tactic:
apply MeasureTheory.ae_restrict_of_ae
Proof state after:
case e_a.h.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof state before:
case e_a.h.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Tactic:
sorry
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
x r R : ℝ
r_nonneg : 0 ≤ r
⊢ {y | dist x y ∈ Set.Ioo r R} = Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)
Tactic:
ext y
Proof state after:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo r R} ↔ y ∈ Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)
Theorem: annulus_real_eq
Proof state before:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ y ∈ {y | dist x y ∈ Set.Ioo r R} ↔ y ∈ Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)
Tactic:
simp
Proof state after:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ r < dist x y ∧ dist x y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Theorem: annulus_real_eq
Proof state before:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ r < dist x y ∧ dist x y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
rw [Real.dist_eq, lt_abs, abs_lt]
Proof state after:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Theorem: annulus_real_eq
Proof state before:
case h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R ↔ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
constructor
Proof state after:
case h.mp
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R → x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mp
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R → x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. rintro ⟨(h₀ | h₀), h₁, h₂⟩
  . left
    constructor <;> linarith
  . right
    constructor <;> linarith
Proof state after:
case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. rintro (⟨h₀, h₁⟩ | ⟨h₀, h₁⟩)
  . constructor
    . left
      linarith
    . constructor <;> linarith
  . constructor
    . right
      linarith
    . constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mp
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R → x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
rintro ⟨(h₀ | h₀), h₁, h₂⟩
Proof state after:
case h.mp.intro.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Theorem: annulus_real_eq
Proof state before:
case h.mp.intro.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R

case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
. left
  constructor <;> linarith
Proof state after:
case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Theorem: annulus_real_eq
Proof state before:
case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
. right
  constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mp.intro.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
left
Proof state after:
case h.mp.intro.inl.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r
Theorem: annulus_real_eq
Proof state before:
case h.mp.intro.inl.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < x - y
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mp.intro.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R
Tactic:
right
Proof state after:
case h.mp.intro.inr.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x + r < y ∧ y < x + R
Theorem: annulus_real_eq
Proof state before:
case h.mp.intro.inr.intro.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : r < -(x - y)
h₁ : -R < x - y
h₂ : x - y < R
⊢ x + r < y ∧ y < x + R
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
⊢ x - R < y ∧ y < x - r ∨ x + r < y ∧ y < x + R → (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
rintro (⟨h₀, h₁⟩ | ⟨h₀, h₁⟩)
Proof state after:
case h.mpr.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R

case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. constructor
  . left
    linarith
  . constructor <;> linarith
Proof state after:
case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
. constructor
  . right
    linarith
  . constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
constructor
Proof state after:
case h.mpr.inl.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Tactic:
. left
  linarith
Proof state after:
case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Tactic:
. constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y ∨ r < -(x - y)
Tactic:
left
Proof state after:
case h.mpr.inl.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ r < x - y
Tactic:
linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inl.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x - R < y
h₁ : y < x - r
⊢ -R < x - y ∧ x - y < R
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ (r < x - y ∨ r < -(x - y)) ∧ -R < x - y ∧ x - y < R
Tactic:
constructor
Proof state after:
case h.mpr.inr.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < x - y ∨ r < -(x - y)

case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Tactic:
. right
  linarith
Proof state after:
case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Tactic:
. constructor <;> linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro.left
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < x - y ∨ r < -(x - y)
Tactic:
right
Proof state after:
case h.mpr.inr.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < -(x - y)
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro.left.h
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ r < -(x - y)
Tactic:
linarith
Proof state after:
no goals
Theorem: annulus_real_eq
Proof state before:
case h.mpr.inr.intro.right
x r R : ℝ
r_nonneg : 0 ≤ r
y : ℝ
h₀ : x + r < y
h₁ : y < x + R
⊢ -R < x - y ∧ x - y < R
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
f : ℝ → ℂ
hf : Measurable f
⊢ Measurable (CarlesonOperatorRat' K f)
Tactic:
apply measurable_iSup
Proof state after:
case hf
f : ℝ → ℂ
hf : Measurable f
⊢ ∀ (i : ℤ),
    Measurable fun b =>
      ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑i * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf
f : ℝ → ℂ
hf : Measurable f
⊢ ∀ (i : ℤ),
    Measurable fun b =>
      ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑i * ↑y).exp‖₊
Tactic:
intro n
Proof state after:
case hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ Measurable fun b =>
    ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ Measurable fun b =>
    ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply measurable_iSup
Proof state after:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ ∀ (i : ℚ),
    Measurable fun b =>
      ⨆ (_ : 0 < i), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑i) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ ∀ (i : ℚ),
    Measurable fun b =>
      ⨆ (_ : 0 < i), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑i) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
intro r
Proof state after:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ Measurable fun b =>
    ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ Measurable fun b =>
    ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply measurable_iSup
Proof state after:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ 0 < r → Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ 0 < r → Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
intro hr
Proof state after:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply Measurable.coe_nnreal_ennreal
Proof state after:
case hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun x => ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (↑r) 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun x => ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (↑r) 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply Measurable.nnnorm
Proof state after:
case hf.hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun a => ∫ (y : ℝ) in {y | dist a y ∈ Set.Ioo (↑r) 1}, f y * K a y * (Complex.I * ↑n * ↑y).exp
Theorem: CarlesonOperatorRat'_measurable
Proof state before:
case hf.hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun a => ∫ (y : ℝ) in {y | dist a y ∈ Set.Ioo (↑r) 1}, f y * K a y * (Complex.I * ↑n * ↑y).exp
Tactic:
sorry
Proof state after:
no goals
Theorem: CarlesonOperatorReal'_measurable
Proof state before:
f : ℝ → ℂ
hf : Measurable f
⊢ Measurable (T' f)
Tactic:
sorry
Proof state after:
no goals
Theorem: CarlesonOperatorReal'_mul
Proof state before:
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ T' f x = ↑a.toNNReal * T' (fun x => 1 / ↑a * f x) x
Tactic:
rw [CarlesonOperatorReal', CarlesonOperatorReal', ENNReal.mul_iSup]
Proof state after:
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ ⨆ 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‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ ⨆ 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‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ r,
          ⨆ (_ : 0 < r),
            ⨆ (_ : r < 1),
              ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊
Tactic:
congr
Proof state after:
case e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ (fun 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‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
⊢ (fun 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‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑i * ↑y).exp‖₊
Tactic:
ext n
Proof state after:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ↑a.toNNReal *
      ⨆ r,
        ⨆ (_ : 0 < r),
          ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
rw [ENNReal.mul_iSup]
Proof state after:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ (_ : 0 < i),
          ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ⨆ i,
      ↑a.toNNReal *
        ⨆ (_ : 0 < i),
          ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
congr
Proof state after:
case e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ (fun 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‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
⊢ (fun 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‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
ext r
Proof state after:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
rw [ENNReal.mul_iSup]
Proof state after:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ⨆ (_ : 0 < r),
      ↑a.toNNReal *
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ⨆ (_ : 0 < r),
      ↑a.toNNReal *
        ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
congr
Proof state after:
case e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ (fun x_1 => ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Theorem: CarlesonOperatorReal'_mul
Proof state before:
case e_s.h.e_s.h.e_s
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
n : ℤ
r : ℝ
⊢ (fun x_1 => ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊) =
    fun i =>
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
ext rpos
Proof state after:
case e_s.h.e_s.h.e_s.h
f : ℝ → ℂ
x a : ℝ
ha : 0 < a
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‖₊ =
    ↑a.toNNReal *
      ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, 1 / ↑a * f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊